Rabin's theorem in the concurrency setting: a conjecture (Q2253187)

Rabin's theorem says that the monadic second-order theory of the infinite binary tree is decidable. A simple consequence is that for every finite state transition system, the monadic second-order theory of its computation tree is decidable. In concurrency theory, 1-safe Petri nets generalize finite state transition systems and labelled event structures are counterparts to computation trees. Unlike the sequential case, not every 1-safe Petri net, i.e., its event structure unfolding, has a decidable monadic second-order theory. This paper presents, as a conjecture, a characterisation of those 1-safe Petri nets that have a decidable monadic second-order theory and provides a number of arguments supporting this conjecture. The characterisation is based on a property of event structures coined grid-freeness, and the papers proves decidability of this property. It is shown that grid-freeness is a necessary condition for the decidability question mentioned above, whereas the sufficiency is left open. Finally, the paper shows that the claim of the conjecture implies decidability of several distributed controller synthesis problems.