Advertisement

Interval logics and sequential transducers

  • Max Michel
  • Jean-Bernard Stefani
Parallelism And Concurrency
  • 118 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)

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.

Keywords

Temporal Logic Atomic Proposition Simple Machine Temporal Formula Output Alphabet 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    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.Google Scholar
  2. [2]
    Pnueli, A. "The Temporal Semantics of Concurrent Programs", Theoretical Computer Science 13. 1981.Google Scholar
  3. [3]
    Hailpern, B. "Verifying Concurrent Processes Using Temporal Logic". LNCS 129. 1982.Google Scholar
  4. [4]
    Lamport, L. "Specifying Concurrent Program Modules". ACM Trans. on Prog. Lang. and Syst. 5, 2. 1983.Google Scholar
  5. [5]
    Kröger, F. "Temporal Logic of Programs". EATCS Monographs on Theoretical Computer Science. Vol. 8. Springer Verlag 1987.Google Scholar
  6. [6]
    Carmo, J. "The Infolog Branching Logic of Events", in Theoretical and Formal Aspects of Information Systems. Sernadas, Bubenko and Olive eds. North-Holland 1985.Google Scholar
  7. [7]
    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.Google Scholar
  8. [8]
    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.Google Scholar
  9. [9]
    Van Benthem, J.F.A.K. "The Logic of Time". Reidel 1983.Google Scholar
  10. [10]
    McDermott, D.V. "A Temporal Logic to Reason About Processes and Plans". Cognitive Science 6. 1982.Google Scholar
  11. [11]
    Allen, J.F.. "Towards a General Theory of Time and Action". Artificial Intelligence 23, 2. 1984.Google Scholar
  12. [12]
    Halpern, J.Y., Shoham, Y. "A Propositional Modal Logic of Time Intervals". Proc. Symp. on Logic in Computer Science, IEEE, Boston, 1986.Google Scholar
  13. [13]
    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.Google Scholar
  14. [14]
    Vardi, M.Y., Wolper, P.L. "An Automata Theoretic Approach to Automatic Program Vertification". Proc. Symp. on Logic in Computer Science, IEEE, Boston, 1986.Google Scholar
  15. [15]
    Michel, M. "Algèbres de Machines et Logique Temporelle". STACS 1984, LNCS 166.Google Scholar
  16. [16]
    Michel, M. "Computation of Temporal Operators". Logique et Analyse 110–111. Special Issue on Automated Reasoning in Non-Classical Logic. June 1985.Google Scholar
  17. [17]
    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.Google Scholar
  18. [18]
    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.Google Scholar
  19. [19]
    Wolper, P.L. "Temporal Logic can be more expressive". Information and Control 56. 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Max Michel
    • 1
  • Jean-Bernard Stefani
    • 2
  1. 1.Centre National d'Etudes des TélécommunicationsIssy-Les-MoulineauxFrance
  2. 2.Centre National d'Etudes des TélécommunicationsService d'Etudes Communes Poste et TélécommunicationsCaenFRANCE

Personalised recommendations