Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas

https://hal.archives-ouvertes.fr/hal-00739349
Contributor : Frédéric Davesne <>
Submitted on : Monday, October 8, 2012 - 9:21:36 AM
Last modification on : Tuesday, June 30, 2020 - 11:56:08 AM

Identifiers

  • HAL Id : hal-00739349, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

104