# zbMATH — the first resource for mathematics

Expressiveness of propositional projection temporal logic with star. (English) Zbl 1221.03018
Summary: This paper investigates the expressiveness of propositional projection temporal logic with star (PPTL$$^*$$). To this end, Büchi automata and $$\omega$$-regular expressions are first extended as stutter Büchi automata (SBA) and extended regular expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL$$^*$$ formulas, SBAs and EREs, PPTL$$^*$$ is proved to represent exactly the full regular language. Moreover, some fragments of PPTL$$^*$$ are characterized and, finally, PPTL$$^*$$ and its fragments are classified into five different language classes.

##### MSC:
 03B44 Temporal logic 03C05 Equational classes, universal algebra in model theory 68Q45 Formal languages and automata 68Q60 Specification and verification (program logics, model checking, etc.)
SPIN
Full Text:
##### References:
 [1] Pnueli, A., The temporal logic of programs, (), pp. 46-67.2 [2] Kripke, S.A., Semantical analysis of modal logic I: normal propositional calculi, Zeitschrift fur mathematische logik und grundlagen der Mathematik, 9, 67-96, (1963) · Zbl 0118.01305 [3] R. Rosner, A. Pnueli, A choppy logic, in: First Annual IEEE Symposium on Logic in Computer Science, LICS, 1986, pp. 306-314. [4] B. Moszkowski, Reasoning about digital circuits. Ph.D. Thesis, Department of Computer Science, Stanford University. TRSTAN-CS-83-970, 1983. [5] B. Moszkowski, Compositional reasoning about projected and infinite time, iceccs, in: First IEEE International Conference on Engineering of Complex Computer Systems, ICECCS’95, 1995, p. 238. [6] Z. Duan, An extended interval temporal logic and a framing technique for temporal logic programming, Ph.D. Thesis, University of Newcastle upon Tyne, May 1996. [7] Duan, Z.; Yang, X.; Kounty, M., Framed temporal logic programming, Science of computer programming, 70, 1, 31-61, (2008) · Zbl 1131.68036 [8] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic with infinite models, Acta informatica, 45, 1, 43-78, (2008) · Zbl 1141.68039 [9] Tian, Cong; Duan, Zhenhua, Alternating interval based temporal logics, (), 694-709 [10] Tian, C.; Duan, Z., Model checking propositional projection temporal logic based on SPIN, () [11] Wolper, P.L., Temporal logic can be more expressive, Information and control, 56, 72-99, (1983) · Zbl 0534.03009 [12] Holzmann, Gerard J., The model checker spin, IEEE transactions on software engineering, 23, 5, 279-295, (1997) [13] Arden, D., Delayed-logic and finite-state machines, (), 1-35 [14] Gabbay, Dov; Pnueli, Amir; Shelah, Saharon; Stavi, Jonathan, On the temporal analysis of fairness, (), 163-173 [15] Aravinda Prasad Sistla, Theoretical issues in the design and verification of distributed systems, Ph.D. Thesis, Harvard University, 1983. · Zbl 0519.68049 [16] Vardi, M.Y.; Wolper, P., Yet another process logic, (), 501-512 · Zbl 0549.68020 [17] Moshe Y. Vardi, A temporal fixpoint calculus, in: POPL’88, 1988, pp. 250-259. [18] McNaughton, Robert; Papert, Seymour A., () [19] H. Barringer, R. Kuiper, A. Pnueli, Now you may compose temporal logic specifications, in: Proc. 16th STOC, 1984, pp. 51-63. [20] H. Barringer, R. Kuiper, A. Pnueli, The compositional temporal approach to CSP-like language, in: Proc. IFIP Conference, The Role of Abstract Models in Information Processing, January 1985. · Zbl 0594.68018 [21] Nguyen, V.; Demers, A.; Gries, D.; Owicki, S., Behavior: A temporal approach to process modeling, (), 237-254 [22] V. Nguyen, D. Gries, S. Owicki, A model and temporal proof system for networks of processes, in: Proc. 12th POPL, 1985, pp. 121-131. [23] Emerson, E.A., Temporal and modal logic, (), 997-1072, (Chapter 16) · Zbl 0900.03030 [24] Thomas, W., Automata on infinite objects, (), 133-191 · Zbl 0900.68316 [25] H. Kamp, Tense logic and the theory of linear order. Ph.D. Thesis, UCLA, 1968. [26] McNaughton, R.; Papert, S., Counter-free automata, (1971), The MIT Press · Zbl 0232.94024 [27] Milner, Robin, Communicating and mobile system: the-calculus, (1999), Cambridge University Press Cambridge · Zbl 0942.68002 [28] L. Stockmeyer, The complexity of decision problems in automata theory and logic, Ph.D. Thesis, MIT, available as Project MAC Technical Report 133, 1974. [29] Tian, Cong; Duan, Zhenhua, Complexity of propositional projection temporal logic with star, (), 73-100 · Zbl 1161.03008
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.