Evènement pour le groupe Modélisation et Verification
|Date|| 2006-11-30 11:00-12:15|
|Titre||Unfolding Concurrent Well-Structured Transition Systems |
|Résumé||Joint work with Frédéric Herbreteau and Grégoire Sutre.
In this work, our main objective is to combine partial-order methods with
verification techniques for infinite-state systems in order to obtain efficient
verification algorithms for concurrent infinite-state systems. This paper
presents a general framework for partial-order modeling and verification of
well-structured transition systems.
Firstly, McMillan has proposed a technique in the verification of
systems modelled with finite-state Petri nets [McM95]. This technique is based on the
concept of net unfoldings and a well-known partial-order semantics of Petri
nets. It construct only a finite complete prefix of the unfolding which
contains full information about the reachable states. The unfolding technique
has been later developed for other model of concurrency, e.g. Synchronous
Products of Transition Systems [ER99], High-Level Petri Nets [KK03], Extended
Finite State Machines [LI05]; and applied to other verification problems,
e.g. checking relevant properties of speed independent circuits [KKTV95], simple
branching time logic [Esp94].
Although the finite prefix obtained by unfolding technique avoids the
interleaving explosion, it is sometimes much larger than necessary. Several
works trying to resolve this problem can be classified into two types. The
first one is to give a more adequate criteria in truncating the unfolding, e.g.
based on a total order of trace [ER99], based on the symmetry of Petri Nets w.r.t
some notions [CGP01]; and the second one is to avoiding the unuseful
multiplication of a same labeled event when unfolding non-safe Petri nets
In our work, we model concurrent systems as synchronized
products of (heterogeneous) components, where the semantics of components is
given in terms of event structures. This allows us to benefit from the
intrinsic concurrency in each component. We propose event structures for
counters and queues, and we present an on-the-fly compositional unfolding
algorithm that computes event structures for synchronized products. For the
particular case of well-structured components, we give property-preserving
truncation criteria [FS01] on event structures in order to obtain effective decision
algorithms for the boundedness, termination and quasi-liveness problems.
Moreover, our technique for avoiding redundancy in the unfolding can also
resolving the irrelevant multiplication problem stated in [KKKV05].
We have implemented a tool, called ESU, for demonstrating the benefits of our
[CGP01] Jean-Michel Couvreur, Sébastien Grivet, and Denis Poitrenaud. Unfolding
of products of symmetrical petri nets. In ICATPN, pages
[ER99] J. Esparza and S. Römer. An unfolding algorithm for synchronous
products of transition systems. In International Conference on Con-
currency Theory, volume 1664 of Lecture Notes in Computer Sci-
ence, pages 2-20, 1999.
[Esp94] Javier Esparza. Model checking using net unfoldings. Sci. Comput.
Program., 23(2-3):151-195, 1994.
[FS01]Alain Finkel, Ph. Schnoebelen: Well-structured transition systems everywhere!
Theor. Comput. Sci. 256(1-2): 63-92 (2001)
[KK03] Victor Khomenko and Maciej Koutny. Branching processes of highlevel
petri nets. In TACAS, pages 458-472, 2003.
[KKKV05] Victor Khomenko, Alex Kondratyev, Maciej Koutny, and Walter
Vogler. Merged processes - a new condensed representation of petri
net behaviour. In CONCUR, pages 338-352, 2005.
[KKTV94] Michael Kishinevsky, Alex Kondratyev, Alexander Taubin, and Victor
Varshavsky. Analysis and identification of speed-independent
circuits on an event model. Formal Methods in System Design,
[LI05] Yu Lei and S. Purushothaman Iyer. An approach to unfolding asynchronous
communication protocols. In FM, pages 334-349, 2005.
[McM95]Kenneth L. McMillan. A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1): 45-65 (1995). |
|Lieu||Salle 076, LaBRI, Rez-de-chaussée |
|Orateur||The Quang Tran |
|Url||LaBRI, Bordeaux, France |
Aucun document lié à cet événement.RetourRetour à l'index