Causality in Bounded Petri Nets is MSO Definable

In this work we show that the causal behaviour of any bounded Petri net is definable in monadic second order MSO logic. Our proof relies in a definability vs recognizability result for DAGs whose edges and vertices can be covered by a constant number of paths. Our notion of recognizability is defined in terms of saturated slice automata, a formalism for the specification of infinite families of graphs. We show that a family $$\mathfrak {G}$$ of k-coverable DAGs is recognizable by a saturated slice automaton if and only if $$\mathfrak {G}$$ is definable in monadic second order logic. This result generalizes Buchi's theorem from the context of strings, to the context of k-coverable DAGs.