Advertisement

On the weak adequacy of branching-time temporal logic

  • Ph. Schoebelen
  • S. Pinchinat
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 432)

Abstract

We study the adequacy of branching-time temporal logic w.r.t. bisimulation semantics in the framework of non-deterministic programs without the finitely-branching restriction. The process equivalence generated by branching-time logic is compared with bisimulation and with two observational equivalences. It is found at best weakly adequate. This further illustrates the strength of the finitely-branching restriction. However, we argue that in connection with branching time temporal logic, one has no better choice than bisimulation as a semantic equivalence: in particular, the equivalence generated by temporal logic is not a congruence w.r.t. usual process operators.

Keywords

Temporal Logic Reverse Implication Model Check Algorithm Infinite Path Rooted Graph 
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.

References

  1. [Abr87]
    S. Abramsky. Observation equivalence as a testing equivalence. Theoretical Computer Science, 53:225–241, 1987.CrossRefGoogle Scholar
  2. [BBK87]
    J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. On the consistency of Koomen's fair abstraction rule. Theoretical Computer Science, 51(1):129–176, 1987.CrossRefGoogle Scholar
  3. [BK87]
    J. A. Bergstra and J. W. Klop. A Convergence Theorem in Process Algebra. Research Report CSR8733, CWI, 1987.Google Scholar
  4. [BK89]
    J. A. Bergstra and J. W. Klop. Process theory based on bisimulation semantics. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, LNCS 354, pages 50–122, Springer-Verlag, 1989.Google Scholar
  5. [BR83]
    S. D. Brookes and W. C. Rounds. Behavioural equivalence relations induced by programming logics. In Proc. 10th ICALP, Barcelona, LNCS 154, pages 97–108, Springer-Verlag, July 1983.Google Scholar
  6. [CE81]
    E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Logics of Programs Workshop, Yorktown Heights, LNCS 131, pages 52–71, Springer-Verlag, May 1981.Google Scholar
  7. [EH83]
    E. A. Emerson and J. Y. Halpern. “Sometimes” and “Not Never” revisited: on branching versus linear time. In Proc. 10th ACM Symp. Principles of Programming Languages, Austin, Texas, pages 127–140, January 1983.Google Scholar
  8. [ES89]
    E. A. Emerson and J. Srinivasan. Branching time temporal logic. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, LNCS 354, pages 123–172, Springer-Verlag, 1989.Google Scholar
  9. [GR83]
    W. G. Golson and W. C. Rounds. Connections between two theories of concurrency: metric spaces and synchronization trees. Information and Control, 57, 1983.Google Scholar
  10. [HM85]
    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, January 1985.CrossRefGoogle Scholar
  11. [HS85]
    M. Hennessy and C. Stirling. The power of the future perfect in program logics. Information and Control, 67:23–52, 1985.CrossRefGoogle Scholar
  12. [Klo88]
    J. W. Klop. Bisimulation Semantics. Lectures given at the REX School/Workshop, Noordwijkerhout, NL, May 1988.Google Scholar
  13. [Lam80]
    L. Lamport. “Sometimes” is sometimes “Not Never”. In Proc. 7th ACM Symp. Principles of Programming Languages, Las Vegas, pages 174–185, January 1980.Google Scholar
  14. [Mil81]
    R. Milner. A modal characterisation of observable machine-behaviour. In Proc. CAAP 81, Genoa, LNCS 185, pages 25–34, Springer-Verlag, March 1981.Google Scholar
  15. [Mil88]
    R. Milner. Operational and Algebraic Semantics of Concurrent Processes. Research Report ECSLFCS-88-46, Lab. for Foundations of Computer Science, Edinburgh, February 1988. To appear in the Handbook of Theoretical Computer Science.Google Scholar
  16. [Par81]
    D. Park. Concurrency and automata on infinite sequences. In Proc. 5th GI Conf., pages 167–183, Springer-Verlag, March 1981.Google Scholar
  17. [Pnu77]
    A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. Foundations of Computer Science, Providence, pages 46–57, 1977.Google Scholar
  18. [San82]
    M. T. Sanderson. Proof Techniques for CCS. PhD thesis, Univ. Edinburgh, November 1982. Available as Report CST-19-82.Google Scholar
  19. [Sch89]
    Ph. Schnoebelen. Congruence Properties of the Process Equivalence Induced by Temporal Logic. 1989. Submitted for publication.Google Scholar
  20. [SJ89]
    Ph. Schnoebelen and Ph. Jorrand. Principles of FP2. Term algebras for specification of parallel machines. In J. W. de Bakker, editor, Languages for Parallel Architectures: Design, Semantics, Implementation Models, chapter 5, pages 223–273, Wiley, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Ph. Schoebelen
    • 1
  • S. Pinchinat
    • 1
    • 2
  1. 1.Laboratoire d'Informatique Fondamentale et d'Intelligence ArtificielleInstitut Imag — CNRSGrenobleFrance
  2. 2.Lifia-ImagGrenoble CedexFrance

Personalised recommendations