AG 1, AG 2, AG 3, AG 4   Info

AG Audience

60 Minutes

Saarbrücken

Since Muller and Schupp have shown that monadic second-order logic (MSOL) is decidable for context-free graphs, several specialized procedures have beed developed for related problems, mostly for sublogics like the modal mu-calculus or even its alternation-free fragment. This talk presents the result that S1S, the trace version of MSOL, is decidable for the strictly richer set of macro graphs. The generation mechanism of macro graphs is a higher-order generalization of the context-free one.

Technically, the result follows from the decidabilitty of the emptiness problem of the trace language of a macro graph under a fairness constraint. 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 unfoldlings. This kind of proof promises to be helpful in the derivation of further results.

Tom Henzinger

301

--email hidden

passcode not visible

logged in users only