Reasoning about processes in applications such as manufacturing, web services, enterprise modeling, and planning requires the representation of composite processes with complicated flows of control. Previous research in process representation has used formalisms such as Event Systems, Petri nets, and the Unified Modeling Language activity diagrams. The computational hardness of temporal projection problems in Event Systems has been extensively examined in the literature, whereas Petri nets and UML activity diagrams are applied to describe more elaborate processes. This thesis takes a systematic look into the temporal reasoning problems in Event Systems and assigns accurate semantics to both Petri nets and, for the first time, to UML activity diagrams. We give an analysis of computational complexity in temporal projection problems by exploring the boundary between their tractable and intractable subproblems. Our results provide new insights into the prominent role the properties of partial ordering play, however we also show that partial ordering is not the sole source of the intractability as has been claimed in an earlier work by Nebel and B{\"a}ckstr{\"o}m. Two influential modeling languages, Petri nets and UML activity diagrams, are axiomatized as two Basic Action Theories of Situation Calculus. They are called, respectively, SCOPE (Situation Calculus Ontology of PEtri nets) and SCAD (Situation Calculus theory of Activity Diagrams). We provide a Prolog implementation of SCOPE and prove the correctness of this program for regressable queries. We use SCAD to axiomatize the structural and dynamic properties of UML activity diagrams and also provide the first set of computational results with regard to the reachability problems in activity diagrams. The correctness of each of these two axiomatizations is also demonstrated by proving that the theory is satisfiable, and the intended interpretation corresponds to a model of the theory.

Reasoning about processes in applications such as manufacturing, web services, enterprise modeling, and planning requires the representation of composite processes with complicated flows of control. Previous research in process representation has used formalisms such as Event Systems, Petri nets, and the Unified Modeling Language activity diagrams. The computational hardness of temporal projection problems in Event Systems has been extensively examined in the literature, whereas Petri nets and UML activity diagrams are applied to describe more elaborate processes. This thesis takes a systematic look into the temporal reasoning problems in Event Systems and assigns accurate semantics to both Petri nets and, for the first time, to UML activity diagrams. We give an analysis of computational complexity in temporal projection problems by exploring the boundary between their tractable and intractable subproblems. Our results provide new insights into the prominent role the properties of partial ordering play, however we also show that partial ordering is not the sole source of the intractability as has been claimed in an earlier work by Nebel and B{\"a}ckstr{\"o}m. Two influential modeling languages, Petri nets and UML activity diagrams, are axiomatized as two Basic Action Theories of Situation Calculus. They are called, respectively, SCOPE (Situation Calculus Ontology of PEtri nets) and SCAD (Situation Calculus theory of Activity Diagrams). We provide a Prolog implementation of SCOPE and prove the correctness of this program for regressable queries. We use SCAD to axiomatize the structural and dynamic properties of UML activity diagrams and also provide the first set of computational results with regard to the reachability problems in activity diagrams. The correctness of each of these two axiomatizations is also demonstrated by proving that the theory is satisfiable, and the intended interpretation corresponds to a model of the theory.

Advances in scientific data management, discovery, dissemination, and sharing are changing the manner in which scientific studies are being conducted and repurposed. Data-intensive scientific practices increasingly require data management related services not available in existing digital libraries. Complicating the issue are the diversity of functional requirements and content in scientific domains as well as scientists' lack of expertise in information and library sciences. Researchers that utilize simulation and experimentation systems need digital libraries to maintain datasets, input configurations, results, analyses, and related documents. A digital library may be integrated with simulation infrastructures to provide automated support for research components, e.g., simulation interfaces to models, data warehouses, simulation applications, computational resources, and storage systems. Managing and provisioning simulation content allows streamlined experimentation, collaboration, discovery, and content reuse within a simulation community. Formal definitions of this class of digital libraries provide a foundation for producing a software toolkit and the semi-automated generation of digital library instances. We present a generic, component-based SIMulation-supporting Digital Library (SimDL) framework. The framework is formally described and provides a deployable set of domain-free services, schema-based domain knowledge representations, and extensible lower and higher level service abstractions. Services in SimDL are specialized for semi-structured simulation content and large-scale data producing infrastructures, as exemplified in data storage, indexing, and retrieval service implementations. Contributions to the scientific community include previously unavailable simulation-specific services, e.g., incentivizing public contributions, semi-automated content curating, and memoizing simulation-generated data products. The practicality of SimDL is demonstrated through several case studies in computational epidemiology and network science as well as performance evaluations. / Ph. D.

Recent research has shown that it is often preferable to encode real-world problems as propositional satisfiability (SAT) problems and then solve using a general purpose SAT solver. However, much of the valuable information and structure of these realistic problems is flattened out and hidden inside the corresponding Conjunctive Normal Form (CNF) encodings of the SAT domain. Recently, systematic SAT solvers have been progressively improved and are now able to solve many highly structured practical problems containing millions of clauses. In contrast, state-of-the-art Stochastic Local Search (SLS) solvers still have difficulty in solving structured problems, apparently because they are unable to exploit hidden structure as well as the systematic solvers. In this thesis, we study and evaluate different ways to effectively recognise, model and efficiently exploit useful structures hidden in realistic problems. A summary of the main contributions is as follows: 1. We first investigate an off-line processing phase that applies resolution-based pre-processors to input formulas before running SLS solvers on these problems. We report an extensive empirical examination of the impact of SAT pre-processing on the performance of contemporary SLS techniques. It emerges that while all the solvers examined do indeed benefit from pre-processing, the effects of different pre-processors are far from uniform across solvers and across problems. Our results suggest that SLS solvers need to be equipped with multiple pre-processors if they are ever to match the performance of systematic solvers on highly structured problems. [Part of this study was published at the AAAI-05 conference]. 2. We then look at potential approaches to bridging the gap between SAT and constraint satisfaction problem (CSP) formalisms. One approach has been to develop a many-valued SAT formalism (MV-SAT) as an intermediate paradigm between SAT and CSP, and then to translate existing highly efficient SAT solvers to the MV-SAT domain. In this study, we follow a different route, developing SAT solvers that can automatically recognise CSP structure hidden in SAT encodings. This allows us to look more closely at how constraint weighting can be implemented in the SAT and CSP domains. Our experimental results show that a SAT-based mechanism to handle weights, together with a CSP-based method to instantiate variables, is superior to other combinations of SAT and CSP-based approaches. In addition, SLS solvers based on this many-valued weighting approach outperform other existing approaches to handle many-valued CSP structures. [Part of this study was published at the AAAI-05 conference]. 3. Finally, we propose and evaluate six different schemes to encode temporal reasoning problems, in particular the Interval Algebra (IA) networks, into SAT CNF formulas. We then empirically examine the performance of local search as well as systematic solvers on the new temporal SAT representations, in comparison with solvers that operate on native IA representations. Our empirical results show that zChaff (a state-of-the-art complete SAT solver) together with the best IA-to-SAT encoding scheme, can solve temporal problems significantly faster than existing IA solvers working on the equivalent native IA networks. [Part of this study was published at the CP-05 workshop].

Reasoning about temporal and spatial information is a common task in computer science, especially in the field of artificial intelligence. The topic of this thesis is the study of such reasoning from a computational perspective. We study a number of different qualitative point based formalisms for temporal reasoning and provide a complete classification of computational tractability for different time models. We also develop more general methods which can be used for proving tractability and intractability of other relational algebras. Even though most of the thesis pertains to qualitative reasoning the methods employed here can also be used for quantitative reasoning. For instance, we introduce a tractable and useful extension to the quantitative point based formalism STP. This extension gives the algebra an expressibility which subsumes the largest tractable fragment of the augmented interval algebra and has a faster and simpler algorithm for deciding consistency. The use of disjunctions in temporal formalisms is of great interest not only since disjunctions are a key element in different logics but also since the expressibility can be greatly enhanced in this way. If we allow arbitrary disjunctions, the problems under consideration typically become intractable and methods to identify tractable fragments of disjunctive formalisms are therefore useful. One such method is to use the independence property. We present an automatic method for deciding this property for many relational algebras. Furthermore, we show how this concept can not only be used for deciding tractability of sets of relations but also to demonstrate intractability of relations not having this property. Together with other methods for making total classifications of tractability this goes a long way towards easing the task of classifying and understanding relational algebras. The tractable fragments of relational algebras are sometimes not expressive enough to model real-world problems and a backtracking solver is needed. For these cases we identify another property among relations which can be used to aid general backtracking based solvers to finnd solutions faster. / Article I is a revised and extended version of the following three papers: 1. Mathias Broxvall and Peter Jonsson. Towards a Complete Classification of Tractability in Point Algebras for Nonlinear Time. In Proceedings of the 5th International Conference on Principles and Practice of Constraint Programming (CP-99), pp. 129-143, Alexandria, VA, USA, Oct, 1999. 2. Mathias Broxvall and Peter Jonsson. Disjunctive Temporal Reasoning in Partially Ordered Time Structures. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-2000), pp. 464-469, Austin, Texas, USA, Aug, 2000. 3. Mathias Broxvall. The Point Algebra for Branching Time Revisited. In Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001), pp. 106-121, Vienna, Austria, Sep, 2001. --- Article II is a revised and extended version of the following paper: Mathias Broxvall, Peter Jonsson and Jochen Renz: Refinements and Independence: A Simple Method for Identifying Tractable Disjunctive Constraints. In Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP-2000), pp. 114-127, Singapore, Sep, 2000.

