Mon, 2007-07-30 22:07 — pietro

I read a few interesting papers about the relation of modal logic (and in particular fix-point modal logics) with description logics and automata techniques.
== Description Logics: Modal Logics for Class-Based Modeling ==
http://www.dis.uniroma1.it/~degiacom/ftp/00/Degi00aiml.ps.gz
In this paper De Giacomo gives a clear overview regarding the relation of several description logics with well known modal logics.
In particular he cites the relation of PDL with the description logic C (that is as ALC but adding union, chaining, reflexive transitive closure and identity role over a concept). All reasoning tasks in C (PDL) are known to be EXPTIME.
Another interesting logic is muALC that is obtained by ACL by adding two concept constructs denoting the greatest and least fix point. The corresponding logic (surprise !) is the modal mu calculus, that is known to be decidable and EXPTIME complete.
-----------
== Relationships with other formalisms ==
http://www.inf.unibz.it/~franconi/dl/course/dlhb/dlhb-04.pdf
In this book chapter, Sattler at al. gives, among other, a survey of the relation between description logic and other fixpoint logics such as PDL, mu-calculus, temporal logics and hybrid logics and the guarded fragment. The bibliography is unfortunately missing as this is a chapter from a book (Description Logic Handbook, edited by F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi, P.F. Patel-Schneider, Cambridge University Press, 2002, pages 142-183.)
-----------
== From tableaux to automata for description logics ==
http://www.csc.liv.ac.uk/~frank/publ/automata.ps
This paper from Baader at al investigates the relation between automata and tableau from description logic. The main motivation is that while tableau are used to provide efficient implementations for description logics, automota based algorithm are more versed to reason about complexity. Therefore having a translation between automata and tableau we can get the best from both worlds.
The authors formalize the notion of Exp-Time admissible tableau and then convert the tableau system in an algorithm based on automaton. The main challenge is bring together the different philosophies underlying tableau and automata based algorithms. The former try to construct a model for the input formula by applying a set of rules, while the latter is based of the concept of acceptance of a tree, i.e. if a given tree describes a model. Of course the empty test for the automaton checks whether such tree exists.
The automaton used in the translation (looping tree automata) works on finite trees. Then given an input gamma, the language accepted by the generated automaton is a tree that is compatible with Gamma. This tree is (minus technical details) the tree generated by an exp-time tableau.
--------------------
== Deciding properties of nonregular programs ==
http://ieeexplore.ieee.org/iel2/310/2915/00089587.pdf?arnumber=89587
------------
== The Propositional mu-calculus : Completeness and Related Results. ==
http://www.labri.fr/Perso/~igw/Papers/igw-BRICS-NS-95-1.ps
In this article the author gives a tableau system for modal mu-calculus that first build a model by using a few intuitive tableau rules, and then validates the model using a marking procedure. The tableau uses a normal form where all mu-calculus formulae are transformed in positive and guarded formulae. This normal form assures the monotonicity of the signature function (below) and it ensures that we can use the Tarski-Kanister theorem. It also uses the concept of '''binding''', where all fix point sub-formulae are associated with a name, and the idea to establish '''dependencies''' among fix-point formulae. The main point is to let the tableau procedure loose until we find a loop and then extract a (pseudo) model M from the tableau. Subsequently, using a marking procedure, we can establish that a formula is valid iff there is a consistent marking of the model M.
The marking procedure is based on the idea of signatures. For each sub-formula B, and state s, we define the signature sig(B,s) as the least sequence of ordinals that make all the fix-points sub-formulae of B valid w.r.t. the current state s. The proof goes simply by induction on the structure of the tableau/tree. The Tarski-Kanister theorem gives the basis for the induction.
This paper strikes me as a generalization of the work we have done with CTL and LCK, and in the light of Walukiewicz's paper, I think it's entirely possible to extend our single pass algorithm to handle the mu-calculus.
-------------------