Computing Science. Regions of Petri Nets with a/sync Connections

摘要

Automated synthesis from behavioural specifications, is an attractive way of constructing correct concurrent systems. In this paper, we investigate the synthesis of Petri nets which use special connections between transitions and places. Along these a/sync connections tokens can be transferred instantaneously between two transitions executed in a single step. We show that for Place/Transition nets with a/sync connections the synthesis problem can be treated within the general approach based on regions of step transition systems. Moreover, we demonstrate that the problem is decidable for finite transition systems, and identify a subclass of nets for which a polynomial decision procedure and construction algorithm exists.