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

17.06 Object-Centric Replay-Based Conformance Checking: Unveiling Desire Lines and Local Deviations

Speaker: Julio Cesar Carrasquel Gamez, PAIS Lab Research Assistant 

Conformance checking methods diagnose whether a process, as observed in an event log, complies with its specification model, e.g., a Petri net. Most of these methods, however, check process instances (cases) individually, neglecting the interaction of such instances in a system. This limitation has been addressed in other areas of process mining by object-centric approaches. These approaches make use of Petri net extensions to model and analyze overlapping instances that are centered on the handling of objects. For instance, some of these approaches were recently presented at the PAIS Lab's seminar series "Wednesday Nights of Petri Nets and Their Extensions". Thus, for example, Fahland's synchronous proclets allow to describe the communication of multiple workflows, van der Aalst's object-centric nets can be discovered from logs where events have multiple case identifiers, whereas Rivkin and van der Werf propose formalisms to verify the interplay between processes and object-persistence models such as databases.

Inspired by the object-centric paradigm, we thus present in this talk a replay-based conformance method using conservative workflow colored nets. This model allows to describe the expected behavior of a system composed by end-to-end processes handling individual objects. Notably, when replaying an event log on top of our model, we consider a jump strategy where tokens representing objects move from their current location to input places of a transition to fire. Token jumps allow to unveil "desire lines", i.e., object paths unforeseen in the specification model. We introduce local conformance metrics based on the proportion of jumps in specific model components. The metrics allow to measure the magnitude of non-compliance in precise parts of a system. Supported by an implementation of our method, we present a practical example based on trading systems, where orders from users are matched to trade. Finally, we compare our approach with other well-known conformance methods.

Цикл семинаров Wednesday Nights of Petri Nets and their Extensions (WN-PNE) с 3 февраля по 21 апреля.

Year 2021 has started… And it also seems that the COVID-19 pandemic will keep on raging all around the world for quite a bit. With that much of uncertainty, why not to spend lockdown evenings with a cup of warm tea and in the company of world-class researchers?  

Petri nets have been at the core of concurrency for more than 50 years. Many valuable, foundational properties were discovered for ordinary P/T-nets, in turn allowing them to be used for modelling and analysing complex systems. At the same time, ordinary P/T-nets are not expressive enough to attack concrete theoretical and industrial problems. This pushes both researchers and practitioners towards finding extensions that suit better their tasks.

WN-PNE is a virtual event that brings together Petri net researches and enthusiasts from all around the world working on the theory and practice of Petri nets and their extensions (data-aware, multi-agent, algebraic/logic, time etc.). The focus of the event is to present ongoing research as well as more foundational contributions to the domain, and provide opportunities for discussion on possible future developments. We also hope that WN-PNE will inspire young researchers and help to foster new collaborations.

Подробности - на сайте WN-PNE.

16.12 On the membership problem for finite automata over symmetric groups

Speaker: Arthur Khashaev, Moscow State University.

We consider automata in which transitions are labeled with arbitrary permutations. The language of such an automaton consists of composition of permutations on all possible accepting computation paths. The membership problem for finite automata over symmetric group is the decision problem, where for a given automaton and a permutation it is asked whether the permutation belongs to the language of the automaton. It is shown that this problem is NP-complete, regardless of whether the automaton is acyclic. We also propose an efficient algorithm for the case of strongly connected automata.

03.11-04.11 XI Workshop "Program Semantics, Specification and Verification: Theory and Applications" PSSV-2020

3 и 4 ноября состоится 11-й ежегодный воркшоп "Program Semantics, Specification and Verification: Theory and Applications" (PSSV 2020). 

Среди тем для обсуждения:

• formalisms for program semantics;
• formal models and semantics of programs and systems;
• semantics of programming and specification languages;
• formal description techniques;
• logics for formal specification and verification;
• deductive program verification etc.

С программой и расписанием можно ознакомиться на сайте воркшопа

Воркшоп проводится при организационной поддержке лаборатории ПОИС факультета компьютерных наук.

20.10 Robustness measure for active management of collective investments

Speaker: Aliya Sharipova, PAIS Lab Research Fellow.

A practical approach to estimating of the investment strategy robustness is considered. As a quantitative measure of robustness, the objective

function smoothness degree and measure of stability of a strategy are proposed for utilization. After the optimization has been conducted, it is essential to utilize an additional criterion for the selection of strategies that possess better robustness property. The utilization of the quantitative estimate of the strategy robustness enables a better strategy to be chosen in the efficiency analysis of collective investments management. 

