Regions of Petri nets with a/sync connections (2012)

Author(s): Kleijn J, Koutny M, Pietkiewicz-Koutny M

    Abstract: Automated synthesis from behavioural specifications,such as transition systems,is an attractive way of constructing correct concurrent systems.In this paper, we investigate the synthesisof Petri nets which use special connectionsbetween transitions and places.Along these a/sync connections tokens can be transferredinstantaneously between transitions executed in a single step.We show that for Place/Transition nets with a/sync connectionsthe synthesis problem can be treatedwithin the general approach based on regions ofstep transition systems.We also show that the problem is decidablefor finite transition systems, and outlinea suitable construction algorithm.

      • Date: 21-04-2012
      • Journal: Theoretical Computer Science
      • Volume: 454
      • Pages: 189-198
      • Publisher: Elsevier BV
      • Publication type: Article
      • Bibliographic status: Published

      Keywords: concurrency, transition system, Petri net, theory of regions, synthesis problem, place transition net, step sequence semantics, synchronous and asynchronous communication, a/sync connection

      Staff

      Professor Maciej Koutny
      Professor of Computing Science

      Dr Marta Pietkiewicz-Koutny
      Lecturer