From Symmetric Nets to Symmetric Nets with Bags (2015 edition, full HD)

This sequence starts with a general overview of the tutorial. Then, the characteristics of different kinds of Petri

nets, from Place/Transition nets to Coloured nets, are put into light and motivate the focus of this tutorial on

Symmetric nets. These are then informally introduced.

This sequence starts with a general overview of the tutorial. Then, the characteristics of different kinds of Petri

nets, from Place/Transition nets to Coloured nets, are put into light and motivate the focus of this tutorial on

Symmetric nets. These are then informally introduced.

This sequence presents the syntax and semantics of Symmetric nets, so that a rigorous presentation of their

firing rule can be given, together with an example. The specific basic colour functions that are used in Symmetric nets

are also detailed.

This sequence presents the syntax and semantics of Symmetric nets, so that a rigorous presentation of their

firing rule can be given, together with an example. The specific basic colour functions that are used in Symmetric nets

are also detailed.

This sequence presents a complete small example, where a simple train system with conditions to avoid trains collisions

is modelled step-by-step. It thus shows the modelling approach process when using Symmetric nets.

This sequence presents a complete small example, where a simple train system with conditions to avoid trains collisions

is modelled step-by-step. It thus shows the modelling approach process when using Symmetric nets.

After having modelled a system using Petri nets, the objective is to verify it satisfies some interesting properties.

To do so, the construction of the reachability graph is introduced, which exhaustively explores all possible states of

the system.

After having modelled a system using Petri nets, the objective is to verify it satisfies some interesting properties.

To do so, the construction of the reachability graph is introduced, which exhaustively explores all possible states of

the system.

Properties to be satisfied by the system must be expressed in a formal language. A first approach is introduced with

LTL (Linear Time Logic) properties.

Properties to be satisfied by the system must be expressed in a formal language. A first approach is introduced with

LTL (Linear Time Logic) properties.