LTL reactive synthesis with a few hints

DOI10.1007/S10817-025-09737-6MaRDI QIDQ6912394zbMATH OpenFDO

Authors Emmanuel Filiot, Jean-François Raskin

Publication date 22 October 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/S10817-025-09737-6

zbMATH Keywords

LTL synthesisMealy machinespassive learningreactive synthesisRPNI

Mathematics Subject Classification ID

Temporal logic (03B44) Computational learning theory (68Q32) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• Alternation
• An Antichain Algorithm for LTL Realizability
• Antichains and compositional algorithms for LTL synthesis
• Better Quality in Synthesis through Quantitative Objectives
• Bounded Synthesis
• Computer aided verification. 30th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14--17, 2018. Proceedings. Part I
• Formally reasoning about quality
• Graph Games and Reactive Synthesis
• Handbook of model checking
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• Learning Moore machines from input-output traces
• Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games
• Minimizing expected cost under hard Boolean constraints, with applications to quantitative synthesis
• On high-quality synthesis
• Scalable anytime algorithms for learning fragments of linear temporal logic
• Synthesizing non-vacuous systems

This page was built for publication: LTL reactive synthesis with a few hints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6912394)