On the undecidability of logics with converse, nominals, recursion and counting Original Research Article

The evolution of description logics (DLs) and propositional dynamic logics produced a hierarchy of decidable logics with multiple maximal elements. It would be desirable to combine different maximal logics into one super-logic, but then inference may turn out to be undecidable. Then it is important to characterize the decidability threshold for these logics. In this perspective, an interesting open question pointed out by Sattler and Vardi [Proc. IJCARʹ01, in: Lecture Notes in Artif. Intel., vol. 2083, Springer, 2001, pp. 76–91] is whether inference in a hybrid μ-calculus with restricted forms of graded modalities is decidable, and which complexity class it belongs to. In this paper we improve a previous result [Proc. IJCAIʹ03, Morgan Kaufmann, 2003, pp. 331–336.] and prove that this calculus and the corresponding DL μALCIOfa are undecidable. We show also that nested fixpoints are not necessary for undecidability.