CUI LSV LIPN LIP6
MeFoSyLoMa CNRS Iniria
QR Code
Last modified
June 28, 2016

Displayed
Nov 21, 2017
From Symmetric Nets to Symmetric Nets with Bags
Petri net 2014 tutorial
Slides & Videos
Download The Tool
Required
VirtualBox must be installed
CosyVerif (for practice)
Practice
Exercice 1 (session 2)
Exercice 2 (session 4)

Introduction

This is the web page dedicated to the tutorial presented at Petri Nets 2014 on June 24, 2014 in Tunis, Tunisia.

Videos of the presentation are available on the session's pages. You may also access them on the UPMC's video web site or on iTunesU.

Scope

Depending on the system to model and analyse, using place/transition nets may easily be cumbersome and error-prone. Hence, it might be convenient to use some class of high-level nets. Coloured Petri nets enjoy the use of a high-level language to describe data while the net structure captures the flow of information. Although they provide very nice means for modelling, their generality has the drawback of the difficulty to apply efficient analysis techniques.

In this tutorial, we focus on symmetric nets which are high-level nets with a limited set of allowed data types, allowing for efficient state space analysis. We also tackle their extension to symmetric nets with bags for which analysis can still be applied.

The tutorial will present the underlying theory, the verification approaches, typical applications, and will put these into practice through hands-on sessions using the CosyVerif verification environment.

Associated Software to be installed

Please get here to download and install CosyVerif.

Schedule

Session 1 : 9:30-11:00 (see dedicated page for slides and videos)

  1. Introduction
    Petri net classes.
    Symmetric Nets (SN).
  2. Syntax and semantics of SN
    Syntax.
    Semantics (Firing rule).
    Reachability Graph construction.
  3. SN and the verification of distributed systems
    Atomic propositions.
    Reachability properties.
    Temporal properties (CTL based).

Session 2 : 11:30-13:00 (lab, see dedicated page for slides and videos)

  1. Introduction to the verification environment.
  2. Example in P/T and in coloured nets (the swimming pool example, maybe the fireman example too).
  3. Study of a simple producer/consumer system (SN).

Session 3 : 14:30-16:00 (see dedicated page for slides and videos)

  1. Global Symmetries vs. Local Symmetries
    Symbolic Reachability Graph (SRG)
    Extended Symbolic Reachability Graph (ESRG)
    Dynamic Symbolic Reachability Graph (DSRG)
  2. Symmetric nets with Bags (SNB)
    Syntactic extensions
    Semantics (Firing rule)
    «unfolding» into SN (when finite)
  3. Conclusion and perspectives

Session 4 : 16:30-18:00 (lab, see dedicated page for documents)

  1. Comparing the explicit approach (prod) with the SRG-based one (GreatSPN)
  2. Discussion of properties breaking symmetries
  3. Modelling in SNB: the «voter» system (simple), the «sales store system» (more complex)