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

• September 30, 2015S1.06 - CTL Properties

  Another logic allows for expressing properties on a tree of possible futures: CTL (Computational Tree Logic) properties.

  ...more

  

  ---

• September 30, 2015S1.06 - CTL Properties (pdf)

  Another logic allows for expressing properties on a tree of possible futures: CTL (Computational Tree Logic) properties.

  ...more

  

  ---

• September 30, 2015S2.01 - Introduction to CosyVerif

  This short session is an introduction to practicals with the CosyVerif verification platform. It briefly introduces the

  underlying principles, the technical requirements for the installation, which are necessary to do the exercises.

  ...more

  

  ---

• September 30, 2015S2.01 - Introduction to CosyVerif (pdf)

  This short session is an introduction to practicals with the CosyVerif verification platform. It briefly introduces the

  underlying principles, the technical requirements for the installation, which are necessary to do the exercises.

  ...more

  

  ---

• September 30, 2015S3.01- Symmetries in Symmetric Nets

  This short sequence starts with a general overview of the last part of the tutorial. Then, the most essential feature

  of Symmetric Nets is presented through the running example. It exhibits the intrinsic symmetries of both markings and

  firings in such models.

  ...more

  

  ---

• September 30, 2015S3.01- Symmetries in Symmetric Nets

  This short sequence starts with a general overview of the last part of the tutorial. Then, the most essential feature

  of Symmetric Nets is presented through the running example. It exhibits the intrinsic symmetries of both markings and

  firings in such models.

  ...more

  

  ---

• September 30, 2015S3.02 - Symmetries to Reduce the Reachability Graph

  In this sequence, symmetries of both markings and firings are formally defined. Symmetries are a powerful tool to

  reduce the size of the reachability graph, thus making it amenable.

  ...more

  

  ---

• September 30, 2015S3.02 - Symmetries to Reduce the Reachability Graph (pdf)

  In this sequence, symmetries of both markings and firings are formally defined. Symmetries are a powerful tool to

  reduce the size of the reachability graph, thus making it amenable.

  ...more

  

  ---

• September 30, 2015S3.03 - Dynamic Subclasses and Symbolic Markings

  The next step towards the definition of the reduced graph consists in defining subclasses of markings as well as

  symbolic markings, that represent a complete subclass.

  ...more

  

  ---

• September 30, 2015S3.03 - Dynamic Subclasses and Symbolic Markings (pdf)

  The next step towards the definition of the reduced graph consists in defining subclasses of markings as well as

  symbolic markings, that represent a complete subclass.

  ...more

  

  ---