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. https://doi.org/10.1007/11817949_9