Engineering an LTLf Synthesis Tool

doi:10.1007/978-3-032-02602-6_10

Engineering an LTLf Synthesis Tool

2026-01-01

0

PRE

AI

A

Alexandre Duret-Lutz *

DOI：10.1007/978-3-032-02602-6_10

Original

Original request for help

Save

Abstract

En 中文

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.

Keywords:

REACTIVE SYNTHESIS

DERIVATIVES

Engineering an LTLf Synthesis Tool

Abstract

Journal

Organization