Related Papers :
2006On the Computation of Stubborn Sets of Colored Petri Nets. In Proceedings of the 26th International Conference on Application and Theory of Petri Nets. Turku, Finland, June 26-30, 2006
Abstract : Valmari's Stubborn Sets method is a member of the so-called partial order methods. These techniques are usually based on a selective search algorithm: at each state processed during the search, a stubborn set is calculated and only the enabled transitions of this set are used to generate the successors of the state. The computation of stubborn sets requires to detect dependencies between transitions in terms of conflict and causality. In colored Petri nets these dependencies are difficult to detect because of the color mappings present on the arcs: conflicts and causality connections depend on the structure of the net but also on these mappings. Thus, tools that implement this technique usually unfold the net before exploring the state space, an operation that is often untractable in practice. We present in this work an alternative method which avoids the cost of unfolding the net. To allow this, we use a syntactically restricted class of colored nets. Note that this class still enables wide modeling facilities since it is the one used in our model checker Helena which has been designed to support the verification of software specifications. The algorithm presented has been implemented and several experiments which show the benefits of our approach are reported. For several models we obtain a reduction close or even equal to the one obtained after an unfolding of the net. We were also able to efficiently reduce the state spaces of several models obtained by an automatic translation of concurrent software.
A Semi-Explicit Method to Store State Spaces in a Compact Way CEDRIC Technical Report No 682, 2004.
Abstract : The limited amount of memory is the major bottleneck in model checking tools and algorithms based on an explicit states enumeration. Thus, techniques which allow to represent the states efficiently are precious for these tools. We present in this work a novel approach which enables to store the state space in a compact way. Though it belongs to the family of explicit storage methods, we qualify it as semi-explicit since states may not be explicitly represented in the state space. Experiments show that very compact representations are obtained, with an acceptable increase of the run time.
An Efficient Algorithm for the Enabling Test of Colored Petri Nets In Proceedings Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (CPN'04), Aarhus, Denmark, oct. 2004.
Abstract : Model checking and simulation tools based on the colored Petri nets formalism spend a significant amount of time in performing enabling tests. This consists in taking into account the color mappings of the net to determine valid transitions variables assignments at a given marking. This work proposes an algorithm for the enabling test problem. It implements the relations of conflict and causality between transitions to efficiently maintain a set of enabled transitions. This set is updated during the search algorithm according to the transitions fired (or unfired). However, in most cases this approach is not sufficient to compute the set of enabled transition bindings, and has to be followed by a unification algorithm. This is the objective of the second part of this work.
New Coloured Reductions for Software Validation In Proceedings Workshop on Discrete Event Systems (Wodes'04), Reims, France, sep. 2004.
Abstract : Structural model abstraction is a powerful technique for reducing the complexity of a state based enumeration analysis. We present in this paper accurate reductions for high-level Petri nets based on new ordinary Petri nets reductions. These reductions involve only structural and algebraical conditions. They preserve the liveness of the net and any LTL formula that does not observe the reduced transitions of the net. The mixed use of structural and algebraical conditions significantly enlarges their application area. Furthermore the specification of the transformation is parametric with respect to the cardinalities of coloured domains.
Syntactical Rules for Colored Petri Nets Manipulation CEDRIC Technical Report No 641, 2004.
Abstract : Defining structural analysis techniques for colored Petri nets or generalizing existing techniques of ordinary nets to colored nets is made difficult by the management of the color mappings of the net. Indeed, the structure of the colored net does not necessarily reflect the one of the underlying net. A solution is to unfold the net and work directly on the unfolded net. Another one is to work directly on the colored net in a symbolic way. We explore in this work a symbolic framework based on constraints systems. A class of colored Petri nets is defined. We define simple rules to translate each color mapping allowed by this class into an equivalent constraints system. At last we work at a syntactical level to check properties of mappings. Two relevant examples of application are given.
. Short presentation of Quasar (pdf version of "What is Quasar" section) : pdf / ps.
last update : 30/06/2005