The task of monitoring the execution of a software-based controller in order to detect, classify, and recover from discrepancies between the actual effects of control actions and the effects predicted by a model, is the topic of this thesis. Model-based execution monitoring is proposed as a technique for increasing the safety and optimality of operation of large and complex industrial process controllers, and of controllers operating in complex and unpredictable environments (such as unmanned aerial vehicles).

In this thesis we study various aspects of model-based execution monitoring, including the following:

The relation between previous approaches to execution monitoring in Control Theory, Artificial Intelligence and Computer Science is studied and a common conceptual framework for design and analysis is proposed.

An existing execution monitoring paradigm, ontological control, is generalized and extended. We also present a prototype implementation of ontological control with a first set of experimental results where the prototype is applied to an actual industrial process control system: The ABB STRESSOMETER cold mill flatness control system.

A second execution monitoring paradigm, stability-based execution monitoring, is introduced, inspired by the vast amount of work on the "stability" notion in Control Theory and Computer Science.

Finally, the two paradigms are applied in two different frameworks. First, in the "hybrid automata" framework, which is a state-of-the-art formal modeling framework for hybrid (that is, discrete+continuous) systems, and secondly, in the logical framework of GOLOG and the Situation Calculus. 

The goal of most agents is not just to reach a goal state, but rather also (or alternatively) to put restrictions on its trajectory, in terms of states it must avoid and goals that it must ‘maintain’. This is analogous to the notions of ‘safety’ and ‘stability’ in the discrete event systems and temporal logic community. In this paper we argue that the notion of ‘stability’ is too strong for formulating ‘maintenance’ goals of an agent – in particular, reactive and software agents, and give examples of such agents. We present a weaker notion of ‘maintainability’ and show that our agents which do not satisfy the stability criteria, do satisfy the weaker criteria. We give algorithms to test maintainability, and also to generate control for maintainability. We then develop the notion of ‘supportability’ that generalizes both ‘maintainability’ and ‘stabilizability, develop an automata theory that distinguishes between exogenous and control actions, and develop a temporal logic based on it.

The class of constraint satisfaction problems (CSPs) over finite domains has been shown to be NP-complete, but many tractable subclasses have been identified in the literature. In this paper we are interested in restrictions on the types of constraint relations in CSP instances. By a result of Jeavons et al. we know that a key to the complexity of classes arising from such restrictions is the closure properties of the sets of relations. It has been shown that sets of relations that are closed under constant, majority, affine, or associative, commutative, and idempotent (ACI) functions yield tractable subclasses of CSP. However, it has been unknown whether other closure properties may generate tractable subclasses. In this paper we introduce a class of tractable (in fact, SL-complete) CSPs based on bipartite graphs. We show that there are members of this class that are not closed under constant, majority, affine, or ACI functions, and that it, therefore, is incomparable with previously identified classes.

Although many formalisms for reasoning about action exist, surprisingly few approaches have taken computational complexity into consideration. The contributions of this article are the following: a temporal logic with a restriction for which deciding satisfiability is tractable, a tractable extension for reasoning about action, and NP-completeness results for the unrestricted problems. Many interesting reasoning problems can be modelled, involving nondeterminism, concurrency and memory of actions. The reasoning process is proved to be sound and complete. (C) 1999 Published by Elsevier Science B.V. All rights reserved.

The autonomy of an artificial agent (e.g. a robot) will certainly depend on its ability to perform "intelligent" tasks, such as learning, planning, and reasoning about its own actions and their effects on the enviroment, for example predicting the consequences of its own behaviour. To be able to perform these (and many more) tasks, the agent will have to represent its knowledge about the world.

The research field "Logics of Action Change" is concerned with the modelling of agents and dynamical, changing environments with logics.In this thesis we study two aspects of automation of logics of action and change. The first aspect, regression, is used to "reason backwards", i.e. to start with the last time point in a description of a course of events, and moving backwards through these events, taking the effects of all actions into consideration. We discuss the consequences for regression of introducing nondeterministic actions, and provide the logic PMON with pre- and postdiction procedures. We employ the classical computer science tool, the weakest liberal precondition operator (wlp) for this, and show that logical entailment of PMON is equivalent to wlp computations.

The second aspect is computational complexity of logics of action and change, which has virtually been neglected by the research community. We present a new and expressive logic, capable of expressing continuous time, nondeterministic actions, concurrency, and memory of actions. We show that satisfiability of a theory in this logic is NP-complete. Furthermore, we identify a tractable subset of the logic, and provide a sound, complete, and polynomial algorithm for satisfiability of the subset.