Antichains: A New Algorithm for Checking Universality of Finite Automata
From MaRDI portal
Publication:5756729
DOI10.1007/11817963_5zbMath1188.68171OpenAlexW1731774687MaRDI QIDQ5756729
Laurent Doyen, Martin De Wulf, Jean-François Raskin, Thomas A. Henzinger
Publication date: 5 September 2007
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11817963_5
Related Items
Ramsey-Based Inclusion Checking for Visibly Pushdown Automata ⋮ Algorithms for Kleene algebra with converse ⋮ Symbolic automata for representing big code ⋮ Model checking transactional memories ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Problems on finite automata and the exponential time hypothesis ⋮ Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes ⋮ Unnamed Item ⋮ Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic ⋮ Unnamed Item ⋮ Antichains and compositional algorithms for LTL synthesis ⋮ Verification of STM on relaxed memory models ⋮ Strategy construction for parity games with imperfect information ⋮ Fixed point guided abstraction refinement for alternating automata ⋮ Parametric random generation of deterministic tree automata ⋮ From non-preemptive to preemptive scheduling using synchronization synthesis ⋮ Completeness and Nondeterminism in Model Checking Transactional Memories ⋮ Strategy Construction for Parity Games with Imperfect Information ⋮ Nested antichains for WS1S ⋮ Nondeterministic syntactic complexity ⋮ A synchronous effects logic for temporal verification of pure Esterel ⋮ Lazy Automata Techniques for WS1S ⋮ Up-To Techniques for Weighted Systems ⋮ Coinductive Algorithms for Büchi Automata ⋮ Strategy synthesis for multi-dimensional quantitative objectives ⋮ Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm ⋮ Automata Learning: A Categorical Perspective ⋮ Transactional Reduction of Component Compositions ⋮ Computing Weakest Strategies for Safety Games of Imperfect Information ⋮ Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Abstraction refinement and antichains for trace inclusion of infinite state systems ⋮ Advanced Ramsey-Based Büchi Automata Inclusion Testing ⋮ Random Generation of Deterministic Tree (Walking) Automata ⋮ Fixpoint Guided Abstraction Refinement for Alternating Automata ⋮ Random Models for Evaluating Efficient Büchi Universality Checking ⋮ Domains for Higher-Order Games ⋮ Unnamed Item ⋮ A verification-driven framework for iterative design of controllers
Uses Software
