Abstract
Impossible futures equivalence is the semantic equivalence on labelled transition systems that identifies systems iff they have the same “AGEF” properties: temporal logic properties saying that reaching a desired outcome is not doomed to fail. We show that this equivalence, with an added root condition, is the coarsest congruence containing weak bisimilarity with explicit divergence that respects deadlock/livelock traces (or fair testing, or any liveness property under a global fairness assumption) and assigns unique solutions to recursive equations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aceto, L.(moderator): Some open problems in Process Algebra (2003), http://www.cs.auc.dk/luca/BICI/open-problems.html
Baeten, J.C.M. (ed.): Applications of Process Algebra. Cambridge Tracts in Theoretical Computer Science 17. Cambridge University Press, Cambridge (1990)
Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: On the consistency of Koomen’s fair abstraction rule. Theoretical Computer Science 51(l/2), 129–176 (1987)
Bloom, B., Istrael, S., Meyer, A.: Bisimulation Can’t Be Traced. Journal of the ACM 42(1), 232–268 (1995)
Brinksma, E., Rensink, A., Vogler, W.: Fair Testing. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 311–327. Springer, Heidelberg (1995); Journal preprint: http://eprints.eemcs.utwente.nl/1623/01/submitted.pdf
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31(3), 560–599 (1984)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. Journal of the ACM 42(2), 458–487 (1995)
Francez, N.: Fairness. Springer, Heidelberg (1986)
van Glabbeek, R.J.: The Linear Time – Branching Time Spectrum II: The semantics of sequential systems with silent moves (extended abstract). In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
van Glabbeek, R.J.: A Characterisation of Weak Bisimulation Congruence. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to J.W. Klop, On the Occasion of His 60th Birthday, LNCS, vol. 3838, pp. 26–39. Springer, Heidelberg (2005)
Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1990); In: Milner, R.(ed.) A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980) (earlier version appeared)
Vogler, W.: Modular Construction and Partial Order Semantics of Petri Nets. LNCS, vol. 625. Springer, Heidelberg (1992)
Voorhoeve, M., Mauw, S.: Impossible Futures and Determinism. Information Processing Letters 80(1), 51–58 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Glabbeek, R., Voorhoeve, M. (2006). Liveness, Fairness and Impossible Futures. In: Baier, C., Hermanns, H. (eds) CONCUR 2006 – Concurrency Theory. CONCUR 2006. Lecture Notes in Computer Science, vol 4137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817949_9
Download citation
DOI: https://doi.org/10.1007/11817949_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37376-6
Online ISBN: 978-3-540-37377-3
eBook Packages: Computer ScienceComputer Science (R0)