Dissecting \texttt{ltlsynt}

DOI10.1007/S10703-022-00407-6OpenAlexW4384300979MaRDI QIDQ6151759FDOQ6151759

Authors: Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet 

Publication date: 11 March 2024

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-022-00407-6

Recommendations

• Practical synthesis of reactive systems from LTL specifications via parity games
• Verification, Model Checking, and Abstract Interpretation
• Synthesis of Reactive(1) designs
• LTL reactive synthesis with a few hints
• Lazy synthesis

zbMATH Keywords

parity gamesreactive synthesisMealy machinesparity automataLTL formulas

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation
• State Reduction in Incompletely Specified Finite-State Machines
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Title not available (Why is that?)
• Modalities for model checking: Branching time logic strikes back
• Effective reductions of Mealy machines
• Title not available (Why is that?)
• Efficient minimization of deterministic weak \(\omega\)-automata
• Title not available (Why is that?)
• Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
• Mathematical Foundations of Computer Science 2003
• One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata
• An improved construction of deterministic omega-automaton using derivatives
• LTL to deterministic Emerson-Lei automata
• Practical “Paritizing” of Emerson-Lei Automata
• From Spot 2.0 to Spot 2.10: What’s New?

Cited In (1)

• LTL reactive synthesis with a few hints

This page was built for publication: Dissecting \texttt{ltlsynt}

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