Decidability for a temporal logic used in discrete-event system analysis

Abstract

The type of plant considered is one that can be modelled by a non-deterministic finite state machine P. The regulator is a deterministic finite state machine R. The closed loop system is formed by connecting P and R in a 'regulator configuration'. Formulae in a propositional temporal language are used to describe the behaviour of the closed-loop system. It is shown that there is a mechanical procedure which, for a given P and R, and a temporal formula Ψ, will determine in a finite number of steps whether or not Ψ must be true. This ‘decidability’ result could be proven using other known results on temporal logic. The proof given here shows that the behaviour of the closed-loop system may safely be assumed to be ultimately periodic. Formulae of a given complexity, say n, will be true in all possible 'runs' of the system just in case they are true in all ultimately periodic runs, with the period and the onset of periodicity bounded by a certain function of n. A ‘synthesis’ result follows immediately from the decidability result. The interpretation of time is discussed at some length. The results are illustrated on two discrete-event system examples. This paper is an expanded version of Knight and Passino (1987).