The complementation problem for Büchi automata with applications to temporal logic

DOI10.1016/0304-3975(87)90008-9zbMath0613.03015OpenAlexW1976773489MaRDI QIDQ1088653

Publication date: 1987

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(87)90008-9

zbMATH Keywords

satisfiability problem infinite words decision procedure extended temporal logic complementing Büchi automata omega regularity repeating acceptance

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15)

Related Items (79)

Ramsey-Based Inclusion Checking for Visibly Pushdown Automata ⋮ Model-Checking HyperLTL for Pushdown Systems ⋮ Ultimately periodic words of rational ω-languages ⋮ Effective Synthesis of Asynchronous Systems from GR(1) Specifications ⋮ Progress measures, immediate determinacy, and a subset construction for tree automata ⋮ Fair Petri nets and structural induction for rings of processes ⋮ Temporal Logic and Fair Discrete Systems ⋮ Automata Theory and Model Checking ⋮ Functional Specification of Hardware via Temporal Logic ⋮ Prognosis of \(\omega\)-languages for the diagnosis of *-languages: a topological perspective ⋮ Imperfect information in reactive modules games ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ Unnamed Item ⋮ Invariant-free clausal temporal resolution ⋮ Bounded model checking of ETL cooperating with finite and looping automata connectives ⋮ Using automata theory for characterizing the semantics of terminological cycles ⋮ Specification and verification of data-driven Web applications ⋮ Temporal equilibrium logic: a survey ⋮ Reasoning About Strategies ⋮ The refinement calculus of reactive systems ⋮ Unnamed Item ⋮ Program schemata vs. automata for decidability of program logics ⋮ On the power of finite ambiguity in Büchi complementation ⋮ PARTIALLY ORDERED TWO-WAY BÜCHI AUTOMATA ⋮ Specifiable robustness in reactive synthesis ⋮ Towards a grand unification of Büchi complementation constructions ⋮ Reasoning About Substructures and Games ⋮ Unambiguous Büchi automata. ⋮ An algorithmic approach for checking closure properties of Ω-regular languages ⋮ Realizability problem for constraint LTL ⋮ Automated temporal equilibrium analysis: verification and synthesis of multi-player games ⋮ Unnamed Item ⋮ Complexity of Topological Properties of Regular ω-Languages ⋮ Simple interpretations among complicated theories ⋮ Linear temporal logic symbolic model checking ⋮ An automatic method for the dynamic construction of abstractions of states of a formal model ⋮ Refinement modal logic ⋮ Multi-player games with LDL goals over finite traces ⋮ Deciding properties of integral relational automata ⋮ Cellular automata, \(\omega{} \omega\)-regular sets, and sofic systems ⋮ Büchi Store: An Open Repository of Büchi Automata ⋮ A compositional automata-based semantics and preserving transformation rules for testing property patterns ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Dynamic logic assigned to automata ⋮ Serializable histories in quantified propositional temporal logic ⋮ Propositional Dynamic Logic with Program Quantifiers ⋮ Fragments of first-order logic over infinite words ⋮ On the complexity of verifying concurrent transition systems ⋮ Fair simulation ⋮ Decidability of infinite-state timed CCP processes and first-order LTL ⋮ From Philosophical to Industrial Logics ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Unnamed Item ⋮ From Monadic Logic to PSL ⋮ Automata-Theoretic Model Checking Revisited ⋮ A theory of ultimately periodic languages and automata with an application to time granularity ⋮ Büchi Complementation and Size-Change Termination ⋮ Partially Ordered Two-Way Büchi Automata ⋮ State of Büchi Complementation ⋮ Using partial orders for the efficient verification of deadlock freedom and safety properties ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ Random Models for Evaluating Efficient Büchi Universality Checking ⋮ Event-clock automata: a determinizable class of timed automata ⋮ A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages ⋮ BÜCHI COMPLEMENTATION MADE TIGHTER ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ On the Expressiveness of Temporal Equilibrium Logic ⋮ Deductive verification of simple foraging robotic behaviours ⋮ From liveness to promptness ⋮ Systolic tree \(\omega\)-languages: The operational and the logical view ⋮ Verification of multi-agent systems with public actions against strategy logic ⋮ Unnamed Item ⋮ From complementation to certification ⋮ Fair simulation ⋮ On the complexity of verifying concurrent transition systems ⋮ On deciding trace equivalences for processes ⋮ A theory of timed automata ⋮ Good-for-Game QPTL: An Alternating Hodges Semantics

Cites Work

This page was built for publication: The complementation problem for Büchi automata with applications to temporal logic