Propositional temporal logics and equivalences
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.
KeywordsTransition System Temporal Logic Event Structure Concurrent System Kripke Structure
Unable to display preview. Download preview PDF.
- [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
- [GKP92]Goltz, U., Kuiper, R., Penczek, W., Propositional Temporal Logics and Equivalences, deliverables of Esprit-BRA project 3096, 1992.Google Scholar
- [KP87]Katz, S., Peled, D., Interleaving Set Temporal Logic, 6th ACM Symposium on Principles of Distributed Computing, Vancouver Canada, 178–190, 1987.Google Scholar
- [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
- [MP88]Manna, Z., Pnueli, A., The Anchored Version of the Temporal Framework, LNCS 354, 1988.Google Scholar
- [MP91]Manna, Z., Pnueli, A., Linear Time Temporal Logic, Springer Verlag, 1991.Google Scholar
- [Mi80]Milner R., A Calculus for Communicating Systems, LNCS 92, 1980.Google Scholar
- [deNF90]deNicola, R., Ferrari, L., Observational Logics and Concurrency, Tech. Report, Dip. di Informatica, Univ. of Pisa, 1990.Google Scholar
- [deNV90]deNicola, R., Vaandrager, F., Three Logics for Branching Bisimulation, Proc. of LICS, 1990.Google Scholar
- [deNMV90]deNicola, R., Montanari, U., and Vaandrager, F., Back and Forth Bisimulations, Proc. of CONCUR'90, 1990.Google Scholar
- [NRT91]Nielsen, M., Rosenberg, G., and Thiagarajan, Transition Systems, Event Structures and Unfoldings, in preparation, 1991.Google Scholar
- [Pa81]Park, D., Concurrency and automata on infinite sequences, 5th Conf. on Theoretical Comp. Sci., LNCS 104, 1981.Google Scholar
- [Ro90]Rozoy, B., On Distributed Languages and Models for Distributed Computation, Technical Report 563, L.R.I., 1990.Google Scholar
- [Si90]Sinachopoulos, A., Partial Order Logics for Elementary Net Systems: State-and Event-approches, Proc. of CONCUR'90, 1990.Google Scholar
- [St87]Stirling, C., Altrincham Workshop, LNCS 398, 1987.Google Scholar
- [TRH88]Trakhtenbrot, B.A., Rabinovich, A., and Hirschfeld J., Nets of Processes, TR 97/88, Tel Aviv Univ., 1988.Google Scholar
- [Wi82]Winskel, G., Event Structure Semantics for CCS and Related Languages, Proc. of ICALP, LNCS 224, 1982.Google Scholar