Finite satisfiability of logic with loops solved under specific conditions
Towards Finite Satisfiability of PDL with Loops
Logic in Computer Science
Summary
Propositional Dynamic Logic (PDL) helps describe how computer programs behave, including loops or cycles. The problem of knowing if these logic statements can be true in some model has been solved before, but only when models could be infinite. This paper studies the harder question of deciding this for only finite models, which is important for practical reasons. The authors found a way to solve this finite satisfiability problem for a large class of formulas by converting models into special infinite tree-like structures that can be checked by automata. This advances understanding of cycles in program logic over finite structures.
What this means in practice
- •For formal verification engineers: Decide finite-state program properties involving loops in certain restricted logical forms, improving automated analysis tools.
- •For database query optimizers: Analyze query languages with recursive structures by understanding finite satisfiability under loop-like constructs, aiding optimization.
A theory result. No direct application yet.
Authors
Bartosz Jan Bednarczyk, Mikołaj Swoboda
Abstract
Propositional Dynamic Logic (PDL) is a well-established modal logic of programs. Among its many extensions, the loop operator stands out for capturing the cyclic behaviour of programs: a world satisfies loop(pi) precisely when it can return to itself along a path matching the regular expression pi. While the satisfiability problem for the resulting logic LPDL was settled already in the 1980s, the decidability of its finite satisfiability problem has remained open ever since. The core difficulty is inherent to the finite setting: requiring and forbidding cycles at once is easily reconciled over arbitrary models, but over finite ones it defeats the existing finite-model-theoretic techniques. We make the first substantial progress towards closing this gap. We prove that finite satisfiability is ExpTime-complete for LPDL formulae (also in the presence of the converse operator) in negation normal form, under the restriction that every negated non-atomic loop has the form loop(pi^+) for some arbitrarily complex program pi -- a generalised form of self-reachability; positive occurrences of loops remain unrestricted. At the heart of our approach lies a novel way of representing intended finite models as their infinite, cactus-like unravellings: these are recognisable by two-way tree automata and satisfy a tailored omega-regular foldability condition that lets us finitise the accepted structures.