Algorithms for Synthesis and Pre-Synthesis Based on Petri Net Structure Theory (ASYST)

点击翻译按钮获取中文摘要

This project contributes to the theory of synthesising Petri nets from labelled transition systems, the basic concepts and algorithms underlying which have recently been described in a monography entitled Petri Net Synthesis (Springer-Verlag, 2015), by Badouel, Bernardinello, and Darondeau. Petri net synthesis is an actively researched, as well as a highly application-prone, topic. Probably, the most well-known areas of application are Asynchronous Digital Design and Process Mining. In both areas, the focus is on special Petri nets (choice-free nets, and marked graphs). For reasons such as this, it is important to optimise Petri net synthesis towards special classes of systems. Optimising with respect to various other classes of Petri nets is vital in order to pave the way for diverse other types of application.A general Petri net synthesis algorithm would involve solving a large number of linear-algebraic inequation systems. If solutions exist, then they can be used in order to construct so-called regions (that is, suitable structures relating to a given transition system). Targetting this algorithm towards specific system classes requires, in general, adding more linear inequation systems, which may slow down the synthesis. The aim of the present project is to demonstrate how established knowledge about the structural characteristics of the target classes can be used in order to offset the slow-down effect, and preferably, lead to better algorithms. It was already shown that, for marked graphs, there exists an algorithm by which only unavoidable regions are constructed very efficiently. In order to corroborate our aim for other Petri net classes as well, we shall investigate ways in which target class specific structural properties can be used in order to reduce the number of region constructions. A general method of incorporating such properties is to provide an explicit pre-synthesis stage during which they can be checked on a given input. The project aims -- inspired by a published, extensive, feasibility study for choice-free systems -- at proving that knowing structural properties before synthesis leads to a reduction of the amount of region construction and to a corresponding optimisation of synthesis.