Description Logics (DLs) are a family of logic-based knowledge representation (KR) formalisms designed to represent and reason about static conceptual knowledge in a semantically well-understood way. On the other hand, standard action formalisms are KR formalisms based on classical logic designed to model and reason about dynamic systems. The largest part of the present work is dedicated to integrating DLs with action formalisms, with the main goal of obtaining decidable action formalisms with an expressiveness significantly beyond propositional. To this end, we offer DL-tailored solutions to the frame and ramification problem. One of the main technical results is that standard reasoning problems about actions (executability and projection), as well as the plan existence problem are decidable if one restricts the logic for describing action pre- and post-conditions and the state of the world to decidable Description Logics. A smaller part of the work is related to decidable extensions of Description Logics with concrete datatypes, most importantly with those allowing to refer to the notions of space and time.

Description Logics (DLs) form a family of knowledge representation formalisms which can be used to represent and reason with conceptual knowledge about a domain of interest. The knowledge represented by DLs is mainly static. In many applications, the domain knowledge is dynamic. This observation motivates the research on how to update the knowledge when changes in the application domain take place. This thesis is dedicated to the study of updating knowledge, more precisely, assertional knowledge represented in DLs. We explore whether the updated knowledge can be expressed in several standard DLs and, if so, whether it is computable and what is its size.

