1) Wider research context
The satisfiability problem, parametrized by a formal language (logic) L, asks if an input formula of L holds in some structure, i.e. has a (possibly infinite) model. The finite satisfiability problem (FSAT) restricts models to finite ones, while finite query entailment (FQE) also checks if such a model violates an input query. We focus on dynamic logics—extensions of modal logic with recursion, such as regular path expressions (PDL) or fixed-point operators (mu-calculus)—which include fragments of OWL 2 and are widely used in formal verification.
The classical approach, pioneered by Vardi, is to show that satisfiable formulae have infinite tree-like models, to construct an automaton accepting exactly those tree-like models, and to test its non-emptiness.
This generalizes to query entailment by building an automaton for the query, complementing it, and checking its intersection with the formula's automaton.
Despite success in hundreds of papers, Vardi’s method gives no insight into FSAT, especially in the presence of recursion.
Existing FSAT techniques rely either on integer programming (unsuitable for recursion) or small-model properties (open for many logics) followed by costly candidate enumeration.
A notable exception is Bojańczyk’s 2002 work, introducing automata over finite graphs that capture two-way mu-calculus and proving decidability of non-emptiness.
2) Objectives
Our goal is to develop a novel automata-based framework for FSAT and FQE, extending Bojańczyk’s finite-graph automata. First, we adapt Vardi’s scheme for FQE, providing a unified solution for many dynamic logics and extending beyond recent results by Gutowski et al for the plain modal logic (ALC).
Second, we address two-way logics with counting and solve FSAT for them using a novel model of two-way graded automata over finite graphs.
This offers the first alternative to integer programming and solves FSAT for fully graded mu-calculus and graded PDL with converse, both open since 1999.
Lastly, we explore finite-graph automata with pebbles trying to tackle the long-standing FSAT problem for PDL with intersection or looping.
3) Approach
We represent finite graphs as infinite trees recognisable by tree automata. The crux is to indentify conditions—expressible, for example, in monadic second-order logic with the unbounding quantifier—that enable transforming these trees back into finite structures.
4) Level of originality
The project will deliver uniform techniques for FSAT and FQE in dynamic modal logics, significantly advancing the state of the art. It also aims to solve open problems on extensions of mu-calculus and PDL, some unresolved for over 25 years.
5) Primary researchers involved
The team includes B. Bednarczyk (PI, expert in PDL-like logics), M. Oritz (mentor, specialist in ontology-based query entailment), and W. Charatonik (external collaborator, expert in logics with counting over trees).
