Liveness, fairness and impossible futures

R.J. Glabbeek, van, M. Voorhoeve

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

11 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationCONCUR 2006 - Concurrency Theory (Proceedings 17th International Conference, Bonn, Germany, August 27-30, 2006)
EditorsC. Baier, H. Hermanns
Place of PublicationBerlin
PublisherSpringer
Pages126-141
ISBN (Print)3-540-37378-4
DOIs
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
Volume4137
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Liveness, fairness and impossible futures'. Together they form a unique fingerprint.

Cite this