Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Reasoning About Systems with Transition Fairness
verfasst von : Benjamin Aminof, Thomas Ball, Orna Kupferman
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Formal verification methods model systems by Kripke structures. In order to model live behaviors of systems, Kripke structures are augmented with
fairness conditions
. Such conditions partition the computations of the systems into fair computations, with respect to which verification proceeds, and unfair computations, which are ignored. Reasoning about Kripke structures augmented with fairness is typically harder than reasoning about non-fair Kripke structures. We consider the
transition fairness
condition, where a computation
π
is fair iff each transition that is enabled in
π
infinitely often is also taken in
π
infinitely often. Transition fairness is a natural and useful fairness condition. We show that reasoning about Kripke structures augmented with transition fairness is not harder than reasoning about non-fair Kripke structures. We demonstrate it for fair CTL and LTL model checking, and the problem of calculating the dominators and postdominators.