Executable Modal and Temporal Logics

In recent years a number of programming languages based upon the direct execution of either modal or temporal logic formulae have been developed. This use of non-classical logics provides a powerful basis for the representation and implementation of a range of dynamic behaviours. Though many of these languages are still experimental, they are beginning to be applied, not only in Computer Science and AI, but also in less obvious areas such as process control and social modelling.

This paper provides an introduction to some of the basic concepts of executable modal and temporal logics.

Temporal logic allows us to use logic programming to specify and to program dynamically changing situations and non-terminating computations in a natural and problem oriented way. Recently so called metric or real-time temporal logics have been proposed for the specification of real-time systems, for which not only qualitative but also quantitative temporal properties are very important. In this work we investigate a subset of metric temporal Horn logic called MTL-programs, for which we give a translation into CLP(A′)-programs and CLP(A′)-goals over a suitable algebra A′. We give a restriction of the CLP(A′)-derivation mechanism sufficient for the derivation of MTL-goals from MTL-programs, which admits efficient satisfiability checking of the constraints generated. Its worst case complexity is linear in the number of variables involved, contrary to general satisfiability checking of constraints over A′ which is NP-complete. Moreover, we show that an extension of the metric temporal logic considered by the inclusion of variables within the temporal operators leads already to a temporal Horn logic which is expressively equivalent to constraint logic programs over A′.

We have developed Tokio interpreter[5] for first order Interval Temporal Logic[11] and an automatic theorem prover [6,7] for Propositional Interval Temporal Logic. The verifier features deterministic tableau expansion and binary decision tree representation of subterms. Combining these, we can avoid repeated similar clausal form time constraints, and it is possible to execute wider range of specifications without time-backtracking.

We introduce a family of logic programming languages for representing and reasoning about time. The family is conceptually simple while covering substantial parts of temporal logic. Given a logic in our framework, there is a systematic way to make it executable as a constraint logic program. Thus we can study and compare various temporal logics and their executable fragments. Our approach allows for different models of time, different temporal operators, and temporal variables for both time points and time periods. Formulas can be labeled with temporal information using annotations. In this way we avoid the proliferation of variables and quantifiers as encountered in first order approaches. Unlike temporal logic, both qualitative and quantitative (metric) temporal reasoning with time points (instants) and periods (temporal intervals) are supported. A Horn clause fragment of our temporal logic can be seen as annotated constraint logic programming language. This class of languages can be implemented by translation into a standard constraint programming language. Thus we can make our temporal logic executable.

This paper is a companion paper to [Fru94c], where an interpreter for annotated languages and their underlying logic is described.

Concurrent MetateM is a programming language based on the notion of concurrent, communicating objects, where each object directly executes a specification given in temporal logic, and communicates with other objects using asynchronous broadcast message-passing. Thus, Concurrent MetateM represents a combination of the direct execution of temporal specifications, together with a novel model of concurrent computation. In contrast to the notions of predicates as processes and stream parallelism seen in concurrent logic languages, Concurrent MetateM represents a more coarse-grained approach, where an object consists of a set of logical rales and communication is achieved by the evaluation of certain types of predicate. Representing concurrent systems as groups of such objects provides a powerful tool for modelling complex reactive systems. Being based upon executable temporal logic, objects in isolation have an intuitive semantics. However, the addition of both operational constraints upon the object's execution and global constraints provided by the model of concurrency and communication, complicates the overall semantics of networks of objects. It is this, more complex, semantics that we address here, where a basis for the full semantics of Concurrent MetateM is provided.

We describe reasoning methods for the interval-based modal temporal logic LLP which employs the modal operators sometimes, always, next, and chop. We propose a constraint deduction approach and compare it with a sequent calculus, developed as the basic machinery for the deductive planning system PHI which uses LLP as underlying formalism.

In [27] we applied the MetateM executable temporal logic programming language in a distributed system guise to a case study of a hospital patient monitoring system. The purpose was to test MetateM as a framework in which to implement prototypes for developing specifications of complex reactive systems. We demonstrated that it is indeed a very useful tool in such situations and that the framework has promising potential for further development. In this paper, we summarize the lessons which were learnt for future developments paying particular attention to those aspects concerned with using full firstorder temporal logic as the underlying language.

We present here an executable modal logic based system: PW-XRete 1. This system is connected with the modal logic through the Kripke's possible worlds semantics. PW-XRete presents a procedure of labeling the worlds that provides an efficient implementation of the possible worlds and, as it showed, is well suited for nonmonotonic reasoning.

This paper discusses the results of a study for representation of law. Starting point is a legal knowledge based system for the Dutch traffic law that treats permissions as specialized obligations. The results of this prototype system have been evaluated and were the subject for further study. The second half of this paper looks into computationally attractive formalisms that capture deontic modalities more naturally.