Solving the ignoring problem for partial order reduction |
| |
Authors: | Sami Evangelista Christophe Pajault |
| |
Affiliation: | 1. Laboratoire d’Informatique de l’Université Paris Nord, Paris, France 2. DAIMI, Aarhus University, Aarhus, Denmark 3. Centre d’Etude et de Recherche en Informatique du Cnam, CNAM, Paris, France
|
| |
Abstract: | Partial order reduction limits the state explosion problem that arises in model checking by limiting the exploration of redundant
interleavings. A state space search algorithm based on this principle may ignore some interleavings by delaying the execution
of some actions provided that an equivalent interleaving is explored. However, if one does not choose postponed actions carefully,
some of these may be infinitely delayed. This pathological situation is commonly referred to as the ignoring problem. The prevention of this phenomenon is not mandatory if one wants to verify if the system halts but it must be resolved for
more elaborate properties like, for example, safety or liveness properties. We present in this work some solutions to this
problem. In order to assess the quality of our propositions, we included them in our model checker Helena. We report the result
of some experiments which show that our algorithms yield better reductions than state of the art algorithms like those implemented
in the Spin tool. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|