S. Safra
M. Y. Vardi
ABSTRACT
We study here the use of different representation for infinitary regular languages in extended temporal logic. We focus on three different kinds of acceptance conditions for finite automata on infinite words, due to Büchi, Streett, and Emerson and Lei (EL), and we study their computational properties. Our finding is that Büchi, Streett, and EL automata span a spectrum of succinctness. EL automata are exponentially more succinct than Büchi automata, and complementation of EL automata is doubly exponential. Streett automata are of intermediate complexity. While translating from Streett automata to Büchi automata involves an exponential blow-up, so does the translation from EL automata to Streett automata. Furthermore, even though Streett automata are exponentially more succinct than Büchi automata, complementation of Streett automata is only exponential. As a result, we show that the decision problem for ETLEL, where temporal connectives are represented by EL automata, is EXPSPACE-complete, and the decision problem for ETLS, where temporal connectives are represented by Streett automata, is PSPACE-complete.
- AS85.Alpern, B., Schneider, F.B.: Verifyin.q temporal properties withovt usin# temporal logic. TechnicM Report TR- 85-723, Cornell University, Dec. 1985. Google Scholar
Digital Library
- AS87.Alpern, B., Schneider, F.B.: Proving Boolean combinations of deterministic properties. Proc. Pad IEEE .qg, mp. on Logic in Computer Science, Ithaca, 1987, pp. 131137.Google Scholar
- Bu62.Buchi, J.R.: On a decision method in restricted sccond-ordcr arithnletics. Proc. {nt 'l Uongr. on Lo~ic, flf ethod. and Phil of Sci. 1960, Stanford UniversiLy Press, 1962, pp. 1-12.Google Scholar
- Ch74.Choueka, Y.: Theories of auLomata on w-tapes- a simplified approach. J. Computer and System. Sciev ,'~ 8(1074), pp. 117-141. Google ScholarDigital Library
- CY88.Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finitestate probabilistic programs. Proc. 29th IEEE Syrup. on Foundation of Computer Science, Oct. 1988, pp. 338- 345.Google Scholar
- EL87.Emerson, E.A., C.L. Lci: Modalities for model checking- branch;ng time strikes back.Google Scholar
- E89.Emerson, E.A.: Tcmporal and Modal Logic. Handbook of Theoretical Uompurer Science, eds. J. van Lccuwen et. ai., North-llolland Pub., ill press, 1989.Google Scholar
- FK84.Francez, N., Kozen, D.: Generalized fair termination. Froc. i lth A CM Syrup. on Principle~ o} Programming Languages, Salt Lake 'City, 1984. Google ScholarDigital Library
- Fr86.Francez, N.: Fairness. Text and Monographs ill Computer Science, Springer-Verlag, 1986. Google ScholarDigital Library
- Ga87.Galton, A.: 'Temporal logics and their applications. Academic Press, 1987. Google ScholarDigital Library
- HR83.Halpern, J.Y., Relf, J.H.: The propositional dynamic logic of deterministic well-structured programs. Theoretical Computer Science 27(1983), pp. 127- 165.Google ScholarCross Ref
- Kr87.KrSger, iv.: Temporal lo~ics o} programs. EATCS Monographs on Theoretical Computer Science, Springer- Verlag, 1987.Google Scholar
- LPZ85.Lichtenstein, O., Pnueli, A., Zuck L.: The glory of the past. Proc. Workshop on Logics of Programs, Brooklyn, Springer-Verlag, Lecture Notes in Computer Science 193, 1985, pp. 97- 107. Google ScholarDigital Library
- Mc66.McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9(1966), pp. 521-530.Google ScholarCross Ref
- Mi88.Michel, M.: Complementation is more difficult with automata on infinite words. Manuscript, 1988.Google Scholar
- MP87.Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by V-automata. Proc. I~ A CM Syrup. on Principles o.{ Pro#ramming LanffuatTes, Munich, Jan. 1987, pp. 1- 12. Google ScholarDigital Library
- Pa81.Park, D.: Concurrency and automata on infinite sequences. Proc. 5th GI Conf. on Theoretical Computer Science, 1981, Springer-Vcrlag, LNCS 104, pp. 167-183. Google ScholarDigital Library
- Pn77.Pnueli, A.: The temporal logic of programs. Proc. t Sth Syrup. on Foundations of Computer Science, 1977, pp. 46-57.Google ScholarDigital Library
- Pn85.Pnueli, A: In transition from global to modular reasoning about programs. Logics and Models oJ Concurrent Systems, ed. K.R. Apt, Springer-Verlag, 1985, pp. 123-144. Google ScholarDigital Library
- Pn86.Pnueli, A: Applications of temporal logic to the specification and verification of reactive systems - a survey of current trends. Current Trends in Cot~currency, eds. J.W. de Bakker et al., Springer-Verlag, Lecture Notes in Computer Science 224, 1986, pp. 510- 584. Google ScholarDigital Library
- Ra69.Rabin, M.O.: Decidability of secondorder theories and automata on infinite trees. Trans. AMS 141(1969), pp. 1-35.Google Scholar
- Sa88.Safra, S.: On the complexity of wautomata. Proc. ~gth IEEE .qymp. on Foundation o} Computer Science, Oct. 1988, pp. 319-327.Google Scholar
- SC85.Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporay logics. J. A CM 32(1985), pp. 733- 749. Google ScholarDigital Library
- St82.Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. In. formation and Control, 54(1982), pp. 121_1.11.Google Scholar
- SVW87.Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B;ichl automata with applications to temporal logic. Theoretical Computer Science 49(1987), pp. 217-237. Google ScholarDigital Library
- To81.Thomas, W.: A combinatorial approach to the theory of w-automata. Information and Control48( 1981 ), pp. 261-283.Google Scholar
- Va85.Vardi, M.Y.' Automatic verification of probabilistic concurrent finite-state programs. Proc. ~6th IEEE Syrnp. on Foundations oJ Computer Science, Portland, 1985, pp. 327-338.Google ScholarDigital Library
- Va87.Vard;, M.Y.: Verification of concurrent programs-- the automatatheoretic framework. Proc. 2nd IEEE Syrup. on Logic in Computer Science, Ithaca, 1987, pp. 167-176.Google Scholar
- VW85.Vardi, M.Y., Wolper, P.: Applications of temporal logic - an automate{- theoretlc perspective. Stanford University, CSLI, 1985.Google Scholar
- VW86.Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. Proc. IEEE Syrup. on Logic in Computer Science, Cambridge, 1986, pp. 332- 344.Google Scholar
- VW88.Vardi, M.Y., Wolper, P.: Reasoning about infinite computation paths. IBM Research Report RJ 6209, April 1988.Google Scholar
- Wo83.Wolper, P.: Temporal logic can be more expressive, lnJormation and Control 56(1983), pp. 72-99.Google Scholar
- WVS83.Wolper, P.L., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. Proc. ~dlh IEEE Syrup. on Foundation o} Computer Science, Tuscon, 1983, pp. 185-194.Google ScholarDigital Library
Index Terms
- On Ω-automata and temporal logic
Recommendations
A Unified Translation of Linear Temporal Logic to ω-Automata
We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). The translations yield automata of asymptotically ...
On the complexity of omega -automata
SFCS '88: Proceedings of the 29th Annual Symposium on Foundations of Computer ScienceAutomata on infinite words were introduced by J.R. Buchi (1962) in order to give a decision procedure for S1S, the monadic second-order theory of one successor. D.E. Muller (1963) suggested deterministic omega -automata as a means of describing the ...
Logic for ω-pushdown automata
AbstractContext-free languages of infinite words have recently found increasing interest. Here, we will present a second-order logic with the same expressive power as Büchi or Muller pushdown automata for infinite words. This extends ...
Comments