Skip to content

Liveness, fairness and impossible futures

Citations of this article
Mendeley users who have this article in their library.
Get full text


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. © Springer-Verlag Berlin Heidelberg 2006.




Van Glabbeek, R., & Voorhoeve, M. (2006). Liveness, fairness and impossible futures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4137 LNCS, pp. 126–141). Springer Verlag.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free