Journal article
Model checking with strong fairness
Formal Methods in System Design, Vol.28(1), pp.57-84
Jan/2006
Abstract
In this paper we present a coherent framework for symbolic model checking of linear-time temporal logic (LTL) properties over finite state reactive systems, taking full fairness constraints into consideration. We use the computational model of a fair discrete system (FDS) which takes into account both justice (weak fairness) and compassion (strong fairness). The approach presented here reduces the model-checking problem into the question of whether a given FDS is feasible (i.e. has at least one computation). The contribution of the paper is twofold: On the methodological level, it presents a direct self-contained exposition of full LTL symbolic model checking without resorting to reductions to either mu-calculus or CTL. On the technical level, it extends previous methods by dealing with compassion at the algorithmic level instead of either adding it to the specification, or transforming compassion to justice. Finally, we extend CTL* stop with past operators, and show that the basic symbolic feasibility algorithm presented here, can be used to model check an arbitrary CTL* formula over an FDS with full fairness constraints.
Details
- Title
- Model checking with strong fairness
- Creators
- Y Kesten (null)Amir Pnueli (null) - The Weizmann Institute of ScienceLO Raviv (null)E Shahar (null)
- Resource Type
- Journal article
- Publication Details
- Formal Methods in System Design, Vol.28(1), pp.57-84; Jan/2006
- Number of pages
- 28
- Language
- English
- DOI
- https://doi.org/10.1007/s10703-006-4342-y
- Scientific Unit
- The Weizmann Institute of Science
- Record Identifier
- 993262378503596
Metrics
12 Record Views