Skip to main content
SpringerLink
Log in

Flat Coalgebraic Fixed Point Logics

  • Conference paper
CONCUR 2010 - Concurrency Theory (CONCUR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6269))

Included in the following conference series:

Abstract

Fixed point logics are widely used in computer science, in particular in artificial intelligence and concurrency. The most expressive logics of this type are the μ-calculus and its relatives. However, popular fixed point logics tend to trade expressivity for simplicity and readability, and in fact often live within the single variable fragment of the μ-calculus. The family of such flat fixed point logics includes, e.g., CTL, the *-nesting-free fragment of PDL, and the logic of common knowledge. Here, we extend this notion to the generic semantic framework of coalgebraic logic, thus covering a wide range of logics beyond the standard μ-calculus including, e.g., flat fragments of the graded μ-calculus and the alternating-time μ-calculus (such as ATL), as well as probabilistic and monotone fixed point logics. Our main results are completeness of the Kozen-Park axiomatization and a timed-out tableaux method that matches ExpTime upper bounds inherited from the coalgebraic μ-calculus but avoids using automata.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  3. Calin, G., Myers, R., Pattinson, D., Schröder, L.: CoLoSS: The Coalgebraic Logic Satisfiability Solver (system description). In: Methods for Modalities (M4M-5, 2007). ENTCS, vol. 231, pp. 41–54. Elsevier, Amsterdam (2009)

    Google Scholar 

  4. Cîrstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic μ-calculus. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 179–193. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. D’Agostino, G., Visser, A.: Finality regained: A coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267–298 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  6. Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theoret. Comput. Sci. 126, 77–96 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  7. Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program 2(3), 241–266 (1982)

    Article  MATH  Google Scholar 

  8. Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. System Sci. 30, 1–24 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  9. Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29, 132–158 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  10. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Logic in Computer Science, LICS 1986, pp. 267–278. IEEE, Los Alamitos (1986)

    Google Scholar 

  11. Fine, K.: In so many possible worlds. Notre Dame J. Formal Logic 13, 516–520 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  12. Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theoret. Comput. Sci. 353, 93–117 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  13. Goré, R., Kupke, C., Pattinson, D.: Optimal tableau algorithms for coalgebraic logics. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 114–128. Springer, Heidelberg (2010)

    Google Scholar 

  14. Kozen, D.: Results on the propositional μ-calculus. Theoret. Comput. Sci. 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  15. Kozen, D., Parikh, R.: An elementary proof of the completeness of PDL. Theoret. Comput. Sci. 14, 113–118 (1981)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  17. Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  18. Laver, R.: Well-quasi-orders and sets of finite sequences. Math. Proc. Cambridge Philos. Soc. 79, 1–10 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  19. Lewis, D.: Convention, A Philosophical Study. Harvard University Press, Cambridge (1969)

    Google Scholar 

  20. Parikh, R.: The logic of games and its applications. Annals of Discrete Mathematics 24, 111–140 (1985)

    MathSciNet  Google Scholar 

  21. Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic 45, 19–33 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  22. Pattinson, D., Schröder, L.: Cut elimination in coalgebraic logics. Inf. Comput. (to appear)

    Google Scholar 

  23. Pauly, M.: A modal logic for coalitional power in games. J. Log. Comput. 12, 149–166 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  24. Peleg, D.: Concurrent dynamic logic. J. ACM 34, 450–479 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  25. Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Foundations of Computer Science, FOCS 1976, pp. 109–121. IEEE, Los Alamitos (1976)

    Google Scholar 

  26. Santocanale, L.: Completions of μ-algebras. Ann. Pure Appl. Logic 154, 27–50 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  27. Santocanale, L., Venema, Y.: Completeness for flat modal fixpoint logics. Annals Pure Appl. Log. (preprint under) (to appear), http://arxiv.org/abs/0812.2390

  28. Schröder, L.: A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog. 73, 97–110 (2007)

    Article  MATH  Google Scholar 

  29. Schröder, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 10, 13:1–13:33 (2009)

    Article  MathSciNet  Google Scholar 

  30. Schröder, L., Pattinson, D.: Strong completeness of coalgebraic modal logics. In: Theoretical Aspects of Computer Science, STACS 2009, pp. 673–684. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl (2009)

    Google Scholar 

  31. Schröder, L., Pattinson, D., Kupke, C.: Nominals for everyone. In: International Joint Conferences on Artificial Intelligence, IJCAI 2009, pp. 917–922. AAAI Press, Menlo Park (2009)

    Google Scholar 

  32. Segerberg, K.: A completeness theorem in the modal logic of programs. In: Universal Algebra and Applications. Banach Centre Publications, vol. 9, pp. 31–46. PWN (1982)

    Google Scholar 

  33. Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Inf. Comput. 157, 142–182 (2000)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DFKI Bremen and Department of Computer Science, Universität Bremen,  

    Lutz Schröder

  2. ILLC, Universiteit van Amsterdam,  

    Yde Venema

Authors
  1. Lutz Schröder
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yde Venema
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire Spécification et Vérification (LSV), ENS de Cachan & CNRS, 94235, Cachan cedex, France

    Paul Gastin

  2. LIAFA, Université Paris Diderot, 75205, Paris cedex, France

    François Laroussinie

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schröder, L., Venema, Y. (2010). Flat Coalgebraic Fixed Point Logics. In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_36

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15375-4_36

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15374-7

  • Online ISBN: 978-3-642-15375-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation