Advertisement

Specifying Program Properties Using Modal Fixpoint Logics: A Survey of Results

  • Martin LangeEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11600)

Abstract

The modal \(\mu \)-calculus is a well-known program specification language with desirable properties like decidability of satisfiability and model checking, axiomatisability etc. Its expressive power is limited by Monadic Second-Order Logic or parity tree automata. Hence, it can only express regular properties.

In this talk I will argue in favour of specification languages whose expressiveness reaches beyond regularity. I will present Viswanathan and Viswanathan’s Higher-Order Fixpoint Logic as a natural extension of the modal \(\mu \)-calculus with highly increased expressive power. We will see how this logic can be used to specify some interesting non-regular properties and then survey results on it with a focus on open questions in this area.

References

  1. 1.
    Afshari, B., Leigh, G.E.: Cut-free completeness for modal mu-calculus. In: Proceedings of the 32nd ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pp. 1–12. IEEE (2017)Google Scholar
  2. 2.
    Arnold, A.: The modal \(\mu \)-calculus alternation hierarchy is strict on binary trees. RAIRO Theor. Inform. Appl. 33, 329–339 (1999)CrossRefGoogle Scholar
  3. 3.
    Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Log. Methods Comput. Sci. 3, 1–33 (2007)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Bradfield, J., Stirling, C.: Modal logics and \(\mu \)-calculi: an introduction. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 293–330. Elsevier, New York (2001)CrossRefGoogle Scholar
  5. 5.
    Bradfield, J., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic: Studies in Logic and Practical Reasoning, vol. 3, pp. 721–756. Elsevier, New York (2007)CrossRefGoogle Scholar
  6. 6.
    Bradfield, J., Walukiewicz, I.: The mu-calculus and model checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 871–919. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8_26CrossRefzbMATHGoogle Scholar
  7. 7.
    Bradfield, J.C.: The modal mu-calculus alternation hierarchy is strict. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 233–246. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-61604-7_58CrossRefGoogle Scholar
  8. 8.
    Bruse, F.: Alternating Parity Krivine Automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 111–122. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44522-8_10CrossRefGoogle Scholar
  9. 9.
    Bruse, F.: Alternation is strict for higher-order modal fixpoint logic. In: Proceedings of the 7th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016. EPTCS, vol. 226, pp. 105–119 (2016)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Bruse, F., Lange, M., Lozes, E.: Space-efficient fragments of higher-order fixpoint logic. In: Hague, M., Potapov, I. (eds.) RP 2017. LNCS, vol. 10506, pp. 26–41. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67089-8_3CrossRefGoogle Scholar
  11. 11.
    Bruse, F., Lange, M., Lozes, E.: Collapses of fixpoint alternation hierarchies in low type-levels of higher-order fixpoint logic. In: Proceedings Workshop on Programming and Reasoning on Infinite Structures, PARIS 2014 (2018)Google Scholar
  12. 12.
    Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, pp. 252–263. ACM (2017)Google Scholar
  13. 13.
    Dam, M.: CTL\(^{*}\) and ECTL\(^{*}\) as fragments of the modal \(\mu \)-calculus. TCS 126(1), 77–96 (1994)CrossRefGoogle Scholar
  14. 14.
    Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2016)CrossRefGoogle Scholar
  15. 15.
    Emerson, E.A., Jutla, C.S.: Tree automata, \(\mu \)-calculus and determinacy. In: Proceedings of the 32nd Symposium on Foundations of Computer Science, San Juan, pp. 368–377. IEEE (1991)Google Scholar
  16. 16.
    Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional \(\mu \)-calculus. In: Symposion on Logic in Computer Science, Washington, D.C., pp. 267–278. IEEE (1986)Google Scholar
  17. 17.
    Enqvist, S., Seifan, F., Venema, Y.: Completeness for the modal \(\mu \)-calculus: separating the combinatorics from the dynamics. Theor. Comput. Sci. 727, 37–100 (2018)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logic of nonregular programs. J. Comput. Syst. Sci. 26(2), 222–243 (1983)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-61604-7_60CrossRefGoogle Scholar
  21. 21.
    Jurdzinski, M., Lazic, R.: Succinct progress measures for solving parity games. In: Proceedings of the 32nd ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pp. 1–9. IEEE (2017)Google Scholar
  22. 22.
    Kobayashi, N., Lozes, É., Bruse, F.: On the relationship between higher-order recursion schemes and higher-order fixpoint logic. In Proceedings of POPL 2017, pp. 246–259. ACM (2017)CrossRefGoogle Scholar
  23. 23.
    Kozen, D.: Results on the propositional \(\mu \)-calculus. TCS 27, 333–354 (1983)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Lange, M.: Local model checking games for fixed point logic with chop. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 240–254. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45694-5_17CrossRefGoogle Scholar
  25. 25.
    Lange, M.: The alternation hierarchy in fixpoint logic with chop is strict too. Inf. Comput. 204(9), 1346–1367 (2006)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Lange, M., Somla, R.: Propositional dynamic logic of context-free programs and fixpoint logic with chop. Inf. Process. Lett. 100(2), 72–75 (2006)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Lehtinen, K.: A modal \(\mu \) perspective on solving parity games in quasi-polynomial time. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pp. 639–648. ACM (2018)Google Scholar
  28. 28.
    Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30538-5_34CrossRefGoogle Scholar
  29. 29.
    Müller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 510–520. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-49116-3_48CrossRefGoogle Scholar
  30. 30.
    Niwiński, D.: Fixed point characterization of infinite behavior of finite-state systems. Theor. Comput. Sci. 189(1–2), 1–69 (1997)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of the 21st IEEE Symposium on Logic in Computer Science, LICS 2006, pp. 81–90. IEEE Computer Society (2006)Google Scholar
  32. 32.
    Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969)MathSciNetzbMATHGoogle Scholar
  33. 33.
    Stirling, C.: Local model checking games (extended abstract). In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60218-6_1CrossRefGoogle Scholar
  34. 34.
    Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 512–528. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-28644-8_33CrossRefGoogle Scholar
  35. 35.
    Walukiewicz, I.: Monadic second order logic on tree-like structures. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 399–413. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60922-9_33CrossRefGoogle Scholar
  36. 36.
    Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional \(\mu \)-calculus. Inf. Comput. 157(1–2), 142–182 (2000)MathSciNetCrossRefGoogle Scholar
  37. 37.
    Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234–263 (2001)MathSciNetCrossRefGoogle Scholar
  38. 38.
    Wilke, T.: Alternating tree automata, parity games, and modal \(\mu \)-calculus. Bull. Belgian Math. Soc. 8(2), 359–391 (2001)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  1. 1.University of KasselKasselGermany

Personalised recommendations