FINGO: Finite Graph Operating Automata Meet Dynamic Logics

The subject of the grant lies on the borderline of logic (model theory), database theory, artificial intelligence (knowledge representation), formal software verification, and automata theory. The main problem investigated in the grant is the satisfiability problem: given a formula phi written in a certain formal language (logic) L, we ask whether the formula phi is satisfiable, that is, whether there exists a satisfying structure. In example applications, e.g., in formal software verification, the formula phi will be the specification of a computer system`s operation, and the structure will be an abstraction of the program or IT system. Then, the question of satisfiability can be used, for example, to check if the system never enters a dangerous zone or if there are no deadlocks in it. In database applications, phi will be a query to the database (written e.g. in popular SQL), and the structure will be a relational database. Depending on what L is, the satisfiability problem can be computationally easier or harder, and even undecidable. In the project, we will focus on the finite satisfiability problem, which additionally requires that the sought structures have a finite size. This reflects our reality more accurately, where databases or biochemical systems are inherently finite. We will also narrow our area of interest to dynamic logics used for program verification, such as extensions of the Mu- calculus or PDL (Propositional Dynamic Logic), for which the finite satisfiability problem is still open. Let us just mention that, although it may seem counterintuitive, the finite satisfiability problem is often harder and requires a completely different set of techniques than the classical satisfiability problem. For example, the classical problem for many computer logics (e.g., used in knowledge representation) relies on the tree model property: if a structure satisfying phi exists, then one resembling a tree also exists. And we can deal with trees much more easily, e.g., by using known results about automata operating on infinite trees (intuitively, these are machines with finite memory reading infinite trees and accepting them or not). The aim of the project is to propose new techniques for dealing with the finite satisfiability problem in a way analogous to that described above, but this time automata, instead of on infinite trees, will operate on finite structures (graphs). We want to develop a series of results (decidability) for emptiness problems (will a given automaton accept some graph?) for extensions of this type of automata. Once this succeeds, we will apply our framework to attack open problems, such as the finite satisfiability of the Two-Way Graded Mu-calculus. We also hope that our research will allow us to get closer to solving the finite satisfiability problem for LoopPDL, PDL with Intersection, or Non-Regular PDL, which have been open since the 80s.