For the most recent entries see the Petri Nets Newsletter.

Verification based on local states.

Huhn, M.; Niebert, P.; Wallner, F.

In: Lecture Notes in Computer Science, Vol. 1384: Tools and Algorithms for the Construction and Analysis of Systems, pages 36-51. Springer-Verlag, 1998.

Abstract: Net unfoldings are a well-known partial order semantics for Petri nets. Here we show that they are well suited to act as models for branching-time logics interpreted on local states. Such local logics (in particular a distributed mi-calculus) can be used to express properties from the point of view of one component in a distributed system. Local logics often allow for more efficient verification procedures because - in contrast to interleaving branching-time logics - they do not refer to the entire space of global states. We reduce verification of local properties to standard model checking algorithms known for interleaving branching-time logics. The key is to extract a finite (usually small), local transition system bisimilar to the complete unfolding. The construction is based on the finite prefix of a net unfolding defined by McMillan.

Keywords: Petri nets, distributed systems, mi-calculus, partial order semantics.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography