Affiliations: School of Computing Science, Newcastle University, Newcastle upon Tyne NE1 7RU, U.K. maciej.koutny@ncl.ac.uk, marta.koutny@ncl.ac.uk
Note: [] Address for correspondence: School of Computing Science, Newcastle University, Newcastle upon Tyne NE1 7RU, U.K
Abstract: One of the possible ways of constructing concurrent systems is their automated synthesis from behavioural specifications. In this paper, we look at a particular instance of this approach which aims at constructing GALS (globally asynchronous locally synchronous) systems from specifications given in terms of transition systems with arcs labelled by steps of executed actions. GALS systems are represented by Elementary Net Systems with Localities (ENL-systems), each locality defining a set of co-located actions. The synthesis procedure is based on the regions of transition systems and we provide a number of criteria aimed at generating a minimal set of regions (conditions) of an ENL-system generating a given transition system.
Keywords: theory of concurrency, Petri nets, localities, analysis and synthesis, step sequence semantics, conflict, theory of regions, transition systems
