Automata Linear Dynamic Logic on Finite Traces

TL;DR

This paper introduces ALDL_f, a new temporal logic combining automata and propositional logic, which is as expressive as Monadic Second-Order Logic and has PSPACE satisfiability complexity.

Contribution

It presents ALDL_f, a novel automata-based temporal logic on finite traces with PSPACE satisfiability, enhancing expressiveness over LTL without added complexity.

Findings

ALDL_f is equivalent to Monadic Second-Order Logic.

Satisfiability for ALDL_f is in PSPACE.

ALDL_f combines propositional logic with nondeterministic finite automata.

Abstract

Temporal logics are widely used by the Formal Methods and AI communities. Linear Temporal Logic is a popular temporal logic and is valued for its ease of use as well as its balance between expressiveness and complexity. LTL is equivalent in expressiveness to Monadic First-Order Logic and satisfiability for LTL is PSPACE-complete. Linear Dynamic Logic (LDL), another temporal logic, is equivalent to Monadic Second-Order Logic, but its method of satisfiability checking cannot be applied to a nontrivial subset of LDL formulas. Here we introduce Automata Linear Dynamic Logic on Finite Traces (ALDL_f) and show that satisfiability for ALDL_f formulas is in PSPACE. A variant of Linear Dynamic Logic on Finite Traces (LDL_f), ALDL_f combines propositional logic with nondeterministic finite automata (NFA) to express temporal constraints. ALDL$_f$ is equivalent in expressiveness to Monadic Second-Order Logic. This is a gain in expressiveness over LTL at no cost.