Student research opportunities

Tableaux versus Automata for Modal Logics

Project Code: CECS_934

This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters, PhD

Keywords:

Modal Logic, Automated Reasoning, Tableaux, Automata

Supervisor:

Dr Dirk Pattinson

Outline:

As we know, modal logics are usually decidable, that means given a modal formula, there is a decision procedure (a program) that -- given the formula as an input -- determines whether the formula is satisfiable, i.e. it is valid in at least one point in at least one model. Dually, this gives universal validity: if the negation of a formula is not satisfiable, then it holds at all points in all models. To establish decidability of a particular logical calculus, there are two standard approaches. The first approach proceeds by giving a complete axiomatisation of the logic under consideration (usually via a tableau or sequnt calculus) and then gives an effective procedure (usually backwards proof search) to determine whether there exists a proof of this formula. The second approach works without any axiomatisation, but instead converts every formula to an automaton, with the following property: the automaton accepts a point in a model if and only if this point satisfies the formula. To see whether a formula is satisfiable, it therefore suffices to determine whether the automaton accepts at least one point in at least one model -- this is the ``emptyness problem'' of the associated class of automata. While both approaches seem to be fundamentally different at the outset, one sees that there are certain similarities: in particular, constructing a decision procedure from a tableau calculus is strikingly similar to constructing an automaton, and solving the emptyness problem at the same time.

Goals of this project

This is a broad project that can be developed into several directions. The most fundamental goal is to make the correspondence between Tableaux and Automata precise. Other questions are whether
we can convert automata into tableaux and vice versa? What are the advantages, both of a theoretical and practica nature, of either approach?

Requirements/Prerequisites

Interest, and working knowledge in either automata theory / tableaux or modal logic.

Student Gain

Exposure to state-of-the art research questions, conceptual understanding of (aspects of) automated reasoning.

Background Literature

A frighteningly comprehensive exposition of Tableau Methods can be found in the Handbook article on Modal Tableau by Rajeev Gore. References to the automata-theoretic method are scattered in the literature can are provided on request.

Contact: