Model Checking and Higher-Order Recursion

Hungar, Hardi
Math. Found. of Comp. Sc.
Since Muller and Schupp have shown in 1985 that monadic second-order logic (MSOL) is decidable for context-free graphs, several specialized procedures have been developed for related problems, mostly for sublogics like the modal mu-calculus, or even its alternation-free fragment. This work shows the decidability of S1S, the trace version of MSOL, for the richer set of phmacro graphs. The generation mechanism of macro graphs is of higher-order nature and relates to the context-free one like macro grammars [Fischer, 1968] relate to context-free grammars. Technically, the result follows from the decidability of the emptiness problem of the trace language of a macro graph with fairness. The decision procedure is given in form of a tableau system. Soundness and completeness follow from the relation of the (finite) tableaux to their infinite unfoldings. This kind of proof promises to be helpful in the derivation of further results.
01 / 1999
LNCS 1672