Antichains and compositional algorithms for LTL synthesis

DOI10.1007/S10703-011-0115-3MaRDI QIDQ453498zbMATH OpenOpenAlexFDO

Authors Emmanuel Filiot, Naiyong Jin, Jean-François Raskin

Publication date 27 September 2012

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

Full work available at URL https://doi.org/10.1007/s10703-011-0115-3

zbMATH Keywords

antichain algorithmsautomata on infinite wordscompositional algorithmsLTL realizability and synthesissafety game

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Applications of game theory (91A80) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44)

Recommendations

• An Antichain Algorithm for LTL Realizability
• Compositional algorithms for LTL synthesis
• Synthesis from LTL specifications with mean-payoff objectives
• Safraless Compositional Synthesis
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 2209335 (Why is no real title available?)
• Algorithms for Omega-Regular Games with Imperfect Information
• An Antichain Algorithm for LTL Realizability
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Automata, logics, and infinite games. A guide to current research
• Borel determinacy
• Bounded Synthesis
• CONCUR 2005 – Concurrency Theory
• Church’s Problem and a Tour through Automata Theory
• Compositional Control Synthesis for Partially Observable Systems
• Compositional algorithms for LTL synthesis
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• On bounded specifications
• Open Implication
• Safraless Compositional Synthesis
• Translating to co-Büchi made tight, unified, and useful
• Verification, Model Checking, and Abstract Interpretation

Cited in

(21)

• A symbolic algorithm for lazy synthesis of eager strategies
• Practical synthesis of reactive systems from LTL specifications via parity games
• The complexity of transducer synthesis from multi-sequential specifications
• Formally verified algorithms for upper-bounding state space diameters
• Synthesis from LTL specifications with mean-payoff objectives
• An Antichain Algorithm for LTL Realizability
• Decoy allocation games on graphs with temporal logic objectives
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Synthesis from component libraries with costs
• scientific article; zbMATH DE number 7147442 (Why is no real title available?)
• Compositional algorithms for LTL synthesis
• LTL reactive synthesis with a few hints
• Approximating optimal bounds in prompt-LTL realizability in doubly-exponential time
• Synthesising succinct strategies in safety games with an application to real-time scheduling
• Real-time policy enforcement with metric first-order temporal logic
• Parametric linear dynamic logic
• Symbolic model checking in non-Boolean domains
• Compositional and symbolic synthesis of reactive controllers for multi-agent systems
• Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
• Down the Borel hierarchy: solving Muller games via safety games
• LTL-model-checking via model composition

Describes a project that uses

Uses Software

• Antichains

This page was built for publication: Antichains and compositional algorithms for LTL synthesis

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