Geodesic
Three notes on the complexity of model checking fixpoint logic with chop
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 41 (2007) no. 2, pp. 177-190

Voir la notice de l'article provenant de la source Numdam

This paper analyses the complexity of model checking fixpoint logic with Chop - an extension of the modal μ-calculus with a sequential composition operator. It uses two known game-based characterisations to derive the following results: the combined model checking complexity as well as the data complexity of FLC are EXPTIME-complete. This is already the case for its alternation-free fragment. The expression complexity of FLC is trivially P-hard and limited from above by the complexity of solving a parity game, i.e. in UP∩co-UP. For any fragment of fixed alternation depth, in particular alternation- free formulas it is P-complete.

DOI : 10.1051/ita:2007011
Classification : 03B44, 68Q17, 68Q60
Keywords: model checking, games, EXPTIME-complete 
@article{ITA_2007__41_2_177_0,
     author = {Lange, Martin},
     title = {Three notes on the complexity of model checking fixpoint logic with chop},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {177--190},
     publisher = {EDP-Sciences},
     volume = {41},
     number = {2},
     year = {2007},
     doi = {10.1051/ita:2007011},
     mrnumber = {2350643},
     zbl = {1133.68046},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.1051/ita:2007011/}
}
TY  - JOUR
AU  - Lange, Martin
TI  - Three notes on the complexity of model checking fixpoint logic with chop
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2007
SP  - 177
EP  - 190
VL  - 41
IS  - 2
PB  - EDP-Sciences
UR  - http://geodesic.mathdoc.fr/articles/10.1051/ita:2007011/
DO  - 10.1051/ita:2007011
LA  - en
ID  - ITA_2007__41_2_177_0
ER  - 
%0 Journal Article
%A Lange, Martin
%T Three notes on the complexity of model checking fixpoint logic with chop
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2007
%P 177-190
%V 41
%N 2
%I EDP-Sciences
%U http://geodesic.mathdoc.fr/articles/10.1051/ita:2007011/
%R 10.1051/ita:2007011
%G en
%F ITA_2007__41_2_177_0
Lange, Martin. Three notes on the complexity of model checking fixpoint logic with chop. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 41 (2007) no. 2, pp. 177-190. doi: 10.1051/ita:2007011

Cité par Sources :