Adding A/Sync Places to the Synthesis Procedure for Whole-Place Operations Nets with Localities

Scientific Annals of Computer Science

article

J. Kleijn¹  M. Koutny²  M. Pietkiewicz-Koutny² 

[1] Leiden Institute of Advanced Computer Science, Leiden University;School of Computing, Newcastle University

关键词: concurrency;    theory of regions;    transition system;    synthesis problem;    Petri net;    step semantics;    locality;    whole-place operations;    synchronous and asynchronous communication;    a/sync places;   

DOI  :  10.7561/SACS.2017.2.177

来源: Alexandru Ioan Cuza University of Iasi

【 摘 要 】

Assuming that the behavioural specification of a concurrent system is given in the form of a step transition system, where the arcs between states are labelled by steps (multisets of executed actions), we focus on the problem of synthesising a Petri net generating a reachability graph isomorphic to a given step transition system. To deal with step transition systems more complicated than those generated by standard Place/Transition nets, we consider in this paper Petri nets with wholeplace operations, localities, and a/sync places. We adapt and extend the general approach developed within the framework of τ -nets and the theory of regions of step transition systems. Building on the results presented in [23], emphasis here is on the role of a/sync places with their potential for an instantaneous transfer of tokens within a step. In a series of results we demonstrate the robustness of the notion of region for Petri net synthesis.

【 授权许可】

CC BY-ND