Three notes on the complexity of model checking fixpoint logic with chop

Martin Lange

RAIRO - Theoretical Informatics and Applications (2007)

  • Volume: 41, Issue: 2, page 177-190
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Lange, Martin. "Three notes on the complexity of model checking fixpoint logic with chop." RAIRO - Theoretical Informatics and Applications 41.2 (2007): 177-190. <http://eudml.org/doc/250076>.

@article{Lange2007,
abstract = { 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. },
author = {Lange, Martin},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Model checking; games; EXPTIME-complete; model checking; mu-calculus; fixpoint calculus with Chop; complexity},
language = {eng},
month = {7},
number = {2},
pages = {177-190},
publisher = {EDP Sciences},
title = {Three notes on the complexity of model checking fixpoint logic with chop},
url = {http://eudml.org/doc/250076},
volume = {41},
year = {2007},
}

TY - JOUR
AU - Lange, Martin
TI - Three notes on the complexity of model checking fixpoint logic with chop
JO - RAIRO - Theoretical Informatics and Applications
DA - 2007/7//
PB - EDP Sciences
VL - 41
IS - 2
SP - 177
EP - 190
AB - 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.
LA - eng
KW - Model checking; games; EXPTIME-complete; model checking; mu-calculus; fixpoint calculus with Chop; complexity
UR - http://eudml.org/doc/250076
ER -

References

top
  1. H. Békic, Programming Languages and Their Definition, Selected Papers. Lect. Notes Comput. Sci. 177 (1984).  
  2. A. Browne, E.M. Clarke, S. Jha, D.E. Long and W. Marrero, An improved algorithm for the evaluation of fixpoint expressions. TCS178 (1997) 237–255.  
  3. R. Cleaveland, Tableau-based model checking in the propositional µ-calculus. Acta Informatica27 (1990) 725–748.  
  4. A. Dawar, E. Grädel and S. Kreutzer, Inflationary fixed points in modal logic, in Proc. 15th Workshop on Computer Science Logic, CSL'01, edited by L. Fribourg, Paris, France. Lect. Notes Comput. Sci. 277–291 (2001).  
  5. S. Dziembowski, M. Jurdziński and D. Niwiński, On the expression complexity of the modal µ-calculus model checking. Unpublished manuscript (1996).  
  6. E.A. Emerson and C.S. Jutla, Tree automata, µ-calculus and determinacy, in Proc. 32nd Symp. on Foundations of Computer Science, San Juan, Puerto Rico 368–377 (1991). IEEE.  
  7. E.A. Emerson, C.S. Jutla and A.P. Sistla, On model-checking for fragments of µ-calculus, in Proc. 5th Conf. on Computer Aided Verification, CAV'93. Lect. Notes Comput. Sci.697 (1993) 385–396.  
  8. E. Grädel, W. Thomas and Th. Wilke, Eds. Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. (2002).  
  9. D. Janin and I. Walukiewicz, On the expressive completeness of the propositional µ-calculus with respect to monadic second order logic, in Proc. 7th Conf. on Concurrency Theory, CONCUR'96, edited by U. Montanari and V. Sassone, Pisa, Italy. Lect. Notes Comput. Sci.1119 (1996) 263–277.  
  10. M. Jurdziński, Deciding the winner in parity games is in UP∩co-UP. Inform. Process. Lett.68 (1998) 119–124.  
  11. M. Jurdziński, Small progress measures for solving parity games, in Proc. 17th Ann. Symp. on Theoretical Aspects of Computer Science, STACS'00, edited by H. Reichel and S. Tison. Lect. Notes Comput. Sci.1770 (2000) 290–301.  
  12. D. Kozen, Results on the propositional µ-calculus. TCS27 (1983) 333–354.  
  13. M. Lange, Alternating context-free languages and linear time µ-calculus with sequential composition, in Proc. 9th Workshop on Expressiveness in Concurrency, EXPRESS'02, edited by P. Panangaden and U. Nestmann, Brno, Czech Republic, Elsevier. ENTCS68.2 (2002) 71–87.  
  14. M. Lange, Local model checking games for fixed point logic with chop, in Proc. 13th Conf. on Concurrency Theory, CONCUR'02, edited by L. Brim, P. Jančar, M. Křetínský and A. Kučera, Brno, Czech Republic. Lect. Notes Comput. Sci.2421 (2002) 240–254.  
  15. M. Lange and R. Somla, The complexity of model checking higher order fixpoint logic, in Proc. 30th Int. Symp. on Math. Foundations of Computer Science, MFCS'05, edited by J. Jedrzejowicz and A. Szepietowski, Gdansk, Poland. Lect. Notes Comput. Sci.3618 (2005) 640–651.  
  16. M. Lange and C. Stirling, Model checking fixed point logic with chop, in Proc. 5th Conf. on Foundations of Software Science and Computation Structures, FOSSACS'02, edited by M. Nielsen and U. H. Engberg, Grenoble, France. Lect. Notes Comput. Sci.2303 (2002) 250–263.  
  17. M. Müller-Olm, A modal fixpoint logic with chop, in Proc. 16th Symp. on Theoretical Aspects of Computer Science, STACS'99, edited by C. Meinel and S. Tison, Trier, Germany. Lect. Notes Comput. Sci.1563 (1999) 510–520.  
  18. H. Seidl, Fast and simple nested fixpoint. Inform. Process. Lett.59 (1996) 303–308.  
  19. C. Stirling, Local model checking games, in Proc. 6th Conf. on Concurrency Theory, CONCUR'95, edited by I. Lee and S. A. Smolka, Berlin, Germany. Lect. Notes Comput. Sci.962 (1995) 1–11.  
  20. M. Viswanathan and R. Viswanathan, A higher order modal fixed point logic, in Proc. 15th Int. Conf. on Concurrency Theory, CONCUR'04, edited by Ph. Gardner and N. Yoshida, London, UK. Lect. Notes Comput. Sci.3170 (2004) 512–528.  
  21. I. Walukiewicz, Pushdown processes: Games and model-checking. Inform. Comput.164 (2001) 234–263.  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.