VLDL Satisfiability and Model Checking via Tree Automata

TL;DR

This paper introduces efficient algorithms for VLDL satisfiability and model checking by reducing these problems to tree automata emptiness, enabling the use of existing tools for recursive system analysis.

Contribution

It provides the first asymptotically optimal algorithms for VLDL satisfiability and model checking through a novel reduction to tree automata emptiness.

Findings

Algorithms run in asymptotically optimal time

Reduction leverages mature tree automata tools

Enables efficient analysis of recursive system properties

Abstract

We present novel algorithms solving the satisfiability problem and the model checking problem for Visibly Linear Dynamic Logic (VLDL) in asymptotically optimal time via a reduction to the emptiness problem for tree automata with B\"uchi acceptance. Since VLDL allows for the specification of important properties of recursive systems, this reduction enables the efficient analysis of such systems. Furthermore, as the problem of tree automata emptiness is well-studied, this reduction enables leveraging the mature algorithms and tools for that problem in order to solve the satisfiability problem and the model checking problem for VLDL.