Advertisement
Published in:
2005 | OriginalPaper | Chapter
Reasoning About Systems with Transition Fairness
Authors : Benjamin Aminof, Thomas Ball, Orna Kupferman
Published in: Logic for Programming, Artificial Intelligence, and Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.