Document Open Access Logo

Modal mu-Calculus with Atoms

Authors Bartek Klin, Mateusz Lelyk

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.30.pdf
  • Filesize: 0.5 MB
  • 21 pages

Document Identifiers

Author Details

Bartek Klin
Mateusz Lelyk

Cite As Get BibTex

Bartek Klin and Mateusz Lelyk. Modal mu-Calculus with Atoms. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.30

Abstract

We introduce an extension of modal mu-calculus to sets with atoms and study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show some limitations to the expressiveness of the calculus and argue that a naive way to remove these limitations results in a logic whose model checking is undecidable.

Subject Classification

Keywords
  • modal mu-calculus
  • sets with atoms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. A. Arnold and D. Niwiński. Rudiments of μ-calculus. Studies in logic and the foundations of mathematics. London, Amsterdam, 2001. Google Scholar
  2. M. Bojańczyk, B. Klin, and S. Lasota. Automata theory in nominal sets. Log. Meth. Comp. Sci., 10, 2014. Google Scholar
  3. M. Bojańczyk and T. Place. Toward model theory with data values. In Procs. ICALP 2012 Part II, volume 7392 of Lecture Notes in Computer Science, pages 116-127, 2012. Google Scholar
  4. J. Bradfield and C.Stirling. Modal mu-calculi. In Handbook of Modal Logic, volume 3, pages 721-756. Elsevier, 2007. Google Scholar
  5. J. Bradfield and C. Stirling. Modal logics and mu-calculi: an introduction. In Handbook of Process Algebra, pages 293-330. North-Holland, 2001. Google Scholar
  6. J. Bradfield and I. Walukiewicz. The mu-calculus and model-checking. In E. Clarke, T. Henzinger, and H. Veith, editors, Handbook of Model Checking. Springer-Verlag, 2015. Google Scholar
  7. C. Carapelle and M. Lohrey. Temporal logics with local constraints (invited talk). In Procs. CSL 2015, volume 41 of LIPIcs, pages 2-13, 2015. Google Scholar
  8. V. Ciancia and U. Montanari. Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput., 208(12):1349-1367, 2010. Google Scholar
  9. S. Cranen, J. F. Groote, and M. Reniers. A linear translation from CTL^* to the first-order modal μ-calculus. Theoretical Computer Science, 412(28):3129-3139, 2011. Google Scholar
  10. Mads Dam. Model checking mobile processes. Information and Computation, 129(1):35-51, 1996. Google Scholar
  11. Rocco De Nicola and Michele Loreti. Multiple-labelled transition systems for nominal calculi and their logics. Mathematical Structures in Computer Science, 18(01):107-143, 2008. Google Scholar
  12. S. Demri and D. D'Souza. An automata-theoretic approach to constraint LTL. Inf. Comput., 205(3):380-415, 2007. Google Scholar
  13. S. Demri, D. D'Souza, and R. Gascon. Temporal logics of repeating values. J. Log. Comput., 22(5):1059-1096, 2012. Google Scholar
  14. S. Demri, D. Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. Logical Methods in Computer Science, 12(3), 2016. Google Scholar
  15. S. Demri and R. Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. Google Scholar
  16. S. Demri, R. Lazic, and D. Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput., 205(1):2-24, 2007. Google Scholar
  17. E. A. Emerson and J. Y. Halpern. "sometimes" and "not never" revisited: On branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. Google Scholar
  18. Gian-Luigi Ferrari, Stefania Gnesi, Ugo Montanari, and Marco Pistore. A model-checking verification environment for mobile processes. ACM Transactions on Software Engineering and Methodology, 12(4):440-473, 2003. Google Scholar
  19. D. Figueira. Alternating register automata on finite words and trees. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  20. D. Figueira and L. Segoufin. Future-looking logics on data words and trees. In Procs. MFCS 2009, volume 5734 of Lecture Notes in Computer Science, pages 331-343, 2009. Google Scholar
  21. N. Francez and M. Kaminski. Finite-memory automata. TCS, 134(2):329-363, 1994. Google Scholar
  22. M. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Asp. Comput., 13(3-5):341-363, 2002. Google Scholar
  23. Jan Friso Groote and Radu Mateescu. Verification of temporal properties of processes in a setting with data. In Procs. AMAST'99, pages 74-90, 1999. Google Scholar
  24. Jan Friso Groote and Tim A. C. Willemse. Model-checking processes with data. Science of Computer Programming, 56(3):251-273, 2005. Google Scholar
  25. M. Jurdzinski and R. Lazic. Alternating automata on data trees and xpath satisfiability. ACM Trans. Comput. Log., 12(3):19:1-19:21, 2011. Google Scholar
  26. B. Klin, E. Kopczyński, J. Ochremiak, and S. Toruńczyk. Locally finite constraint satisfaction problems. In Procs. LICS 2015, pages 475-486, 2015. Google Scholar
  27. B. Klin and M. Szynwelski. SMT solving for functional programming over infinite structures. In MFSP, volume 207, pages 57-75, 2016. URL: http://dx.doi.org/10.4204/EPTCS.207.3.
  28. E. Kopczyński and S. Toruńczyk. Lois: Syntax and semantics. In Procs. of POPL 2017, pages 586-598, 2017. Google Scholar
  29. D. Kozen. Results on the propositional μ-calculus. Theor. Comp. Sci., 27(3):333-354, 1983. URL: http://dx.doi.org/10.1016/0304-3975(82)90125-6.
  30. Hui-Min Lin. Predicate μ-calculus for mobile ambients. Journal of Computer Science and Technology, 20(1):95-104, 2005. Google Scholar
  31. F. Neven, T. Schwentick, and V. Vianu. Towards regular languages over infinite alphabets. In MFCS, pages 560-572, 2001. Google Scholar
  32. J. Ochremiak. Extended constraint satisfaction problems. PhD thesis, University of Warsaw, 2016. Google Scholar
  33. J. Parrow, J. Borgström, L.-H. Eriksson, R. Gutkovas, and T. Weber. Modal logics for nominal transition systems. In Procs. CONCUR 2015, volume 42 of LIPIcs, pages 198-211, 2015. Google Scholar
  34. A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  35. L. Segoufin. Automata and logics for words and trees over an infinite alphabet. In Procs. CSL 2006, volume 4207 of Lecture Notes in Computer Science, pages 41-57, 2006. Google Scholar
  36. W. Thomas and T. Wilke. Automata, logics, and infinite games: A guide to current research. Bulletin of Symbolic Logic, 10(1):114-115, 2004. Google Scholar
  37. N. Tzevelekos. Fresh-register automata. SIGPLAN Not., 46(1):295-306, 2011. Google Scholar
  38. Y. Venema. Lectures on the modal μ-calculus. ILLC, Univ. of Amsterdam, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact