Enriched Modal Logics

VCLA will be hosting a RiSE seminar talk by Aniello Murano on November 7th, 2013.

ABSTRACT

In recent years, modal logics have been deeply investigated under enriched modalities such as inverse programs, nominals, and graded modalities. Intuitively, inverse programs allow to travel backwards along accessibility relations, nominals are propositional variables interpreted as singleton sets, and graded modalities enable statements about a number of successors (and possibly predecessors) of a state. In this talk, we will report recent results achieved by considering the mu-calculus, as well as its sublogic CTL, enriched with these modalities.

First, we recall that the full enriched mu-calculus, which is the propositional mu-calculus enriched with inverse programs, graded modalities, and nominals, is undecidable. Then, we show that all its fragments, obtained by dropping at least one of the additional constructs are decidable and ExpTime-complete, as for the classical mu-calculus. In particular, these results are obtained by using an automata-theoretic approach. Specifically, we introduce new automata models as variant of classical parity tree automata.

Then, we turn to the case of CTL with graded modalities (GCTL). We first show that GCTL is at least exponentially more succinct than mu-calculus enriched with graded modalities. Then, we prove that the satisfiability problem for GCTL remains solvable in ExpTime, as it is for CTL, even in the case the graded numbers are coded in binary. This result is obtained by exploiting an automata-theoretic approach, which involves a model of alternating automata with satellites.

Finally, we will discuss about some interesting open questions.

*********

This talk is based on the following papers:

P.A. Bonatti, C. Lutz, A. Murano, and M.Y. Vardi The Complexity of Enriched ?-Calculi (a preliminary version appeared in ICALP'06) Logical Methods in Computer Science, 2008 Vol. 4 (3:11), pages 1 - 27.

A. Bianco, F. Mogavero, and A. Murano Graded Computation Tree Logic (a preliminary version appeared in LICS'09 and CSL'10) ACM Transactions on Computational Logic, 2012. Vol. 13, N. 3, Article 25, pages 1-53.