Abstract
We propose an extension, called \( \mathcal{L}_p^ + , o \), of the temporal logic LTL, which enables talking about finitely many register values: the models are infinite words over tuples of integers (resp. real numbers). The formulas of \( \mathcal{L}_p^ + , o \) are flat: on the left of an until, only atomic formulas or LTL formulas are allowed. We prove, in the spirit of the correspondence between automata and temporal logics, that the models of a \( \mathcal{L}_p^ + , o \) formula are recognized by a piecewise flat counter machine; for each state q, at most one loop of the machine on q may modify the register values.
Emptiness of (piecewise). at counter machines is decidable (this follows from a result in [9]). It follows that satisfiability and model-checking the negation of a formula are decidable for \( \mathcal{L}_p^ + , o \). On the other hand, we show that inclusion is undecidable for such languages. This shows that validity and model-checking positive formulas are undecidable.
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
P. A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Proc. Computer Aided Veri.cation, volume 1427 of Lecture Notes in Computer Science, pages 305–18. Springer-Verlag, 1998.
R. Alur and D. Dill. Automata for modeling real-time systems. In Proc. 17th Int. Coll. on Automata, Languages and Programming, Warwick, LNCS 443, pages 322–35. Springer-Verlag, 1990.
R. Alur, K. Etessami, S. La Torre, and D. Peled. Parametric temporal logic for model measuring. In Proc. Int. Conf. on Automata, Languages and Programming (ICALP’99), volume 1644 of Lecture Notes in Computer Science, pages 159–68, Prague, 1999. Springer-Verlag.
A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In Tenth Annual IEEE Symposium on Logic in Computer Science, pages 123–133, 1995.
A. Bouajjani, R. Echahed, and P. Habermehl. Verifying infinite state processes with sequential and parallel composition. In Proc. POPL’95, pages 95–106, San Francisco, 1995.
A. Bouajjani, R. Echahed, and R. Robbana. Verification of nonregular temporal properties of context free processes. In Proc. CONCUR’94, volume 836 of Lecture Notes in Computer Science, pages 81–97. Springer-Verlag, 1994.
A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFO channel systems with non regular sets of configurations. In Proc. 24th Int. Coll. on Automata, Languages and Programming (ICALP), volume 1256 of Lecture Notes in Computer Science, 1997.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.
H. Comon and Y. Jurski. Multiple counters automata, safety analysis and presburger arithmetic. In A. Hu and M. Vardi, editors, Proc. Computer Aided Verification, volume 1427 of LNCS, pages 268–279, Vancouver, 1998. Springer-Verlag.
H. Comon and Y. Jurski. Counter automata, fixpoints and additive theories. Submitted to TCS. Available at http://www.lsv.enscachan.fr/~comon/ftp.articles/mca.ps.gz, 1999.
H. Comon and Y. Jurski. Timed automata and the theory of real numbers. In Proc. Conf. on Concurrency Theory (CONCUR), number 1664 in Lecture Notes in Computer Science, pages 242–257. Springer-Verlag, 1999.
D. R. Dams. Flat fragments of ctl and ctl*. Journal of the IGPL, 7(1):55–78, 1999.
E. Emerson and J. Y. Halpern. Sometimes and not never revisited. J. ACM, 33, 1986.
E. Emerson and R. Trefier. Parametric quantitative temporal reasoning. In Proc. IEEE Symp. on Logic in Computer Science, pages 336–343, Trento, 1999. IEEE Comp. Soc. Press.
J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems. Safety. Springer-Verlag, 1995.
M. Minsky. Computation, Finite and Infinite Machines. Prentice Hall, 1967.
A. Sistla and E. M. Clarke. The complexity of propositional linear temporal logic. J. ACM, 32:733–749, 1985.
M. Vardi. An automata-theoretic approach to linear time temporal logic. In Logic for concurrency: structure versus automata, volume 1043 of Lecture Notes in Computer Science. Springer Verlag, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Comon, H., Cortier, V. (2000). Flatness Is Not a Weakness. In: Clote, P.G., Schwichtenberg, H. (eds) Computer Science Logic. CSL 2000. Lecture Notes in Computer Science, vol 1862. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44622-2_17
Download citation
DOI: https://doi.org/10.1007/3-540-44622-2_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67895-3
Online ISBN: 978-3-540-44622-4
eBook Packages: Springer Book Archive