• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Семинары 2021-2022 уч.г.

21.01 Data Petri Nets as a Formalism for Representing Decision-Aware Process Models

Speaker: Nikolay Suvorov, PAIS Lab Research Assistant

In recent years, there has been an increasing interest in enriching the traditional control flow perspective of processes with additional dimensions. This report is focused on Data Petri nets (DPNs) which are a data aware extension of Petri nets where the net is enriched with data variables of different types, while transitions are guarded by formulae that inspect and update such variables. Such formalism provides a possibility to consider not only the control flow perspective of the process but also the dataflow perspective as well as the decisions made based on the data.

The report covers syntax and semantics of DPNs, techniques to discover DPNs from the event data, ways to perform conformance checking on models represented as DPNs and different algorithms to check soundness of DPNs.

2022 год

15.09 Overview of real-time models

Speaker: Evgenii Vinarskii, PAIS Lab Research Assistant 

This presentation is devoted to the current deals in studying real-time models. We consider the classical Timed Automaton (TA) model. Then we move to the Timed Finite State Machines (TFSM) model. There are three main TFSM models: (i) TFSM with timed guards, (ii) TFSM with timeouts (iii) TFSM with timed guards and timeouts. We consider equivalence relation between various real-time models and bisimulation relation between timed and untimed models.

08.09 Studying the properties of timed finite state machines

Speaker: Evgenii Vinarskii, PAIS Lab Research Assistant 

Sequential reactive systems are formal models of programs that interact with the environment by receiving inputs and producing corresponding outputs. The behavior of a reactive system depends not only on the flow of input data, but also on the time the input data arrive and the delays that occur when generating responses. To capture these aspects, a timed finite state machine (TFSM) is used. TFSM is an extension of finite state machine (FSM) which is used for modelling and analysis of real-time reactive systems. 

This presentation is devoted to refined semantics ofTFSMs, this gives us an opportunity to model more complex real-time systems.For example, we show how to represent the behavior of Software Defined Networking (SDN) Controller via TFSM. Then we discuss how the verification methods for the refined TFSM change compared with classical one.


 

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!
Сервис предназначен только для отправки сообщений об орфографических и пунктуационных ошибках.