Skip to main content
SpringerLink
Log in

On the Model Checking of the Graded \(\mu \)-calculus on Trees

  • Conference paper
  • First Online:
Advances in Artificial Intelligence and Soft Computing (MICAI 2015)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9413))

Included in the following conference series:

Abstract

The \(\mu \)-calculus is an expressive propositional modal logic augmented with least and greatest fixed-points, and encompasses many temporal, program, dynamic and description logics. The model checking problem for the \(\mu \)-calculus is known to be in NP \(\cap \) Co-NP. In this paper, we study the model checking problem for the \(\mu \)-calculus extended with graded modalities. These constructors allow to express numerical constraints on the occurrence of accessible nodes (worlds) satisfying a certain formula. It is known that the model checking problem for the graded \(\mu \)-calculus with finite models is in EXPTIME. In the current work, we introduce a linear-time model checking algorithm for the graded \(\mu \)-calculus when models are finite unranked trees.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Grädel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, pp. 306–317. IEEE Computer Society (1997)

    Google Scholar 

  2. Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In Allen, J.F., Fikes, R., Sandewall, E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 335–346. Morgan Kaufmann (1991)

    Google Scholar 

  3. Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded \(\mu \)-calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 423–437. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The complexity of enriched mu-calculi. Logical Methods in Computer Science 4(3) (2008)

    Google Scholar 

  5. Bárcenas, E., Genevès, P., Layaïda, N., Schmitt, A.: Query reasoning on trees with types, interleaving, and counting. In: Walsh, T. (ed.) IJCAI. IJCAI/AAAI (2011)

    Google Scholar 

  6. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^20\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  7. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  8. Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343–352 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  9. Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model checking for the \({\mu }\)-calculus and its fragments. Theor. Comput. Sci. 258(1–2), 491–522 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  10. Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods Syst. Des. 2(2), 121–147 (1993)

    Article  MATH  Google Scholar 

  11. Calvanese, D., Giacomo, G.D., Lenzerini, M., Vardi, M.Y.: Node selection query languages for trees. In: Fox, M., Poole, D. (eds.) AAAI. AAAI Press (2010)

    Google Scholar 

  12. Ferrante, A., Murano, A., Parente, M.: Enriched \({\mu }\)-calculi module checking. Logical Methods in Computer Science 4(3) (2008)

    Google Scholar 

  13. Seidl, H., Schwentick, T., Muscholl, A.: Counting in trees. In Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata. Texts in Logic and Games, vol. 2, pp. 575–612. Amsterdam University Press (2008)

    Google Scholar 

  14. Demri, S., Lugiez, D.: Complexity of modal logics with Presburger constraints. J. Applied Logic 8(3), 233–252 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  15. Bianco, A., Mogavero, F., Murano, A.: Graded computation tree logic. ACM Trans. Comput. Log. 13(3), 25 (2012)

    Article  MathSciNet  Google Scholar 

  16. Bárcenas, E., Lavalle, J.: Expressive reasoning on tree structures: recursion, inverse programs, Presburger constraints and nominals. In: Castro, F., Gelbukh, A., González, M. (eds.) MICAI 2013, Part I. LNCS, vol. 8265, pp. 80–91. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Bárcenas, E., Lavalle, J.: Global numerical constraints on trees. Logical Methods in Computer Science 10(2) (2014)

    Google Scholar 

  18. Laroussinie, F., Meyer, A., Petonnet, E.: Counting CTL. Logical Methods Comput. Sci. 9(1), 1–34 (2012)

    MathSciNet  Google Scholar 

  19. Ferrante, A., Napoli, M., Parente, M.: Model checking for graded CTL. Fundam. Inform. 96(3), 323–339 (2009)

    MATH  MathSciNet  Google Scholar 

  20. Genevès, P., Layaïda, N., Schmitt, A., Gesbert, N.: Efficiently deciding \(\mu \)-calculus with converse over finite trees. ACM Trans. Comput. Logic 16(2), 16:1–16:41 (2015)

    Article  Google Scholar 

  21. Gottlob, G., Koch, C., Pichler, R., Segoufin, L.: The complexity of XPath query evaluation and XML typing. J. ACM 52(2), 284–335 (2005)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgment

This work was partially developed under the support of the Mexican National Science Council (CONACYT) in the scope of the Cátedras CONACYT project Infraestructura para Agilizar el Desarrollo de Sistemas Centrados en el Usuario (Ref 3053).

Author information

Authors and Affiliations

  1. Consejo Nacional de Ciencia Y Tecnología (CONACYT), Mexico City, Mexico

    Everardo Bárcenas

  2. Facultad de Estadística E Informática, Universidad Veracruzana, Xalapa, Mexico

    Everardo Bárcenas & Edgard Benítez-Guerrero

  3. Benemérita Universidad Autónoma de Puebla, Puebla, Mexico

    Jesús Lavalle

  4. Instituto Nacional de Astrofísica, Óptica Y Electrónica, Puebla, Mexico

    Jesús Lavalle

Authors
  1. Everardo Bárcenas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Edgard Benítez-Guerrero
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jesús Lavalle
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Everardo Bárcenas .

Editor information

Editors and Affiliations

  1. Instituto Politécnico Nacional, Centro de Investigación en Computación, Mexico City, Mexico

    Grigori Sidorov

  2. Facultad de ciencias, Universidad Autónoma Nacional, México, Distrito Federal, Mexico

    Sofía N. Galicia-Haro

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Bárcenas, E., Benítez-Guerrero, E., Lavalle, J. (2015). On the Model Checking of the Graded \(\mu \)-calculus on Trees. In: Sidorov, G., Galicia-Haro, S. (eds) Advances in Artificial Intelligence and Soft Computing. MICAI 2015. Lecture Notes in Computer Science(), vol 9413. Springer, Cham. https://doi.org/10.1007/978-3-319-27060-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27060-9_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27059-3

  • Online ISBN: 978-3-319-27060-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation