PAIS LAB seminar: Petri Net Transformations - Abstraction, Refinement, Morphisms

Speaker: Roman Nesterov, Research Assistant, Postgraduate Student and Lecturer at the Faculty of Computer Science

 

Abstract. 

The second part of this talk will mainly cover properties of refinement transformations.

The use of Petri net transformations makes the verification of concurrent systems easier. On the one hand, starting from a sophisticated model, one may apply reduction transformations that preserve properties of the initial model and verify necessary properties on a transformed abstract model. On the other hand, having a simple model, it is possible to apply refinement transformations that yield a more complicated model reflecting properties of an initial abstract model.

Abstraction/refinement relations between Petri net models can be formalized in several ways, one of which is based on morphisms allowing to substitute places with subnets or to collapse subnets to a single place in Petri nets.

This talk will present several abstraction/refinement transformations that helps to systematically construct these morphisms. We will discuss properties and limitations of the proposed transformations and how they are related to the transformations already existing in the literature.

  

Location: room R 407, Pokrovsky Boulevard, 11

Seminar working language – English