Abstract
A key issue in the design of a model-checking tool is the choice of the formal language with which properties are specified. It is now recognized that a good language should extend linear temporal logic with the ability to specify all ω-regular properties. Also, designers, who are familiar with finite-state machines, prefer extensions based on automata than these based on fixed points or propositional quantification. Early extensions of linear temporal logic with automata use nondeterministic Büchi automata. Their drawback has been inability to refer to the past and the asymmetrical structure of nondeterministic automata. In this work we study an extension of linear temporal logic, called ETL2a, that uses two-way alternating automata as temporal connectives. Twoway automata can traverse the input word back and forth and they are exponentially more succinct than one-way automata. Alternating automata combine existential and universal branching and they are exponentially more succinct than nondeterministic automata. The rich structure of two-way alternating automata makes ETL2a a very powerful and convenient logic. We show that ETL2a formulas can be translated to nondeterministic Büchi automata with an exponential blow up. It follows that the satisfiability and model-checking problems for ETL2a are PSPACE-complete, as are the ones for LTL and its earlier extensions with automata. So, in spite of the succinctness of two-way and alternating automata, the advantages of ETL2a are obtained without a major increase in space complexity. The recent acceptance of alternating automata by the industry and the development of symbolic procedures for handling them make us optimistic about the practicality of ETL2a.
Supported in part by BSF grant 9800096.
Supported in part by NSF grant CCR-9700061, NSF grant CCR-9988322, BSF grant 9800096, and by a grant from the Intel Corporation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Armoni, L. Fix, A. Flaisher, R. Gerth, T. Kanza, A. Landver, S. Mador Haim, A. Tiemeyer, M.Y. Vardi, and Y. Zber. The ForSpec compiler. Submitted, 2001.
R. Armoni, L. Fix, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador Haim, A. Tiemeyer, E. Singerman, and M.Y. Vardi. The ForSpec temporal logic: A new temporal property-specification logic. Submitted, 2001.
B. Banieqbal and H. Barringer. Temporal logic with fixed points. In Temporal Logic in Specification, LNCS 398, 62–74. Springer-Verlag, 1987.
I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In 6th CAV, LNCS 818, 182–193, Springer-Verlag, 1994.
I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of RCTL formulas. In 10th CAV, LNCS 1427, 184–194. Springer-Verlag, 1998.
J.C. Birget. State-complexity of finite-state devices, state compressibility and incompressibility. Mathematical Systems Theory, 26(3):237–269, 1993.
H. Barringer and R. Kuiper. Hierarchical development of concurrent systems in a framework. In Seminar in Concurrency, LNCS 197, 35–61. Springer-Verlag, 1985.
J.A. Brzozowski and E. Leiss. Finite automata and sequential networks. TCS, 10:19–35, 1980.
E.M. Clarke, O. Grumberg, and R.P. Kurshan. A synthesis of two approaches for verifying finite state concurrent systes. Logic and Computation, 2(5):605–618, 1992.
E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114–133, January 1981.
D. Drusinsky and D. Harel. On the power of bounded concurrency I: Finite automata. Journal of the ACM, 41(3):517–539, 1994.
E.A. Emerson and R.J. Trefler. Generalized quantitative temporal reasoning: An automata theoretic approach. In TAPSOFT, LNCS 1214, 189–200. Springer, 1997.
B. Finkbeiner. Symbolic refinement checking with nondeterministic BDDs. In TACAS, LNCS 2031. Springer-Verlag, 2001.
N. Francez. Program verification. Int. Computer Science. Addison-Weflay, 1992.
D. Gabbay. The declarative past and imperative future. In Temporal Logic in Specification, LNCS 398, 407–448. Springer-Verlag, 1987.
N. Globerman and D. Harel. Complexity results for two-way and multipebble automata and their logics. TCS, 143:161–184, 1996.
J.G. Henriksen and P.S. Thiagarajan. Dynamic linear time temporal logic. Annals of Pure and Applied Logic, 96(1–3):187–207, 1999.
O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak. In 5th ISTCS, 147–158. IEEE Computer Society Press, 1997.
O. Kupferman and M.Y. Vardi. μ-calculus synthesis. In 25th MFCS, LNCS 1893, 497–507. Springer-Verlag, 2000.
O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, LNCS 193, 196–218, Springer-Verlag, 1985.
A. R. Meyer. Weak monadic second order theory of successor is not elementary recursive. In Proc. Logic Colloquium, Vol. 453 of Lecture Notes in Mathematics, 132–154. Springer-Verlag, 1975.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992.
D.E. Muller and P.E. Schupp. The theory of ends, pushdown automata, and second-order logic. TCS, 37:51–75, 1985.
D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. TCS, 54:267–276, 1987.
D.E. Muller and P.E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. TCS, 141:69–107, 1995.
D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In 13th IC ALP, LNCS 226, 1986.
N. Piterman. Extending temporal logic with ω-automata. M.Sc. Thesis, The Weizmann Institute of Science, Israel, 2000, http://www.wisdom.weizmann.ac.il/home/nirp/public_html/publications/msc_thesis.ps.
A. Pnueli. The temporal semantics of concurrent programs. TCS, 13:45–60, 1981.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123–144. Springer-Verlag, 1985.
A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733–749, 1985.
A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. TCS, 49:217–237, 1987.
W. Thomas. A combinatorial approach to the theory of ω-automata. Information and Computation, 48:261–283, 1981.
M.Y. Vardi. A temporal fixpoint calculus. In 15th POPL, pages 250–259, 1988.
M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, 238–266, 1996.
M.Y. Vardi. Reasoning about the past with two-way automata. In 25th ICALP LNCS 1443, 628–641. Springer-Verlag, 1998.
M.Y. Vardi and P. Wolper. Yet another process logic. In Logics of Programs, LNCS 164, 501–512. Springer-Verlag, 1984.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, November 1994.
P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1–2):72–99, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Piterman, N., Vardi, M.Y. (2001). Extended Temporal Logic Revisited. In: Larsen, K.G., Nielsen, M. (eds) CONCUR 2001 — Concurrency Theory. CONCUR 2001. Lecture Notes in Computer Science, vol 2154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44685-0_35
Download citation
DOI: https://doi.org/10.1007/3-540-44685-0_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42497-0
Online ISBN: 978-3-540-44685-9
eBook Packages: Springer Book Archive