Selected publications by Stefan Schwoon

Abstract:
In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finite-state) Petri nets, which can be used for verification purposes. Contextual nets are a generalisation of Petri nets suited to model systems with read-only access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan's construction to a suitable encoding of the contextual net into an ordinary net. However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. A construction for generating such a contextual complete prefix has been proposed for a special class of nets, called read-persistent. In this paper, we propose an algorithm that works for arbitrary semi-weighted, bounded contextual nets. The construction explicitly takes into account the fact that, unlike in ordinary or read-persistent nets, an event can have several different histories in general contextual net computations.

@incollection{BCKS-topnoc08,
   author = {Baldan, Paolo and Corradini, Andrea and K{\"o}nig, Barbara and Schwoon, Stefan},
   booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{I}},
   DOI = {10.1007/978-3-540-89287-8_12},
   month = nov,
   pages = {199-220},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {{M}c{M}illan's complete prefix for contextual nets},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCKS-topnoc08.ps},
   volume = {5100},
   year = {2008},
}

About LSV