14.10 Petri Nets with Parameterised Data: Modelling and Verification

Speaker: Andrey Rivkin, postdoctoral researcher, KRDB Research Center for Knowledge and Data, Free University of Bozen-Bolzano.

During the last decade, various approaches have been put forward to integrate business processes with different types of data. Each of these approaches reflects specific demands in the whole process-data integration spectrum. One particularly important point is the capability of these approaches to flexibly accommodate processes with multiple cases that need to co-evolve. In this work, we introduce and study an extension of coloured Petri nets, called catalog-nets, providing two key features to capture this type of processes. On the one hand, net transitions are equipped with guards that simultaneously inspect the content of tokens and query facts stored in a read-only, persistent database. On the other hand, such transitions can inject data into tokens by extracting relevant values from the database or by generating genuinely fresh ones. We systematically en- code catalog-nets into one of the reference frameworks for the (parameterised) verification of data and processes. We show that fresh-value injection is a particularly complex feature to handle, and discuss strategies to tame it. Finally, we discuss how catalog nets relate to well-known formalisms in this area.

22.09 О проблеме эквивалентности последовательных программ с процедурами

Докладчик – Казбекова Диана, стажер-исследователь НУЛ ПОИС.

Задача проверки эквивалентности программ -- одна из центральных проблем теории и практики программирования. Необходимость в решении этой задачи возникает при построении оптимизирующих компиляторов, трансляторов, а также в задачах верификации программ и обнаружения вредоносных фрагментов кода. Функциональная эквивалентность программ неразрешима, однако, существует более строгое отношение эквивалентности, аппроксимирующее функциональную эквивалентность. Для того чтобы проверять эквивалентность программ, нужно формализовать понятие программы. В докладе рассматриваются стандартные схемы программ и их логико-термальная эквивалентность. 

В модели стандартных схем программ отсутствует возможность вызова процедур. Предложена расширенная модель стандартных схем программ с процедурами, определено отношение логико-термальной эквивалентности, предложен метод построения формальных грамматик, порождающих логико-термальные истории. Таким образом, задача проверки логико-термальной эквивалентности программ сводится к задаче проверки эквивалентности формальных грамматик специального вида. 

08.09 Topological entropy as a tool for measuring precision, recall and simplicity of process models discovered from event logs

Speaker: Anna Kalenkova, Research Fellow, School of Computing and Information Systems, Melbourne School of Engineering, University of Melbourne, Australia.

Process models automatically discovered from event logs vary in their structure and behavior. To rank these models, entropy-based techniques can be applied. This presentation covers methods for the behavioral (1) and structural analysis (2) of automatically discovered process models basing on the notion of entropy. 

(1) Conformance checking techniques quantify the similarity between traces described in a process model and executed traces recorded in a corresponding event log. Recently, the process mining community has initiated a discussion on the desired properties of conformance checking measures [1]. The entropy-based conformance checking techniques fulfill the put forward properties providing a sound tool for assessing discrepancies between process models and event logs. In this presentation, the entropy-based methods for the exact [2] and partial [3] trace matching are discussed.

(2) Although various conformance checking techniques that relate the behavior of discovered models to the behavior recorded in event logs have been proposed, there are no methods for evaluating whether this behavior is represented in the simplest possible way. Existing techniques for measuring simplicity of discovered models focus on their structural characteristics such as size or density and ignore the behavior these models encoded. In this presentation, we discuss a conceptual framework [4] that can be instantiated into a concrete approach for estimating the simplicity of a model, considering the behavior the model describes, thus allowing a more holistic analysis. The evaluation over real-life event logs for several instantiations of the framework demonstrates its feasibility in practice.

[1] Syring, A., Tax, N., van der Aalst, W.: Evaluating conformance measures in process mining using conformance propositions. In: ToPNoC XIV. pp. 192–221. Springer (2019). 

[2] Polyvyanyy, A., Solti, A., Weidlich, M., Di Ciccio, C., Mendling, J.: Monotone precision and recall measures for comparing executions and specifications of dynamic systems. ACM Trans. Softw. Eng. Methodol. 29(3) (Jun 2020). 

[3] Polyvyanyy, A., Kalenkova, A.: Monotone conformance checking for partially matching designed and observed processes. In: ICPM. pp. 81–88. IEEE (2019). 

[4] A. Kalenkova, A. Polyvyanyy, and M. La Rosa, “A framework for estimating simplicity of automatically discovered process models based on structural and behavioral characteristics,” in BPM. Springer, 2020.