An Antichain Algorithm for LTL Realizability

DOI10.1007/978-3-642-02658-4_22zbMath1242.68158OpenAlexW2095620890MaRDI QIDQ3636866

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

Publication date: 30 June 2009

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02658-4_22

Mathematics Subject Classification ID

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

Related Items (17)

Spanning the spectrum from safety to liveness ⋮ Graph Games and Reactive Synthesis ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Latticed-LTL synthesis in the presence of noisy inputs ⋮ Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis ⋮ Unnamed Item ⋮ Synthesis of Reactive(1) designs ⋮ Antichains and compositional algorithms for LTL synthesis ⋮ Symbolic bounded synthesis ⋮ Unbeast: Symbolic Bounded Synthesis ⋮ Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\) ⋮ Synthesizing robust systems ⋮ Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm ⋮ Doomsday equilibria for omega-regular games ⋮ Realizability of Real-Time Logics ⋮ Automata on infinite trees ⋮ Synthesis of succinct systems

This page was built for publication: An Antichain Algorithm for LTL Realizability