Abstract
This paper applies and extends to (discrete propositional linear) interval logic results obtained in previous papers on the correspondence between extended discrete propositional linear temporal logic and sequential machines with infinite input/output. The machines obtained enable us to derive decision procedures for certain kinds of interval logics. One system of interval logic is considered, and its associated system of machines is constructed. With this construction we also obtain a kind of translation between this interval logic and extended discrete propositional linear temporal logic.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Manna, Z., Pnueli, A. "Verification of Concurrent Programs: The Temporal Framework", in The Correctness Problem in Computer Science. Boyer and Moore eds. Academic Press. 1981.
Pnueli, A. "The Temporal Semantics of Concurrent Programs", Theoretical Computer Science 13. 1981.
Hailpern, B. "Verifying Concurrent Processes Using Temporal Logic". LNCS 129. 1982.
Lamport, L. "Specifying Concurrent Program Modules". ACM Trans. on Prog. Lang. and Syst. 5, 2. 1983.
Kröger, F. "Temporal Logic of Programs". EATCS Monographs on Theoretical Computer Science. Vol. 8. Springer Verlag 1987.
Carmo, J. "The Infolog Branching Logic of Events", in Theoretical and Formal Aspects of Information Systems. Sernadas, Bubenko and Olive eds. North-Holland 1985.
Ehrich, H.D., Gogolla, M., Lipeck, U.W. "Specifying Adimissibility of Dynamic Database Constraints Using Temporal Logic", in Theoretical and Formal Aspects of Information Systems. Sernadas, Bubenko and Olive eds. North-Holland 1985.
Carmo, J., Sernadas, A. "A Temporal Logic Framework for a Layered Approach to System Specification and Verification", in Proc. Conf. on Temporal Aspects in Information Systems, IFIP, Sophia Antipolis, 1987.
Van Benthem, J.F.A.K. "The Logic of Time". Reidel 1983.
McDermott, D.V. "A Temporal Logic to Reason About Processes and Plans". Cognitive Science 6. 1982.
Allen, J.F.. "Towards a General Theory of Time and Action". Artificial Intelligence 23, 2. 1984.
Halpern, J.Y., Shoham, Y. "A Propositional Modal Logic of Time Intervals". Proc. Symp. on Logic in Computer Science, IEEE, Boston, 1986.
Büchi, J.R. "On a Decision Method in Restricted Second Order Arithmetic". Proc. 1960 Intern. Congress on Logic, Methodology and Philosophy of Science. Stanford University Press 1962.
Vardi, M.Y., Wolper, P.L. "An Automata Theoretic Approach to Automatic Program Vertification". Proc. Symp. on Logic in Computer Science, IEEE, Boston, 1986.
Michel, M. "Algèbres de Machines et Logique Temporelle". STACS 1984, LNCS 166.
Michel, M. "Computation of Temporal Operators". Logique et Analyse 110–111. Special Issue on Automated Reasoning in Non-Classical Logic. June 1985.
Schwartz, R. Melliar-Smith, P.M., Vogt, F. "An Interval Logic for Higher-Level Temporal Reasoning". SIGACT/SIGOPS Conf. on Princ. of Distributed Computing, Montreal, 1983.
Schwartz, R. Melliar-Smith, P.M., Vogt, F. "Interval Logic: A Higher Level Temporal Reasoning for Protocol Verification", in Protocol Specification, Testing, and Verification III. Rudin and West eds. North-Holland 1983.
Wolper, P.L. "Temporal Logic can be more expressive". Information and Control 56. 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michel, M., Stefani, JB. (1988). Interval logics and sequential transducers. In: Dauchet, M., Nivat, M. (eds) CAAP '88. CAAP 1988. Lecture Notes in Computer Science, vol 299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026108
Download citation
DOI: https://doi.org/10.1007/BFb0026108
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19021-9
Online ISBN: 978-3-540-38930-9
eBook Packages: Springer Book Archive