×

Modal \(\mu\)-calculus with atoms. (English) Zbl 1434.03071

Goranko, Valentin (ed.) et al., 26th EACSL annual conference on computer science logic, CSL 2017, Stockholm, Sweden, August 20–24, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 82, Article 30, 21 p. (2017).
Summary: 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.
For the entire collection see [Zbl 1372.68009].

MSC:

03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI