Antichains and compositional algorithms for LTL synthesis
DOI10.1007/S10703-011-0115-3zbMATH Open1258.03046OpenAlexW2108036288MaRDI QIDQ453498FDOQ453498
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
Recommendations
antichain algorithmsautomata on infinite wordscompositional algorithmsLTL realizability and synthesissafety game
Formal languages and automata (68Q45) Applications of game theory (91A80) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44)
Cites Work
- Borel determinacy
- Automata, logics, and infinite games. A guide to current research
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Church’s Problem and a Tour through Automata Theory
- CONCUR 2005 – Concurrency Theory
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- Title not available (Why is that?)
- Bounded Synthesis
- Verification, Model Checking, and Abstract Interpretation
- Open Implication
- Algorithms for Omega-Regular Games with Imperfect Information
- An Antichain Algorithm for LTL Realizability
- Safraless Compositional Synthesis
- Translating to co-Büchi made tight, unified, and useful
- On bounded specifications
- Compositional Control Synthesis for Partially Observable Systems
- Compositional algorithms for LTL synthesis
Cited In (22)
- An Antichain Algorithm for LTL Realizability
- Synthesis from component libraries with costs
- Practical synthesis of reactive systems from LTL specifications via parity games
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Title not available (Why is that?)
- Synthesis from LTL specifications with mean-payoff objectives
- Synthesising succinct strategies in safety games with an application to real-time scheduling
- Title not available (Why is that?)
- LTL-model-checking via model composition
- Compositional and symbolic synthesis of reactive controllers for multi-agent systems
- Formally verified algorithms for upper-bounding state space diameters
- Title not available (Why is that?)
- Down the Borel hierarchy: solving Muller games via safety games
- Decoy allocation games on graphs with temporal logic objectives
- Compositional algorithms for LTL synthesis
- Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
- Real-time policy enforcement with metric first-order temporal logic
- A symbolic algorithm for lazy synthesis of eager strategies
- LTL reactive synthesis with a few hints
- Symbolic model checking in non-Boolean domains
- Parametric linear dynamic logic
- Doomsday equilibria for omega-regular games
Uses Software
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)