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.
|Title of host publication||CONCUR 2006 - Concurrency Theory (Proceedings 17th International Conference, Bonn, Germany, August 27-30, 2006)|
|Editors||C. Baier, H. Hermanns|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|
Glabbeek, van, R. J., & Voorhoeve, M. (2006). Liveness, fairness and impossible futures. In C. Baier, & H. Hermanns (Eds.), CONCUR 2006 - Concurrency Theory (Proceedings 17th International Conference, Bonn, Germany, August 27-30, 2006) (pp. 126-141). (Lecture Notes in Computer Science; Vol. 4137). Springer. https://doi.org/10.1007/11817949_9