We provide a characterization theorem, in the style of van Ben them and Janin-Walukiewicz, for the alternation-free fragment of the modal mu-calculus. For this purpose we introduce a variant of standard monadic second-order logic (MSO), which we call well-founded monadic second-order logic (WFMSO). When interpreted in a tree model, the second-order quantifiers of WFMSO range over subsets of conversely well-founded sub trees. The first main result of the paper states that the expressive power of WFMSO over trees exactly corresponds to that of weak MSO-Automata. Using this automata-theoretic characterization, we then show that, over the class of all transition structures, the bisimulation-invariant fragment of WFMSO is the alternation-free fragment of the modal mu-calculus. As a corollary, we find that the logics WFMSO and WMSO (weak monadic second-order logic, where second-order quantification concerns finite subsets), are incomparable in expressive power. © 2013 IEEE.
A Characterization Theorem for the Alternation-Free Fragment of the Modal μ-Calculus / Facchini A.; Venema Y.; Zanasi F.. - ELETTRONICO. - (2013), pp. 6571580.478-6571580.487. (Intervento presentato al convegno 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 tenutosi a New Orleans, LA, usa nel 2013) [10.1109/LICS.2013.54].
A Characterization Theorem for the Alternation-Free Fragment of the Modal μ-Calculus
Zanasi F.
Primo
2013
Abstract
We provide a characterization theorem, in the style of van Ben them and Janin-Walukiewicz, for the alternation-free fragment of the modal mu-calculus. For this purpose we introduce a variant of standard monadic second-order logic (MSO), which we call well-founded monadic second-order logic (WFMSO). When interpreted in a tree model, the second-order quantifiers of WFMSO range over subsets of conversely well-founded sub trees. The first main result of the paper states that the expressive power of WFMSO over trees exactly corresponds to that of weak MSO-Automata. Using this automata-theoretic characterization, we then show that, over the class of all transition structures, the bisimulation-invariant fragment of WFMSO is the alternation-free fragment of the modal mu-calculus. As a corollary, we find that the logics WFMSO and WMSO (weak monadic second-order logic, where second-order quantification concerns finite subsets), are incomparable in expressive power. © 2013 IEEE.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.