---
_id: '4466'
abstract:
- lang: eng
  text: 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 alternationfree 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.
acknowledgement: This work was supported in part by NSF grant CCR-9988172, the AFOSR
  MURI grant F49620-00-1-0327, and a Microsoft Research Fellowship.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments
    of the mu-calculus. In: <i>Proceedings of the 9th International Conference on
    Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 2619.
    Springer; 2003:49-64. doi:<a href="https://doi.org/10.1007/3-540-36577-X_5">10.1007/3-540-36577-X_5</a>'
  apa: 'Henzinger, T. A., Kupferman, O., &#38; Majumdar, R. (2003). On the universal
    and existential fragments of the mu-calculus. In <i>Proceedings of the 9th International
    Conference on Tools and Algorithms for the Construction and Analysis of Systems
    </i> (Vol. 2619, pp. 49–64). Warsaw, Poland: Springer. <a href="https://doi.org/10.1007/3-540-36577-X_5">https://doi.org/10.1007/3-540-36577-X_5</a>'
  chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
    and Existential Fragments of the Mu-Calculus.” In <i>Proceedings of the 9th International
    Conference on Tools and Algorithms for the Construction and Analysis of Systems
    </i>, 2619:49–64. Springer, 2003. <a href="https://doi.org/10.1007/3-540-36577-X_5">https://doi.org/10.1007/3-540-36577-X_5</a>.
  ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
    fragments of the mu-calculus,” in <i>Proceedings of the 9th International Conference
    on Tools and Algorithms for the Construction and Analysis of Systems </i>, Warsaw,
    Poland, 2003, vol. 2619, pp. 49–64.
  ista: 'Henzinger TA, Kupferman O, Majumdar R. 2003. On the universal and existential
    fragments of the mu-calculus. Proceedings of the 9th International Conference
    on Tools and Algorithms for the Construction and Analysis of Systems . TACAS:
    Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.
    2619, 49–64.'
  mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of
    the Mu-Calculus.” <i>Proceedings of the 9th International Conference on Tools
    and Algorithms for the Construction and Analysis of Systems </i>, vol. 2619, Springer,
    2003, pp. 49–64, doi:<a href="https://doi.org/10.1007/3-540-36577-X_5">10.1007/3-540-36577-X_5</a>.
  short: T.A. Henzinger, O. Kupferman, R. Majumdar, in:, Proceedings of the 9th International
    Conference on Tools and Algorithms for the Construction and Analysis of Systems
    , Springer, 2003, pp. 49–64.
conference:
  end_date: 2003-04-11
  location: Warsaw, Poland
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2003-04-07
date_created: 2018-12-11T12:08:59Z
date_published: 2003-03-14T00:00:00Z
date_updated: 2024-01-08T13:17:35Z
day: '14'
doi: 10.1007/3-540-36577-X_5
extern: '1'
intvolume: '      2619'
language:
- iso: eng
month: '03'
oa_version: None
page: 49 - 64
publication: 'Proceedings of the 9th International Conference on Tools and Algorithms
  for the Construction and Analysis of Systems '
publication_identifier:
  isbn:
  - '9783540008989'
publication_status: published
publisher: Springer
publist_id: '263'
quality_controlled: '1'
status: public
title: On the universal and existential fragments of the mu-calculus
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2619
year: '2003'
...