From Symmetric Nets to Symmetric Nets with Bags

Follow From Symmetric Nets to Symmetric Nets with Bags
Share on
Copy link to clipboard

Nowadays, systems tend to be more and more distributed. Distribution brings a huge complexity and a strong need to deduce possible (good and bad) behaviors on the global system, from the known behavior of its actors. For such systems, we know that classical development methods are not adequate since…

Fabrice Kordon


    • Oct 8, 2014 LATEST EPISODE
    • infrequent NEW EPISODES
    • 10m AVG DURATION
    • 38 EPISODES


    More podcasts from Fabrice Kordon

    Search for episodes from From Symmetric Nets to Symmetric Nets with Bags with a specific topic:

    Latest episodes from From Symmetric Nets to Symmetric Nets with Bags

    3.11 - Second Example of SNB

    Play Episode Listen Later Oct 8, 2014 15:59


    To complete the presentation of Symmetric nets with bags, a more advanced example is presented.

    3.11 - Second Example of SNB (PDF)

    Play Episode Listen Later Oct 8, 2014


    To complete the presentation of Symmetric nets with bags, a more advanced example is presented.

    3.10 - Functions Used in SBN and Firing Rule

    Play Episode Listen Later Oct 8, 2014 8:48


    Since Symmetric Nets with Bags allow for manipulating bags of values, they make use of new functions on colours and on bags in their firing rule. These functions are explained and examplified.

    3.10 - Functions Used in SBN and Firing Rule (PDF)

    Play Episode Listen Later Oct 8, 2014


    Since Symmetric Nets with Bags allow for manipulating bags of values, they make use of new functions on colours and on bags in their firing rule. These functions are explained and examplified.

    3.09 - Symmetric Nets with Bags

    Play Episode Listen Later Oct 8, 2014 9:13


    Models can be made easier to describe by enhancing parametrisation and reducing interleaving. To do so, Symmetric Nets with Bags are introduced, that allow for manipulating bags of values instead of individual values.

    3.09 - Symmetric Nets with Bags (PDF)

    Play Episode Listen Later Oct 8, 2014


    Models can be made easier to describe by enhancing parametrisation and reducing interleaving. To do so, Symmetric Nets with Bags are introduced, that allow for manipulating bags of values instead of individual values.

    3.08 - SN and Partial Symmetries

    Play Episode Listen Later Oct 8, 2014 9:26


    When these elements are so distinct that they show only individual behaviour, partial symmetries, as presented in this sequence, must be used to reduce the Symbolic Reachability Graph.

    3.08 - SN and Partial Symmetries (PDF)

    Play Episode Listen Later Oct 8, 2014


    When these elements are so distinct that they show only individual behaviour, partial symmetries, as presented in this sequence, must be used to reduce the Symbolic Reachability Graph.

    3.07 - Static Subclasses

    Play Episode Listen Later Oct 8, 2014 11:38


    This approach of Symbolic Reachability Graph is further improved by defining static subclasses, where all elements within a same subclass have the same behaviour.

    3.07 - Static Subclasses (PDF)

    Play Episode Listen Later Oct 8, 2014


    This approach of Symbolic Reachability Graph is further improved by defining static subclasses, where all elements within a same subclass have the same behaviour.

    3.06 - The Symbolic Reachability Graph

    Play Episode Listen Later Oct 8, 2014 8:18


    The previous sequences have set all the basis necessary for the construction of the Symbolic Reachability Graph. It takes advantage of the symmetry between markings, and between firings, so as to study the behaviour at a symbolic level.

    3.06 - The Symbolic Reachability Graph (PDF)

    Play Episode Listen Later Oct 8, 2014


    The previous sequences have set all the basis necessary for the construction of the Symbolic Reachability Graph. It takes advantage of the symmetry between markings, and between firings, so as to study the behaviour at a symbolic level.

    3.05 - Symbolic Firing Rule

    Play Episode Listen Later Oct 8, 2014 3:47


    In order to express the behaviour of the system between symbolic markings, a similar approach is necessary, thus defining a symbolic firing rule.

    3.05 - Symbolic Firing Rule (PDF)

    Play Episode Listen Later Oct 8, 2014


    In order to express the behaviour of the system between symbolic markings, a similar approach is necessary, thus defining a symbolic firing rule.

    3.04 - Dynamic Subclasses and Symbolic Markings

    Play Episode Listen Later Oct 8, 2014 6:54


    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.

    3.04 - Dynamic Subclasses and Symbolic Markings (PDF)

    Play Episode Listen Later Oct 8, 2014


    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.

    3.03 - Symmetries to Reduce the Reachability Graph of SN (PDF)

    Play Episode Listen Later Oct 8, 2014


    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.

    3.03 - Symmetries to Reduce the Reachability Graph of SN

    Play Episode Listen Later Oct 8, 2014 10:11


    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.

    3.02 - Global vs Local Symmetries

    Play Episode Listen Later Oct 8, 2014 9:33


    In this sequence, 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.

    3.02 - Global vs Local Symmetries (PDF)

    Play Episode Listen Later Oct 8, 2014


    In this sequence, 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.

    3.01 - Opening

    Play Episode Listen Later Oct 8, 2014 0:58


    This short sequence is a general overview of the last part of the tutorial.

    3.01 - Opening (PDF)

    Play Episode Listen Later Oct 8, 2014


    This short sequence is a general overview of the last part of the tutorial.

    2.01 - Introduction to Practical Work

    Play Episode Listen Later Oct 8, 2014 11:59


    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.

    2.01 - Introduction to Practical Work (PDF)

    Play Episode Listen Later Oct 8, 2014


    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.

    1.07 - CTL properties

    Play Episode Listen Later Oct 8, 2014 14:16


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

    1.07 - CTL properties (PDF)

    Play Episode Listen Later Oct 8, 2014


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

    1.06 - LTL properties

    Play Episode Listen Later Oct 8, 2014 11:46


    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.

    1.06 - LTL properties (PDF)

    Play Episode Listen Later Oct 8, 2014


    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.

    1.05 - The reachability graph for SN analysis

    Play Episode Listen Later Oct 8, 2014 12:31


    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.

    1.05 - The reachability graph for SN analysis (PDF)

    Play Episode Listen Later Oct 8, 2014


    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.

    1.04 - Modelling with Symmetric Nets (PDF)

    Play Episode Listen Later Oct 8, 2014


    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.

    1.04 - Modelling with Symmetric Nets

    Play Episode Listen Later Oct 8, 2014 7:27


    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.

    1.03 - Syntax and semantics of SN

    Play Episode Listen Later Oct 8, 2014 22:50


    The syntax and semantics of Symmetric nets are defined, 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.

    1.03 - Syntax and semantics of SN (PDF)

    Play Episode Listen Later Oct 8, 2014


    The syntax and semantics of Symmetric nets are defined, 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.

    1.02 - Introduction

    Play Episode Listen Later Oct 8, 2014 14:58


    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.

    1.02 - Introduction (PDF)

    Play Episode Listen Later Oct 8, 2014


    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.

    1.01 - Opening

    Play Episode Listen Later Oct 8, 2014 2:21


    This short sequence is a general overview of the tutorial, and more specifically of the first part.

    1.01 - Opening (PDF)

    Play Episode Listen Later Oct 8, 2014


    This short sequence is a general overview of the tutorial, and more specifically of the first part.

    Claim From Symmetric Nets to Symmetric Nets with Bags

    In order to claim this podcast we'll send an email to with a verification link. Simply click the link and you will be able to edit tags, request a refresh, and other features to take control of your podcast page!

    Claim Cancel