---
_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: Proceedings of the 9th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems . Vol 2619.
Springer; 2003:49-64. doi:10.1007/3-540-36577-X_5'
apa: 'Henzinger, T. A., Kupferman, O., & Majumdar, R. (2003). On the universal
and existential fragments of the mu-calculus. In Proceedings of the 9th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 2619, pp. 49–64). Warsaw, Poland: Springer. https://doi.org/10.1007/3-540-36577-X_5'
chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
and Existential Fragments of the Mu-Calculus.” In Proceedings of the 9th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
, 2619:49–64. Springer, 2003. https://doi.org/10.1007/3-540-36577-X_5.
ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
fragments of the mu-calculus,” in Proceedings of the 9th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems , 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.” Proceedings of the 9th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems , vol. 2619, Springer,
2003, pp. 49–64, doi:10.1007/3-540-36577-X_5.
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'
...