Synthesis of Petri nets with localities

Automated synthesis from behavioural specifications is an attractive way of constructing computational systems. In this paper, we look at a specific instance of this approach which aims at constructing GALS (globally asynchronous locally synchronous) systems. GALS systems are represented by Petri nets with localities, each locality defining a set of co-located actions, and specifications are given in terms of transition systems with arcs …