×

Decidability for a temporal logic used in discrete-event system analysis. (English) Zbl 0719.93005

Summary: 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 \(\Psi\), will determine in a finite number of steps whether or not \(\Psi\) 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 the authors’ work, “Decidability for temporal logic in control theory”, Proc. 25th Ann. Allerton Conf. Commun. Control Comput., Monticello/Illin. 1987, 335-444 (Urbana-Champaign/Illin. 1987).

MSC:

93A99 General systems theory
93C55 Discrete-time control/observation systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Buchi J. R., Proceedings of the 1960 International Congress of Logic, Methodology, and Philosophy of Science pp 1– (1962)
[2] Fusaoka A., Proceedings of the 8th International Conference on Artifical Intelligence 1 pp 405– (1983)
[3] Galton A., Temporal Logics and Their Applications (1987) · Zbl 0683.68003
[4] Knight J. F., Proceedings of the Twenty-Fifth Allerton Conference on Communication, Control, and Computing pp 335– (1987)
[5] Manna , Z. , and Pnueli , A. , 1983 , Verification of concurrent programs: a temporal proof system. Report no. STAN-CS-83–967, Department of Computer Science, Stanford University. · Zbl 0507.68005
[6] Manna , A. , and Wolper , P. , Synthesis of communicating processes from temporal logic specifications. Report no. STAN-CS-81–872, Department of Computer Science, 1981 , Stanford University. · Zbl 0522.68030
[7] Ostroff J. S., Ph.D. dissertation (1987)
[8] Ostroff J. S., Proceedings of the 24th Conference on Decision and Control pp 656– (1985)
[9] Passino K. M., Proceedings of the Twenty-Sixth Allerton Conference on Communication, Control, and Computing pp 1160– (1988)
[10] DOI: 10.1137/0325013 · Zbl 0618.93033 · doi:10.1137/0325013
[11] DOI: 10.1080/00207178608933645 · Zbl 0606.93002 · doi:10.1080/00207178608933645
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.