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)

• 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
• Concurrent Kleene algebra with observations: from hypotheses to completeness
• The modal \(\mu \)-calculus caught off guard
• Probabilistic temporal logics via the modal mu-calculus
• Generalising automaticity to modal properties of finite structures
• A parametric analysis of the state-explosion problem in model checking
• A delayed promotion policy for parity games
• Cycle detection in computation tree logic
• A delayed promotion policy for parity games
• Deciding the unguarded modal \(\mu\)-calculus
• Incremental reasoning on monadic second-order logics with logic programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Obligation Blackwell games and p-automata
• Taming strategy logic: non-recurrent fragments
• Flow logic
• Fuzzy alternating Büchi automata over distributive lattices
• GSTE is partitioned model checking
• Branching-Time Temporal Logics with Minimal Model Quantifiers
• Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
• Title not available (Why is that?)
• Model-checking iterated games
• Cooperative concurrent games
• Weighted automata on infinite words in the context of attacker-defender games
• Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree Automata
• Reasoning about Quality and Fuzziness of Strategic Behaviors
• On the comparison of discounted-sum automata with multiple discount factors
• Reasoning About Regular Properties: A Comparative Study
• Reasoning About Substructures and Games
• Easy Yet Hard: Model Checking Strategies of Agents
• Equivalence of probabilistic \(\mu\)-calculus and p-automata
• On temporal logic versus Datalog
• Extending co-logic programs for branching-time model checking
• Multi-Valued Reasoning about Reactive Systems
• A model of finite automata on timed omega-trees
• On robot games of degree two
• Distributed automata in an assumption-commitment framework
• An Operational Guide to Monitorability
• 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

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)