Büchi Complementation and Size-Change Termination

DOI10.1007/978-3-642-00768-2_2zbMath1234.68256arXiv1110.6183OpenAlexW1548996544MaRDI QIDQ3617751

Seth Fogarty, Moshe Y. Vardi

Publication date: 31 March 2009

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1110.6183

Mathematics Subject Classification ID

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

Related Items (10)

Ramsey-Based Inclusion Checking for Visibly Pushdown Automata ⋮ Size-Change Termination and Satisfiability for Linear-Time Temporal Logics ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Fixed point guided abstraction refinement for alternating automata ⋮ Linear temporal logic symbolic model checking ⋮ Coinductive Algorithms for Büchi Automata ⋮ State of Büchi Complementation ⋮ Advanced Ramsey-Based Büchi Automata Inclusion Testing ⋮ Random Models for Evaluating Efficient Büchi Universality Checking ⋮ Unnamed Item

Cites Work

• Unnamed Item
• The complementation problem for Büchi automata with applications to temporal logic
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Weak alternating automata are not that weak
• Deciding full branching time logic
• The size-change principle for program termination
• Experimental Evaluation of Classical Automata Constructions
• Automata-Theoretic Model Checking Revisited
• Programming Languages and Systems
• Improved Algorithms for the Automata-Based Approach to Model-Checking

This page was built for publication: Büchi Complementation and Size-Change Termination