Liveness, Fairness and Impossible Futures

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.

• Type: Conference
• Year: 2006
• Where: CONCUR
• Authors: Rob J. van Glabbeek, Marc Voorhoeve
• Keywords: CONCUR 2006, Distributed And Parallel Computing, Impossible Futures Equivalence, Semantic Equivalence, Temporal Logic Properties