Antichains and compositional algorithms for LTL synthesis

DOI10.1007/s10703-011-0115-3zbMath1258.03046OpenAlexW2108036288MaRDI QIDQ453498

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

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

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

Related Items

Symbolic Model Checking in Non-Boolean Domains, Unnamed Item, Compositional and symbolic synthesis of reactive controllers for multi-agent systems, Synthesising succinct strategies in safety games with an application to real-time scheduling, Formally verified algorithms for upper-bounding state space diameters, Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes, Real-time policy enforcement with metric first-order temporal logic, Unnamed Item, Unnamed Item, Down the Borel hierarchy: solving Muller games via safety games, Parametric linear dynamic logic, Synthesis from component libraries with costs, Doomsday equilibria for omega-regular games, Practical synthesis of reactive systems from LTL specifications via parity games, A symbolic algorithm for lazy synthesis of eager strategies, Decoy allocation games on graphs with temporal logic objectives

Uses Software

• Antichains

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Borel determinacy
• Automata, logics, and infinite games. A guide to current research
• Translating to Co-Büchi Made Tight, Unified, and Useful
• On Bounded Specifications
• Compositional Control Synthesis for Partially Observable Systems
• Bounded Synthesis
• Open Implication
• An Antichain Algorithm for LTL Realizability
• Compositional Algorithms for LTL Synthesis
• Algorithms for Omega-Regular Games with Imperfect Information
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Church’s Problem and a Tour through Automata Theory
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Safraless Compositional Synthesis
• CONCUR 2005 – Concurrency Theory
• Verification, Model Checking, and Abstract Interpretation