Abstract
This paper focuses on decidability problems for metric and layered temporal logics. We prove the decidability of both the theory of metric temporal structures provided with an infinite number of arbitrarily coarse temporal layers and the theory of metric temporal structures provided with an infinite number of arbitrarily fine temporal layers. The proof for the first theory is obtained by reduction to the decidability problem of an extension of S1S which is the logical counterpart of the class of ω-languages accepted by systolic tree automata. The proof for the second one is done through the reduction to the monadic second-order decidable theory of k successors SkS
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. and T. Henzinger: 1993, ‘Real-time logics: complexity and expressiveness’. Information and Computation 104, 35–77.
Benthem, J. v.: 1995, ‘Temporal Logic’. In: D. Gabbay, C. Hogger, and J. Robinson (eds.): Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4. Oxford University Press, pp. 241–350.
Ciapessoni, E., E. Corsetti, A. Montanari, and P. San Pietro: 1993, ‘Embedding Time Granularity in a Logical Specification Language for Synchronous Real-Time Systems’. Science of Computer Programming 20, 141–171.
Corsetti, E., A. Montanari, and E. Ratto: 1991, ‘Dealing with Different Time Granularities in Formal Specifications of Real-Time Systems’. The Journal of Real-Time Systems 3, 191–215.
Fiadeiro, J. and T. Maibaum: 1992, ‘Sometimes “Tomorrow” is “Sometimes”–Action Refinement in a Temporal Logic of Objects’. In: Proc. ICTL’94, LNAI 827. pp. 48–66.
Koymans, R.: 1992, ‘Specifying Message Passing and Time-Critical Systems with Temporal Logic’. In: LNCS 651.
Läuchli, H. and C. Savoiz: 1987, ‘Monadic Second-Order Definable Relations on the Binary Tree’. Journal of Symbolic Logic 52, 219–226.
Montanari, A. and M. de Rijke: 1995, ‘Two-Sorted Metric Temporal Logic’. Technical Report CS-R9577, CWI, University of Amsterdam. To appear in Theoretical Computer Science.
Montanari, A., A. Peron, and A. Policriti: 1996, ‘Decidable theories of co-layered metric temporal structures’. Technical Report ML-96–07, Institute for Logic Language and Information, University of Amsterdam.
Montanari, A. and A. Policriti: 1996, ‘Decidability Results for Metric and Layered Temporal Logics’. Notre Dame Journal of Formal Logic 37 260–282.
Monti, A. and A. Peron: 1995a, ‘Systolic Tree ω-Languages’. In: Proceedings of STACS-95, LNCS 900. pp. 131–142.
Monti, A. and A. Peron: 1995b, ‘Systolic Tree co-Languages: The Operational and the Logical View’. Technical Report SI-95/11, Dipartimento di Scienze dell’Informazione, Università di Roma “La Sapienza”.
Thomas, W.: 1990, ‘Automata on Infinite Objects’. In: J. van Leeuwen (ed.): Handbook of Theoretical Computer Science, Vol. B. Elsevier Science Publishers, pp. 133–191.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Montanari, A., Peron, A., Policriti, A. (2000). Decidable Theories of ω-Layered Metric Temporal Structures. In: Barringer, H., Fisher, M., Gabbay, D., Gough, G. (eds) Advances in Temporal Logic. Applied Logic Series, vol 16. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9586-5_5
Download citation
DOI: https://doi.org/10.1007/978-94-015-9586-5_5
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5389-3
Online ISBN: 978-94-015-9586-5
eBook Packages: Springer Book Archive