A Symbolic Approach to Safety LTL Synthesis

TL;DR

This paper introduces a simplified approach to Safety LTL synthesis, enabling more efficient system design by reducing the problem to Horn-SAT and employing symbolic methods with BDDs, outperforming existing tools.

Contribution

It presents the first explicit reduction of Safety LTL synthesis to Horn-SAT and develops a symbolic BDD-based approach, improving efficiency over previous methods.

Findings

Horn-SAT reduction enables linear-time solutions.

Symbolic BDD-based approach outperforms existing tools.

Safety LTL synthesis is significantly simpler than general LTL synthesis.

Abstract

Temporal synthesis is the automated design of a system that interacts with an environment, using the declarative specification of the system's behavior. A popular language for providing such a specification is Linear Temporal Logic, or LTL. LTL synthesis in the general case has remained, however, a hard problem to solve in practice. Because of this, many works have focused on developing synthesis procedures for specific fragments of LTL, with an easier synthesis problem. In this work, we focus on Safety LTL, defined here to be the Until-free fragment of LTL in Negation Normal Form~(NNF), and shown to express a fragment of safe LTL formulas. The intrinsic motivation for this fragment is the observation that in many cases it is not enough to say that something "good" will eventually happen, we need to say by when it will happen. We show here that Safety LTL synthesis is significantly simpler algorithmically than LTL synthesis. We exploit this simplicity in two ways, first by describing an explicit approach based on a reduction to Horn-SAT, which can be solved in linear time in the size of the game graph, and then through an efficient symbolic construction, allowing a BDD-based symbolic approach which significantly outperforms extant LTL-synthesis tools.