Mso logic and the partial order semantics of place/transition-nets

Abstract

In this work, we study the interplay between monadic second order logic and the partial order theory of bounded place/transition-nets. First, we show that the causal behavior of any bounded p/t-net can be compared with respect to inclusion with the set of partial orders specified by a given MSO sentence ϕ. Subsequently, we address the synthesis of Petri nets from MSO specifications. More precisely, we show that given any MSO sentence ϕ, one can automatically construct a bounded Petri net whose behaviour minimally includes the set of partial orders specified by ϕ. Combining this synthesis result with the comparability results we study three problems in the realm of automated correction of faulty Petri nets, and show that these problems are decidable.