Sciweavers

CORR
2006
Springer

PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions

13 years 3 months ago
PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions
We are interested in verifying dynamic properties of finite state reactive systems under fairness assumptions by model checking. The systems we want to verify are specified through a top-down refinement process. In order to deal with the state explosion problem, we have proposed in previous works to partition the reachability graph, and to perform the verification on each part separately. Moreover, we have defined a class, called Bmod, of dynamic properties that are verifiable by parts, whatever the partition. We decide if a property P belongs to Bmod by looking at the form of the B
Samir Chouali, Jacques Julliand, Pierre-Alain Mass
Added 11 Dec 2010
Updated 11 Dec 2010
Type Journal
Year 2006
Where CORR
Authors Samir Chouali, Jacques Julliand, Pierre-Alain Masson, Françoise Bellegarde
Comments (0)