Propositional temporal logics and equivalences

  • Ursula Goltz
  • Ruurd Kuiper
  • Wojciech Penczek
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


We compare propositional temporal logics by comparing the equivalences that they induce on models. Linear time, branching time and partial order temporal logics are considered. The logics are interpreted on occurrence transition systems, generated by labelled prime event structures without autoconcurrency. The induced equivalences are also compared to directly defined equivalences, e.g., history preserving bisimulation, pomset bisimulation, pomset trace equivalence, and others. It is then shown which of the induced equivalences are and which are not preserved under action refinement.

Rather unexpectedly, the addition of the backward next step operator to the weakest logic considered yields a logic stronger than all others. It is shown that weak history preserving bisimulation can be obtained as the equivalence induced by a slightly constrained version of that logic.


Transition System Temporal Logic Event Structure Concurrent System Kripke Structure 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BC87]
    Boudol, G., Castellani, I., On the Semantics of Concurrency: Partial Orders and Transition Systems, Proc. of TAPSOFT 87, LNCS 249, 123–137, 1987.zbMATHMathSciNetGoogle Scholar
  2. [BCG88]
    Browne, M.C., Clarke, B.M., and Grumberg, O., Characterizing Finite Kripke Structures in Propositional Temporal Logic, TCS 59 (1,2), 115–131, 1988.zbMATHMathSciNetCrossRefGoogle Scholar
  3. [CES83]
    Clarke, E.M., Emerson, E.A., Sistla, A.P., Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, Proc. 10th Annual ACM Symp. on Principles of Programming Languages, Austin, 117–126, 1983.Google Scholar
  4. [EH86]
    Emerson, E.A., Halpern, J.Y., Sometimes and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic, Journal of the ACM 33 (1), 151–178, 1986.zbMATHMathSciNetCrossRefGoogle Scholar
  5. [vGG89]
    Glabbeek, R. van. and Goltz, U.: Equivalence Notions for Concurrent Systems and Refinement of Actions, LNCS 379, pp. 237–248, 1989.zbMATHGoogle Scholar
  6. [GKP92]
    Goltz, U., Kuiper, R., Penczek, W., Propositional Temporal Logics and Equivalences, deliverables of Esprit-BRA project 3096, 1992.Google Scholar
  7. [HC84]
    Hughes, G.E., Cresswell, M.J., A Companion to Modal Logic, London, Methuen, 1984.zbMATHGoogle Scholar
  8. [KP87]
    Katz, S., Peled, D., Interleaving Set Temporal Logic, 6th ACM Symposium on Principles of Distributed Computing, Vancouver Canada, 178–190, 1987.Google Scholar
  9. [La80]
    Lamport, L., Sometime is sometimes not never, On the Temporal Logic of Programs, 7th ACM Symp. on Princ. of Programming Logic, 174–185, 1980.Google Scholar
  10. [LG91]
    Loogen, R. and Goltz, U., Modelling Nondeterministic Concurrent Processes with Event Structures, Fundamenta Informaticae 14, No. 1, 39–73, 1991.zbMATHMathSciNetGoogle Scholar
  11. [MP88]
    Manna, Z., Pnueli, A., The Anchored Version of the Temporal Framework, LNCS 354, 1988.Google Scholar
  12. [MP91]
    Manna, Z., Pnueli, A., Linear Time Temporal Logic, Springer Verlag, 1991.Google Scholar
  13. [Mi80]
    Milner R., A Calculus for Communicating Systems, LNCS 92, 1980.Google Scholar
  14. [deNF90]
    deNicola, R., Ferrari, L., Observational Logics and Concurrency, Tech. Report, Dip. di Informatica, Univ. of Pisa, 1990.Google Scholar
  15. [deNV90]
    deNicola, R., Vaandrager, F., Three Logics for Branching Bisimulation, Proc. of LICS, 1990.Google Scholar
  16. [deNMV90]
    deNicola, R., Montanari, U., and Vaandrager, F., Back and Forth Bisimulations, Proc. of CONCUR'90, 1990.Google Scholar
  17. [NPW81]
    Nielsen, M., Plotkin, G., and Winskel, G., Petri Nets, Event Structures and Domains, Part I, TCS 13, Vol. 1, pp. 85–109, 1981.MathSciNetCrossRefGoogle Scholar
  18. [NRT91]
    Nielsen, M., Rosenberg, G., and Thiagarajan, Transition Systems, Event Structures and Unfoldings, in preparation, 1991.Google Scholar
  19. [Pa81]
    Park, D., Concurrency and automata on infinite sequences, 5th Conf. on Theoretical Comp. Sci., LNCS 104, 1981.Google Scholar
  20. [Pe90]
    Penczek, W., A Concurrent Branching Time Temporal Logic, Proceedings of the Workshop on Computer Science Logic, Kaiserslautern, LNCS 440, 337–354, 1990.zbMATHMathSciNetGoogle Scholar
  21. [Ro90]
    Rozoy, B., On Distributed Languages and Models for Distributed Computation, Technical Report 563, L.R.I., 1990.Google Scholar
  22. [Si90]
    Sinachopoulos, A., Partial Order Logics for Elementary Net Systems: State-and Event-approches, Proc. of CONCUR'90, 1990.Google Scholar
  23. [St87]
    Stirling, C., Altrincham Workshop, LNCS 398, 1987.Google Scholar
  24. [TRH88]
    Trakhtenbrot, B.A., Rabinovich, A., and Hirschfeld J., Nets of Processes, TR 97/88, Tel Aviv Univ., 1988.Google Scholar
  25. [Wi82]
    Winskel, G., Event Structure Semantics for CCS and Related Languages, Proc. of ICALP, LNCS 224, 1982.Google Scholar
  26. [Wi88]
    Winskel, G., An Introduction to Event Structures, LNCS 354, pp. 364–387, 1988.MathSciNetGoogle Scholar
  27. [Wo87]
    Wolper, P., On the Relation of Programs and Computations to Models of Temporal Logic, Altrincham Workshop, LNCS 398, 75–123, 1987.MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Ursula Goltz
    • 1
  • Ruurd Kuiper
    • 2
  • Wojciech Penczek
    • 3
  1. 1.GMDBonnGermany
  2. 2.Department of Computer ScienceEindhoven University of TechnologyThe Netherlands
  3. 3.Institute of Computer ScienceWarsawPoland

Personalised recommendations