Selected publications at LSV

Abstract:
In recent years, a research thread focused on the use of the unfolding semantics for verification purposes. This started with a paper by McMillan, which devises an algorithm for constructing a finite complete prefix of the unfolding of a safe Petri net, providing a compact representation of the reachability graph. The extension to contextual nets and graph transformation systems is far from being trivial because events can have multiple causal histories. Recently, we proposed an abstract algorithm that generalizes McMillan's construction to bounded contextual nets without resorting to an encoding into plain P/T nets. Here, we provide a more explicit construction that renders the algorithm effective. To allow for an inductive definition of concurrency, missing in the original proposal and essential for an efficient unfolding procedure, the key intuition is to associate histories not only with events, but also with places. Additionally, we outline how the proposed algorithm can be extended to graph transformation systems, for which previous algorithms based on the encoding of read arcs would not be applicable.

@inproceedings{bbcks-icgt10,
   address = {Enschede, The Netherlands},
   author = {Baldan, Paolo and Bruni, Alessandro and Corradini, Andrea and K{\"o}nig, Barbara and Schwoon, Stefan},
   booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {G}raph {T}ransformations ({ICGT}'10)},
   DOI = {10.1007/978-3-642-15928-2_7},
   editor = {Ehrig, Hartmut and Rensink, Arend and Rozenberg, Grzegorz and Sch{\"u}rr, Andy},
   month = sep # {-} # oct,
   pages = {91-106},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {On the Computation of {M}c{M}illan's Prefix for Contextual Nets and Graph Grammars},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bbcks-icgt10.pdf},
   volume = {6372},
   year = {2010},
}

About LSV