Speaker: Kais Klai (OAS, TU/e)

Title: Symbolic and modular verification approaches for Petri net models


 Abstract: Checking properties of concurrent systems often leads to
 the building of a graph corresponding either to the state graph of the system
 or some synchronized product of it with an automaton.
 In both cases, one has to tackle the state explosion problem,
 i.e., the exponential increase in the number of states w.r.t.
 the number of system’s components.

Among the numerous techniques proposed to cope with such an explosion,
the symbolic approaches and the modular verification represent two of the most efficient techniques
allowing to drastically reduce the size of the state space explored during the verification process.
The symbolic model checking aims to check the property on a compact representation of the system by
using Binary Decision Diagrams (BDD) techniques while modular approaches take advantage
of the modular design of concurrent and distributed systems and aim to
deduce the properties of the global system from those of its components analysed in isolation.

In this talk, I will present some contributions
to symbolic and modular verification of Petri net models.

As the first contribution, I will present a behavioural approach based on
the Symbolic Observation Graph (SOG).
Such a graph is an abstraction of the original reachability graph which preserves the
LTL-X (Linear-time Temporal Logic minus the next operator) logic,
i.e., checking a property of this logic on the SOG is equivalent to check it on the original graph.

The second approach is a modular approach based on the decomposition of Petri nets.
The original model is broken down into components,
then each component is completed by an abstraction of its environment and
analysed separately from the rest.
The abstraction is of the environment is
deduced automatically from the place invariants of the system.
The preservation of general properties (liveness and boundedness) is ensured.

Finally, a mixed approach will be presented combining behavioural and
structural aspects within an incremental and modular verification approach.