Modular Automata 2 Distributed Petri Nets 4 Synthesis

Modular automata are symbolic transition systems halfway between families of automata and their synchronized products. They allow for analysis of liveness properties without incurring the state space explosion problem. A modular automaton is composed of modules and a synchronization graph. We consider the problem whether such specifications may be implemented by a distributed Petri net up to language equivalence. The challenge is to avoid computing the state space of the modular automaton to be implemented. We show that this is possible, opening the way to the synthesis of nets from modular specifications