Dr. Kamila Barylska

Abstract:

The behavioural specification of a given concurrent system can be described in a form of a labelled transition system (lts). One of the challenging tasks of system analysis is to construct a model of a system with exactly the same behaviour. Region theory [1] provides a polynomial algorithm, based on solving linear inequations, that checks whether a given finite labelled transition system is the reachability graph of some place/transition Petri net [2], and if it is, synthesises one of them.

Unfortunately, since the lts may be extremely large, the process of synthesis may be remarkably time consuming, as it is based on solving a great amount of linear equations. It seems reasonable to investigate certain classes of labelled transition systems in hope of obtaining more efficient (and also deterministic) algorithm of solving them, or at least of deciding whether a given lts is synthesizable.

For some applications, only certain types of labelled transition systems are relevant. This leads to the idea of investigating properties of labelled transition systems before synthesising them, in the hope of obtaining more efficient and possibly also more deterministic synthesis algorithms. It may even be possible to find exact structural characterisations, based solely on graph-theoretical properties.

That is why we make an effort on characterising the set of finite words over a binary alphabet, which are Petri net solvable, i.e., for which a place/transition net with an isomorphic reachability graph exists. The talk describes results concerning properties of binary Petri net solvable and unsolvable words along with some conjectures confirmed by computer experiments.

References:

[1] E. Badouel, P. Darondeau: Theory of Regions. In W. Reisig, G. Rozenberg (eds): Lectures on Petri Nets I: Basic Models. LNCS Vol. 1491, 529–586 (1998).

[2] T. Murata: Petri Nets: Properties, Analysis and Applications. Proc. of the IEEE, Vol. 77(4), 541-580 (1989).

(Joint work with Eike Best, Evgeny Erofeev, Łukasz Mikulski, Marcin Piątkowski)