An automata-theoretic approach to branching-time model checking

DOI10.1145/333979.333987zbMATH Open1133.68376OpenAlexW1988808695MaRDI QIDQ5385339FDOQ5385339

Authors: Orna Kupferman, Moshe Y. Vardi, Pierre Wolper 

Publication date: 5 May 2008

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/333979.333987

Recommendations

• Branching-time temporal logic and tree automata
• scientific article; zbMATH DE number 177521
• Alternating automata: unifying truth and validity checking for temporal logics
• Modalities for model checking: Branching time logic strikes back
• From linear time to branching time

Mathematics Subject Classification ID

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

Cited In (only showing first 100 items - show all)

• Modalities for model checking: Branching time logic strikes back
• Branching-time model-checking of probabilistic pushdown automata
• Improving parity games in practice
• Alternating automata: unifying truth and validity checking for temporal logics
• Run-Time Monitoring of Electronic Contracts
• Visibly linear temporal logic
• Title not available (Why is that?)
• Automata theory and model checking
• Model checking \(\omega \)-regular properties with decoupled search
• Model Checking Information Flow in Reactive Systems
• Symbolic model checking for \(\mu\)-calculus requires exponential time
• On the universal and existential fragments of the \(\mu\)-calculus
• Efficient timed model checking for discrete-time systems
• Multi-valued model checking games
• Improved model checking of hierarchical systems
• Quantifying Bounds in Strategy Logic
• On the Complexity of Branching-Time Logics
• Reasoning about sequences of memory states
• Lattice Automata
• Complexity of weak acceptance conditions in tree automata.
• Module checking
• Specification and verification of data-driven Web applications
• How to translate efficiently extensions of temporal logics into alternating automata
• Model checking abilities of agents: a closer look
• PSPACE-completeness of modular supervisory control problems
• On decidability and complexity of low-dimensional robot games
• Weighted automata on infinite words in the context of attacker-defender games
• An automata-theoretic approach to infinite-state systems
• Complexity of synthesis of composite service with correctness guarantee
• \textit{Once} and \textit{for all}
• The Complexity of CTL* + Linear Past
• Temporal property verification as a program analysis task
• Knowledge base exchange: the case of OWL 2 QL
• Coverage metrics for temporal logic model checking
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Explaining counterexamples using causality
• Temporal logic and fair discrete systems
• Complexity results on branching-time pushdown model checking
• On the complexity of verifying concurrent transition systems
• Permissive strategies: from parity games to safety games
• An automata-based approach for \(\text{CTL}^{*}\) with constraints
• Solving parity games using an automata-based algorithm
• Fair simulation
• A Parametrized Analysis of Algorithms on Hierarchical Graphs
• Title not available (Why is that?)
• Verification, Model Checking, and Abstract Interpretation
• Diagnosability of fair transition systems
• A decidable class of problems for control under partial observation
• Query learning of derived \(\omega\)-tree languages in polynomial time
• Automata-Theoretic Model Checking Revisited
• Linear temporal logic symbolic model checking
• Tool support for learning Büchi automata and linear temporal logic
• An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus
• From model checking to equilibrium checking: reactive modules for rational verification
• On temporal logics with data variable quantifications: decidability and complexity
• Reasoning about equilibria in game-like concurrent systems
• On modal \(\mu\)-calculus with explicit interpolants
• Title not available (Why is that?)
• Specification and Verification of Multi-Agent Systems
• Logic programming approach to automata-based decision procedures
• Alternating nonzero automata
• Fuzzy alternating automata over distributive lattices
• Efficient CTL verification via Horn constraints solving
• On feasible cases of checking multi-agent systems behavior.
• Reasoning about strategies: on the model-checking problem
• EXPTIME Tableaux for the Coalgebraic μ-Calculus
• Polynomial identification of \(\omega \)-automata
• Pushdown module checking
• Title not available (Why is that?)
• Automata-theoretic techniques for modal logics of programs
• TYPENESS FOR ω-REGULAR AUTOMATA
• On the expressivity and complexity of quantitative branching-time temporal logics
• Graded modalities in strategy logic
• Practical verification of multi-agent systems against \textsc{Slk} specifications
• Complete axiomatization and decidability of alternating-time temporal logic
• Title not available (Why is that?)
• Model Checking Quantitative Linear Time Logic
• Automata, Logic and Games for the $$\lambda $$ -Calculus
• Hierarchical cost-parity games
• The regular viewpoint on PA-processes
• ATL* Satisfiability Is 2EXPTIME-Complete
• Uniform strategies, rational relations and jumping automata
• On the complexity of \(\mathsf{ATL}\) and \(\mathsf{ATL}^*\) module checking
• Relating word and tree automata
• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• Size-change termination and satisfiability for linear-time temporal logics
• Enriched μ–Calculus Pushdown Module Checking
• Model-checking graded computation-tree logic with finite path semantics
• Using assumptions to distribute CTL model checking
• Language-emptiness checking of alternating tree automata using symbolic reachability analysis
• CTL\(^\ast\) with graded path modalities
• Title not available (Why is that?)
• Conditions of contracts for separating responsibilities in heterogeneous systems
• \(\varSigma^{\mu}_2\) is decidable for \(\varPi^{\mu}_2\)
• Formal Modeling and Analysis of Timed Systems
• Results on alternating-time temporal logics with linear past
• Alternating-time temporal logics with linear past
• Synthesis of succinct systems
• Model measuring for discrete and hybrid systems
• The descriptive complexity of modal \(\mu\) model-checking games

Uses Software

• CESAR

This page was built for publication: An automata-theoretic approach to branching-time model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5385339)