Unfolding Concurrent Well-Structured Transition Systems

Frédéric Herbreteau
Labri, Bordeaux
Friday, 9 May, 2008 (All day)

Partial-order methods are commonly used in analysis of finite systems consisting of many concurrent components. We propose an extension of unfolding algorithms to parallel compositions of infinite-state systems. We argue that it is advantageous to model each component by an event structure. Indeed this permits to exhibit intrinsic concurrency present in infinite-state systems like for instance automata with queues or counters. We generalize the notion of complete finite prefix of an unfolding from 1-safe Petri nets to all well-structured transition systems. We give an on-the-fly unfolding algorithm that given event structures representing the components produces an event structure representing their synchronized product. The benefits of our approach have been demonstrated by a prototype implementation.