Effective Marking Equivalence Checking in Systems with Dynamic Process Creation - Université d'Évry Access content directly
Conference Papers Year : 2012

Effective Marking Equivalence Checking in Systems with Dynamic Process Creation

Abstract

The starting point of this work is a framework allowing to model systems with dynamic process creation, equipped with a procedure to detect symmetric executions (i.e., which di er only by the identities of processes). This allows to reduce the state space, potentially to an exponentially smaller size, and, because process identi ers are never reused, this also allows to reduce to nite size some in nite state spaces. However, in this approach, the procedure to detect symmetries does not allow for computationally e cient algorithms, mainly because each newly computed state has to be compared with every already reached state. In this paper, we propose a new approach to detect symmetries in this framework that will solve this problem, thus enabling for e cient algorithms. We formalise a canonical repre- sentation of states and identify a su cient condition on the analysed model that guarantees that every symmetry can be detected. For the models that do not fall into this category, our approach is still correct but does not guarantee a maximal reduction of state space.
No file

Dates and versions

hal-00739349 , version 1 (08-10-2012)

Identifiers

  • HAL Id : hal-00739349 , version 1

Cite

Lukasz Fronc. Effective Marking Equivalence Checking in Systems with Dynamic Process Creation. 14th International Workshop on Verification of Infinite-State Systems (INFINITY 2012), Aug 2012, Paris, France. (elec. proc). ⟨hal-00739349⟩
40 View
0 Download

Share

Gmail Facebook X LinkedIn More