DECIDABILITY FOR A TEMPORAL LOGIC USED IN DISCRETE-EVENT SYSTEM-ANALYSIS

被引:13
作者
KNIGHT, JF [1 ]
PASSINO, KM [1 ]
机构
[1] UNIV NOTRE DAME,DEPT ELECT & COMP ENGN,NOTRE DAME,IN 46556
基金
美国国家科学基金会;
关键词
D O I
10.1080/00207179008953606
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
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 IJI, will determine in a finite number of steps whether or not IJI 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 perodic. Formulae of a given complexity, say II, 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). © 1990 Taylor and Francis Group, LLC.
引用
收藏
页码:1489 / 1506
页数:18
相关论文
共 12 条
  • [1] BUCHI JR, 1962, 1960 P INT C LOG MET, P1
  • [2] FUSAOKA A, 1983, 8TH P INT C ART INT, V1, P405
  • [3] GALTON A, 1987, TEMPORAL LOGICS THEI
  • [4] KNIGHT JF, 1987, 25TH P ALL C COMM CO, P335
  • [5] MANNA A, 1981, STANCS81872 STANF U
  • [6] MANNA Z, 1983, STANCS83967 STANF U
  • [7] OSTROFF JS, 1987, 8618 U TOR DEP EL EN
  • [8] OSTROFF JS, 1987, 26TH P IEEE C DEC CO, P681
  • [9] OSTROFF JS, 1985, 24TH P IEEE C DEC CO, P656
  • [10] PASSINO KM, 1988, 26TH P ALL C COMM CO, P1160