|
|
 |
|
Jeudi 9 Octobre
| Heure: |
16:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Unfolding-based Reachability Checking of Petri Nets |
| Description: |
César Rodríguez In model checking, a well known source of state-space explosion (SSE) is
the explicit representation of concurrent actions by their interleavings.
Partial-order reductions attempt to address this by constructing an
equivalent state space where irrelevant executions of the original are
discarded. A comparatively less well-known approach emerges from the use
of partial-order semantics, where the state space is instead represented by
a partial order where concurrent actions are simply left unordered. Petri
net unfoldings are arguably the most prominent verification technique
issued from this idea.
In this talk, three different semantics for Petri nets will be presented,
the last one of which will be the aforementioned unfolding semantics. We
will then see how unfoldings can be employed in practical verification and,
time permitting, how to improve the method to address additional sources of
SSE. |
|
|
