Monadic second-order logic, graph coverings and unfoldings of transition systems (Q1295371)

Transition systems are directed graphs which can be regarded as abstract programs and then their unfoldings represent the behaviours of programs. When transition systems are defined as relational structures, monadic second-order (MSO) logic offers a natural formalism for expressing their properties. In an earlier paper, the first author conjectured that if the unfoldings of the transition systems of a class \(P\) are definable by an MSO formula, then \(P\) itself is also effectively MSO-definable. Here, the conjecture is proved for transition systems with countable outdegrees. The tools used in the proof include automata on infinite trees and coverings of transition systems. Such coverings, which are homomorphisms of graphs, are extensively studied from various points of view and they are also considered in the context of general directed graphs.