Abstract
The study of the decidability of the so-called sequential calculus S1S calls into play two techniques employing tools at the heart of Logic and Computer Science: Büchi automata on infinite words [1] and Shelah’s composition method [10]. In this paper we continue along the line started by Thomas in [14] and we compare the decidability proofs for S1S also in a case in which the basic endowment of interpreted predicates is not restricted to <, but it is extended with a binary operator. In particular, we outline how the composition method can be successfully applied to give an alternative proof of the decidability of the proper extension of S1S with the binary predicate flip (see [9] and the following sections1).
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
J.R. Büchi. On a Decision Method in Restricted Second Order Arithmetic. Proc. of the 1960 Internat. Congr. of Logic, Methodology and Philosophy of Science, E. Nagel et al. (Eds.), Stanford University Press 1962, pp. 1-11.
O. Carton, W. Thomas. The Monadic Theory of Morphic Infinite Words and Generalizations. Proc. of the 25th International Symposium on Mathematical Foundations of Computer Science, LNCS 1893, Springer, 2000.
C.C. Chang, H.J. Keisler. Model Theory. North-Holland, Amsterdam 1973.
K. Culik II, A. Salomaa, and D. Wood. Systolic tree acceptors. R.A.I.R.O In-formatique Théorique, 18:53–69, 1984.
H. W. Kamp. Tense Logic and the Theory of Linear Order. Ph.D. Thesis, University of California, Los Angeles, 1968.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems (Specification). Springer-Verlag, 1992.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems (Safety). Springer-Verlag, 1995.
A. Montanari, A. Peron, and A. Policriti. Extending Kamp’s Theorem to Model Time Granularity. Journal of Logic and Computation, 12(4):641–678, 2002.
A. Monti, A. Peron. Systolic Tree ω-Languages: The Operational and the Logical View. Theoretical Computer Science, 233:1–18, 2000.
S. Shelah. The Monadic Theory of Order. In Ann. Math., 102:379–419, 1975.
A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with application to temporal logic. Theoretical Computer Science, 49:217–237, 1987.
W. Thomas. Automata on Infinite Objects. Handbook of Theoretical Computer Science, vol. B, J. van Leeuwen (Ed.), Elsevier Sci. Pub., 133-191, 1990.
W. Thomas. Languages, Automata, and Logic. Handbook of Formal Languages, vol. III, G. Rozenberg and A. Salomaa (Eds.), Springer, 389-455, 1997.
W. Thomas. Ehrenfeucht Games, the Composition Method, and the Monadic Theory of Ordinal Words. Structures in Logic and Computer Science, A Selection of Essays in Honor of A. Ehrenfeucht, J. Mycielski et al. (Eds.), volume 1261 of Lecture Notes in Computer Science, Springer, 118-143, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Marzano, E., Montanari, A., Policriti, A. (2003). Binary Extensions of S1S and the Composition Method. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-39910-0_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21002-3
Online ISBN: 978-3-540-39910-0
eBook Packages: Springer Book Archive