---
res:
bibo_abstract:
- One source of complexity in the μ-calculus is its ability to specify an unbounded
number of switches between universal (AX) and existential (EX) branching modes.
We therefore study the problems of satisfiability, validity, model checking, and
implication for the universal and existential fragments of the μ-calculus, in
which only one branching mode is allowed. The universal fragment is rich enough
to express most specifications of interest, and therefore improved algorithms
are of practical importance. We show that while the satisfiability and validity
problems become indeed simpler for the existential and universal fragments, this
is, unfortunately, not the case for model checking and implication. We also show
the corresponding results for the alternation-free fragment of the μ-calculus,
where no alternations between least and greatest fixed points are allowed. Our
results imply that efforts to find a polynomial-time model-checking algorithm
for the μ-calculus can be replaced by efforts to find such an algorithm for the
universal or existential fragment.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Orna
foaf_name: Kupferman, Orna
foaf_surname: Kupferman
- foaf_Person:
foaf_givenName: Ritankar
foaf_name: Majumdar, Ritankar S
foaf_surname: Majumdar
bibo_doi: 10.1016/j.tcs.2005.11.015
bibo_issue: '2'
bibo_volume: 354
dct_date: 2006^xs_gYear
dct_publisher: Elsevier@
dct_title: On the universal and existential fragments of the mu-calculus@
...