Regions of Petri nets with a/sync connections
Automated synthesis from behavioural specifications, such as transition systems, 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 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. We also show that the problem is decidable for finite transition systems, and outline a suitable construction algorithm. (C) 2012 Elsevier B.V. All rights reserved.
petri net a/sync connection transition system concurrency synthesis problem theory of regions place transition net step sequence semantics synchronous and asynchronous communication