Liveness, fairness and impossible futures

Download files
Access & Terms of Use
open access
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.
Persistent link to this record
DOI
Link to Publisher Version
Additional Link
Author(s)
van Glabbeek, Robert
Voorhoeve, M
Supervisor(s)
Creator(s)
Editor(s)
Translator(s)
Curator(s)
Designer(s)
Arranger(s)
Composer(s)
Recordist(s)
Conference Proceedings Editor(s)
Other Contributor(s)
Corporate/Industry Contributor(s)
Publication Year
2006
Resource Type
Conference Paper
Degree Type
UNSW Faculty
Files
download 0200602318_if.pdf 207.79 KB Adobe Portable Document Format
Related dataset(s)