Thursday, November 7, 2013
Speaker: Aniello Murano
Venue: TU Wien
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.