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

• September 30, 2015S1.01 - Introduction to Symmetric Nets

  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.

  ...more

  

  ---

• September 30, 2015S1.01 - Introduction to Symmetric Nets (pdf)

  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.

  ...more

  

  ---

• September 30, 2015S1.02 - Syntax and Semantics of Symmetric Nets

  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.

  ...more

  

  ---

• September 30, 2015S1.02 - Syntax and Semantics of Symmetric Nets (pdf)

  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.

  ...more

  

  ---

• September 30, 2015S1.03 - Modelling with 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.

  ...more

  

  ---

• September 30, 2015S1.03 - Modelling with Symmetric Nets (pdf)

  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.

  ...more

  

  ---

• September 30, 2015S1.04 - The ReachabilityGraph for Symmetric Nets Analysis

  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.

  ...more

  

  ---

• September 30, 2015S1.04 - The ReachabilityGraph for Symmetric Nets Analysis (pdf)

  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.

  ...more

  

  ---

• September 30, 2015S1.05 - LTL 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.

  ...more

  

  ---

• September 30, 2015S1.05 - LTL Properties (pdf)

  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.

  ...more

  

  ---