Evènement pour le groupe Modélisation et Verification


Date 2006-11-30  11:00-12:15
TitreUnfolding 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 [KKKV05]. 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 approach. [CGP01] Jean-Michel Couvreur, Sébastien Grivet, and Denis Poitrenaud. Unfolding of products of symmetrical petri nets. In ICATPN, pages 121-143, 2001. [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, 4(1):33-75, 1994. [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).  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurThe Quang Tran 
Emailquang.tran@labri.fr 
UrlLaBRI, Bordeaux, France 



Aucun document lié à cet événement.

Retour
Retour à l'index