Abstract
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.
Supported in part by Esprit Basic Research Action 3148 (DEMON)
Supported by Esprit-BRA project 3096: Formal Methods and Tools for the Development of Distributed and Real-Time Systems (SPEC)
Supported in part by the Dutch NFI/NWO project REX and also by The Wolfson Research Awards Scheme in The United Kingdom
Preview
Unable to display preview. Download preview PDF.
References
Boudol, G., Castellani, I., On the Semantics of Concurrency: Partial Orders and Transition Systems, Proc. of TAPSOFT 87, LNCS 249, 123–137, 1987.
Browne, M.C., Clarke, B.M., and Grumberg, O., Characterizing Finite Kripke Structures in Propositional Temporal Logic, TCS 59 (1,2), 115–131, 1988.
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.
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.
Glabbeek, R. van. and Goltz, U.: Equivalence Notions for Concurrent Systems and Refinement of Actions, LNCS 379, pp. 237–248, 1989.
Goltz, U., Kuiper, R., Penczek, W., Propositional Temporal Logics and Equivalences, deliverables of Esprit-BRA project 3096, 1992.
Hughes, G.E., Cresswell, M.J., A Companion to Modal Logic, London, Methuen, 1984.
Katz, S., Peled, D., Interleaving Set Temporal Logic, 6th ACM Symposium on Principles of Distributed Computing, Vancouver Canada, 178–190, 1987.
Lamport, L., Sometime is sometimes not never, On the Temporal Logic of Programs, 7th ACM Symp. on Princ. of Programming Logic, 174–185, 1980.
Loogen, R. and Goltz, U., Modelling Nondeterministic Concurrent Processes with Event Structures, Fundamenta Informaticae 14, No. 1, 39–73, 1991.
Manna, Z., Pnueli, A., The Anchored Version of the Temporal Framework, LNCS 354, 1988.
Manna, Z., Pnueli, A., Linear Time Temporal Logic, Springer Verlag, 1991.
Milner R., A Calculus for Communicating Systems, LNCS 92, 1980.
deNicola, R., Ferrari, L., Observational Logics and Concurrency, Tech. Report, Dip. di Informatica, Univ. of Pisa, 1990.
deNicola, R., Vaandrager, F., Three Logics for Branching Bisimulation, Proc. of LICS, 1990.
deNicola, R., Montanari, U., and Vaandrager, F., Back and Forth Bisimulations, Proc. of CONCUR'90, 1990.
Nielsen, M., Plotkin, G., and Winskel, G., Petri Nets, Event Structures and Domains, Part I, TCS 13, Vol. 1, pp. 85–109, 1981.
Nielsen, M., Rosenberg, G., and Thiagarajan, Transition Systems, Event Structures and Unfoldings, in preparation, 1991.
Park, D., Concurrency and automata on infinite sequences, 5th Conf. on Theoretical Comp. Sci., LNCS 104, 1981.
Penczek, W., A Concurrent Branching Time Temporal Logic, Proceedings of the Workshop on Computer Science Logic, Kaiserslautern, LNCS 440, 337–354, 1990.
Rozoy, B., On Distributed Languages and Models for Distributed Computation, Technical Report 563, L.R.I., 1990.
Sinachopoulos, A., Partial Order Logics for Elementary Net Systems: State-and Event-approches, Proc. of CONCUR'90, 1990.
Stirling, C., Altrincham Workshop, LNCS 398, 1987.
Trakhtenbrot, B.A., Rabinovich, A., and Hirschfeld J., Nets of Processes, TR 97/88, Tel Aviv Univ., 1988.
Winskel, G., Event Structure Semantics for CCS and Related Languages, Proc. of ICALP, LNCS 224, 1982.
Winskel, G., An Introduction to Event Structures, LNCS 354, pp. 364–387, 1988.
Wolper, P., On the Relation of Programs and Computations to Models of Temporal Logic, Altrincham Workshop, LNCS 398, 75–123, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goltz, U., Kuiper, R., Penczek, W. (1992). Propositional temporal logics and equivalences. In: Cleaveland, W. (eds) CONCUR '92. CONCUR 1992. Lecture Notes in Computer Science, vol 630. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0084794
Download citation
DOI: https://doi.org/10.1007/BFb0084794
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55822-4
Online ISBN: 978-3-540-47293-3
eBook Packages: Springer Book Archive