Abstract
We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on ω-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability problem for the logics working on ω k-sequences is expspace-complete when the integers are represented in binary, and pspace-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.
The first author acknowledges partial support by the ACI “Sécurité et Informatique” CORTOS. The second author acknowledges partial support by the e-Society project of MEXT. Part of this work was done while the second author was affiliated to LSV, CNRS & ENS de Cachan.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. Journal of the ACM 43, 116–146 (1996)
Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. TCS 303(1), 7–34 (2003)
Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 1–20. Springer, Heidelberg (1995)
Bedon, N.: Langages reconnaissables de mots indexés par des ordinaux. PhD thesis, Université Marne-la-Vallée (1998)
Bérard, B., Picaronny, C.: Accepting Zeno words: a way toward timed refinements. In: Privara, I., Ružička, P. (eds.) MFCS 1997. LNCS, vol. 1295, pp. 149–158. Springer, Heidelberg (1997)
Bès, A.: Decidability and definability results related to the elementary theory of ordinal multiplication. Fundamenta Mathematicae 171, 197–211 (2002)
Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed control with partial observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 180–192. Springer, Heidelberg (2003)
Bruyère, V., Carton, O.: Automata on linear orderings. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol. 2136, pp. 236–247. Springer, Heidelberg (2001)
Büchi, J.: Transfinite automata recursions and weak second order theory of ordinals. In: Int. Cong. Logic, Methodology and Philosophy of Science, Jerusalem, pp. 3–23 (1964)
Büchi, J., Siefkes, D.: The monadic second order theory of all countable ordinals. Lecture Notes in Mathematics, vol. 328. Springer, Heidelberg (1973)
Carton, O.: Accessibility in automata on scattered linear orderings. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 155–164. Springer, Heidelberg (2002)
Choffrut, C.: Elementary theory of ordinals with addition and left translation by ω. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 15–20. Springer, Heidelberg (2002)
Choueka, Y.: Finite automata, definable sets, and regular expressions over ω n-tapes. JCSS 17, 81–97 (1978)
Cuijpers, P., Reniers, M., Engels, A.: Beyond Zeno-behaviour. Technical report, TU of Eindhoven (2001)
Demri, S., Nowak, D.: Reasoning about transfinite sequences (May 2005) arXiv:cs.LO/0505073
Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. JCSS 18, 194–211 (1979)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980. ACM Press, New York (1980)
Godefroid, P., Wolper, P.: A partial approach to model checking. I&C 110(2), 305–326 (1994)
Hemmer, J., Wolper, P.: Ordinal finite automata and languages (extended abstract). Technical report, Université of Liège (1991)
Hirshfeld, Y., Rabinovich, A.: Logics for real time: decidability and complexity. Fundamenta Informaticae 62, 1–28 (2004)
Kamp, J.: Tense Logic and the theory of linear order. PhD thesis, UCLA, USA (1968).
Lutz, C., Walther, D., Wolter, F.: Quantitative temporal logics: PSPACE and below. In: TIME 2005 (2005) (to appear)
Maurin, F.: The theory of integer multiplication with order restricted to primes is decidable. The Journal of Symbolic Logic 62(1), 123–130 (1997)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th ACM POPL, Austin, Texas, pp. 179–190 (1989)
Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE 77, 81–98 (1989)
Reynolds, M.: The complexity of the temporal logic with until over general linear time. JCSS 66(2), 393–426 (2003)
Rohde, S.: Alternating Automata and The Temporal Logic of Ordinals. PhD thesis, University of Illinois (1997)
Vardi, M., Wolper, P.: Reasoning about infinite computations. I&C 115, 1–37 (1994)
Wojciechowski, J.: Classes of transfinite sequences accepted by nondeterministic finite automata. Annales Societatid Mathematicae Polonae, 191–223 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Demri, S., Nowak, D. (2005). Reasoning About Transfinite Sequences. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_20
Download citation
DOI: https://doi.org/10.1007/11562948_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)