Abstract
We present regular linear temporal logic (RLTL), a logic that generalizes linear temporal logic with the ability to use regular expressions arbitrarily as sub-expressions. Every LTL operator can be defined as a context in regular linear temporal logic. This implies that there is a (linear) translation from LTL to RLTL.
Unlike LTL, regular linear temporal logic can define all ω-regular languages, while still keeping the satisfiability problem in PSPACE. Unlike the extended temporal logics \(\text{ETL}_*\), RLTL is defined with an algebraic signature. In contrast to the linear time μ-calculus, RLTL does not depend on fix-points in its syntax.
Part of this work was done during the first author’s stay at Stanford University and was supported by ARO DAAD190310197. The second author has been supported in part by NSF grants CCR-01-21403, CCR-02-20134, CCR-02-09237, CNS-0411363, and CCF-0430102, and by NAVY/ONR contract N00014-03-1-0939.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
IEEE P1850 - Standard for PSL - Property Specification Language (September 2005)
Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL 1986. Procs. of the 13th Annual ACM Symp. on Principles of Programming Languages, pp. 173–183. ACM Press, New York (1986)
Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the Int’l Congress on Logic Methodology and Philosophy of Science, pp. 1–12. Stanford University Press (1962)
Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)
Fisman, D., Eisner, C., Havlicek, J.: Formal syntax and Semantics of PSL: Appendix B of Accellera Property Language Reference Manual, Version 1.1 (March 2004)
Harel, D., Peleg, D.: Process logic with regular formulas. Theoretical Computer Science 38, 307–322 (1985)
Henriksen, J.G., Thiagarajan, P.S.: Dynamic linear time temporal logic. Annals of Pure and Applied Logic 96(1-3), 187–207 (1999)
Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages and computation. Addison-Wesley, Reading (1979)
Hromkovic, J., Seibert, S., Wilke, T.: Translating regular expressions into small ε-free nondeterministic finite automata. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 55–66. Springer, Heidelberg (1997)
Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, vol. 34, pp. 3–41. Princeton University Press, Princeton, New Jersey (1956)
Kozen, D.: Results on the propositional μ-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages, and Programming. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: ISTCS 1997. Proc. of the Fifth Israel Symposium on Theory of Computing and Systems, pp. 147–158. IEEE Computer Society Press, Los Alamitos (1997)
Lange, M.: Weak automata for the linear time μ-calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 267–281. Springer, Heidelberg (2005)
Lange, M., Stirling, C.: Model checking fixed point logic with chop. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol. 2303, Springer, Heidelberg (2002)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, Heidelberg (1995)
Muller, D.E., Schupp, P.E.: Altenating automata on infinite trees. Theoretical Computer Science 54, 267–276 (1987)
Müller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 510–520. Springer, Heidelberg (1999)
Pnueli, A.: The temporal logic of programs. In: FOCS 1977. Proc. of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–67. IEEE Computer Society Press, Los Alamitos (1977)
Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems – a survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510–584. Springer, Heidelberg (1986)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear termporal logics. Journal of the ACM 32(3), 733–749 (1985)
Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, Department of Electrical Engineering, MIT, Boston, Massachusetts (1974)
Vardi, M.Y.: Personal communication
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115, 1–37 (1994)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56, 72–99 (1983)
Yamamoto, H.: On the power of input-synchronized alternating finite automata. In: Du, D.-Z., Eades, P., Sharma, A.K., Lin, X., Estivill-Castro, V. (eds.) COCOON 2000. LNCS, vol. 1858, p. 457. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leucker, M., Sánchez, C. (2007). Regular Linear Temporal Logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2007. ICTAC 2007. Lecture Notes in Computer Science, vol 4711. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75292-9_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-75292-9_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75290-5
Online ISBN: 978-3-540-75292-9
eBook Packages: Computer ScienceComputer Science (R0)