Liveness, fairness and impossible futures

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.