Engineering an LTLf Synthesis Tool

TL;DR

This paper presents an efficient LTLf synthesis tool that uses a novel direct translation to a BDD-based DFA, enabling faster synthesis by solving reachability games during construction.

Contribution

The paper introduces a new direct translation from LTLf to a BDD-based DFA, improving synthesis performance over existing tools.

Findings

Outperforms existing LTLf synthesis tools on benchmark suite

Uses a novel direct translation to BDD-based DFA

Enables on-the-fly reachability game solving during construction

Abstract

The problem of LTLf reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolution of the inputs and outputs has a prefix that satisfies a given LTLf specification. We describe the implementation of an LTLf synthesizer that outperforms existing tools on our benchmark suite. This is based on a new, direct translation from LTLf to a DFA represented as an array of Binary Decision Diagrams (MTBDDs) sharing their nodes. This MTBDD-based representation can be interpreted directly as a reachability game that is solved on-the-fly during its construction.