[Truncated abstract] In this thesis, I address the modelling and computer simulation of spatial, eventdriven systems from a computer science perspective. Spatially explicit models of wildland fire (wildfire) behaviour are addressed as the specific application domain. Wildfire behaviour is expressed as a formal model and the associated simulations are compared to existing models and implementations. It is shown that the in- teracting spatial automata formalism provides a general framework for modelling spatial event-driven systems and is appropriate to wildfire systems. The challenge adressed is that of physically realistic modelling of wildfire behaviour in heterogeneous environments . . . Many current models do not incorporate the influence of a neighbourhood (the geometry of the fire front local to an unburnt volume of fuel, for example), but rather determine the propagation of fire using only point information. Whilst neighbourhood-based influence of behaviour is common to cellular automata theory, its use is very rare in existing models of wildfire models. In this thesis, I present the modelling technique and demonstrate its applicability to wildfire systems via a series of simulation experiments, where I reproduce known spatial wildfire dynamics. I conclude that the interacting spatial automata formalism is appropriate as a basis for constructing new computer simulations of wildfire spread behaviour. Simulation results are compared to existing implementations, highlighting the limitations of current models and demonstrating that the new models are capable of greater physical realism.

Description Logics (DLs) form a family of knowledge representation formalisms which can be used to represent and reason with conceptual knowledge about a domain of interest. The knowledge represented by DLs is mainly static. In many applications, the domain knowledge is dynamic. This observation motivates the research on how to update the knowledge when changes in the application domain take place. This thesis is dedicated to the study of updating knowledge, more precisely, assertional knowledge represented in DLs. We explore whether the updated knowledge can be expressed in several standard DLs and, if so, whether it is computable and what is its size.

In this licentiate thesis, I present detailed case studies of students as they make use of simulated digital learning environments to engage with physics phenomena. In doing so, I reveal the moment-to-moment minutiae of physics students’ open-ended inquiry in the presence of two digital tools, namely the sandbox software Algodoo and the PhET simulation My Solar System (both running on an interactive whiteboard). As this is a topic which has yet to receive significant attention in the physics education research community, I employ an interpretivist, case-oriented methodology to illustrate, build, and refine several theoretical perspectives. Notably, I combine the notion of semi-formalisms with the notion of Newtonian modeling, I illustrate how Algodoo can be seen to function as a Papertian microworld, I meaningfully combine the theoretical perspectives of social semiotics and embodied cognition into a single analytic lens, and I reveal the need for a more nuanced taxonomy of students’ embodiment during physics learning activities. Each of the case studies presented in this thesis makes use of conversation analysis in a fine-grained examination of video-recorded, small-group student interactions. Of particular importance to this process is my attention to students’ non-verbal communication via gestures, gaze, body position, haptic-touch, and interactions with the environment. In this way, I bring into focus the multimodally-rich, often informal interactions of students as they deal with physics content. I make visible the ways in which the students (1) make the conceptual connection between the physical world and the formal/mathematical domain of disciplinary physics, (2) make informal and creative use of mathematical representations, and (3) incorporate their bodies to mechanistically reason about physical phenomena. Across each of the cases presented in this thesis, I show how, while using open-ended software on an interactive whiteboard, students can communicate and reason about physics phenomena in unexpectedly fruitful ways.