An automata-theoretic approach to branching-time model checking
From MaRDI portal
Publication:5385339
DOI10.1145/333979.333987zbMath1133.68376OpenAlexW1988808695MaRDI QIDQ5385339
Pierre Wolper, Orna Kupferman, Moshe Y. Vardi
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
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items (only showing first 100 items - show all)
Model Checking Information Flow in Reactive Systems ⋮ Model checking \(\omega \)-regular properties with decoupled search ⋮ On the universal and existential fragments of the \(\mu\)-calculus ⋮ Complete axiomatization and decidability of alternating-time temporal logic ⋮ Efficient timed model checking for discrete-time systems ⋮ Specification and Verification of Multi-Agent Systems ⋮ Generalising automaticity to modal properties of finite structures ⋮ Complexity results on branching-time pushdown model checking ⋮ Permissive strategies: from parity games to safety games ⋮ Model measuring for discrete and hybrid systems ⋮ Temporal Logic and Fair Discrete Systems ⋮ Automata Theory and Model Checking ⋮ Extending Co-logic Programs for Branching-Time Model Checking ⋮ Knowledge base exchange: the case of OWL 2 QL ⋮ Practical verification of multi-agent systems against \textsc{Slk} specifications ⋮ Graded modalities in strategy logic ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ GSTE is partitioned model checking ⋮ Coverage metrics for temporal logic model checking ⋮ Diagnosability of fair transition systems ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ Reasoning about equilibria in game-like concurrent systems ⋮ Logic programming approach to automata-based decision procedures ⋮ Weighted Automata on Infinite Words in the Context of Attacker-Defender Games ⋮ Equivalence of probabilistic \(\mu\)-calculus and p-automata ⋮ From model checking to equilibrium checking: reactive modules for rational verification ⋮ Specification and verification of data-driven Web applications ⋮ Model-checking iterated games ⋮ Fuzzy alternating Büchi automata over distributive lattices ⋮ Deciding the unguarded modal -calculus ⋮ Reasoning About Strategies ⋮ Enriched μ–Calculus Pushdown Module Checking ⋮ Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable ⋮ Cooperative concurrent games ⋮ Reasoning About Substructures and Games ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ On feasible cases of checking multi-agent systems behavior. ⋮ On temporal logic versus Datalog ⋮ Multi-valued model checking games ⋮ Improved model checking of hierarchical systems ⋮ Concurrent Kleene algebra with observations: from hypotheses to completeness ⋮ Unnamed Item ⋮ Reasoning about sequences of memory states ⋮ ATL* Satisfiability Is 2EXPTIME-Complete ⋮ Complexity of synthesis of composite service with correctness guarantee ⋮ \textit{Once} and \textit{for all} ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Hierarchical cost-parity games ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Temporal property verification as a program analysis task ⋮ Explaining counterexamples using causality ⋮ Linear temporal logic symbolic model checking ⋮ Run-Time Monitoring of Electronic Contracts ⋮ Conditions of contracts for separating responsibilities in heterogeneous systems ⋮ The Modal μ-Calculus Caught Off Guard ⋮ Alternating-time temporal logics with linear past ⋮ Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\) ⋮ Visibly linear temporal logic ⋮ Unnamed Item ⋮ Model checking abilities of agents: a closer look ⋮ Pushdown module checking ⋮ On decidability and complexity of low-dimensional robot games ⋮ \(\varSigma^{\mu}_2\) is decidable for \(\varPi^{\mu}_2\) ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Weighted automata on infinite words in the context of attacker-defender games ⋮ An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus ⋮ PSPACE-completeness of modular supervisory control problems ⋮ A parametric analysis of the state-explosion problem in model checking ⋮ CTL\(^\ast\) with graded path modalities ⋮ A delayed promotion policy for parity games ⋮ Cycle detection in computation tree logic ⋮ On modal \(\mu\)-calculus with explicit interpolants ⋮ Model-checking graded computation-tree logic with finite path semantics ⋮ On Robot Games of Degree Two ⋮ Improving parity games in practice ⋮ Quantifying Bounds in Strategy Logic ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ Branching-Time Temporal Logics with Minimal Model Quantifiers ⋮ OBLIGATION BLACKWELL GAMES AND P-AUTOMATA ⋮ Easy Yet Hard: Model Checking Strategies of Agents ⋮ EXPTIME Tableaux for the Coalgebraic μ-Calculus ⋮ Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree Automata ⋮ On the Complexity of Branching-Time Logics ⋮ Solving Parity Games Using an Automata-Based Algorithm ⋮ Symbolic model checking for \(\mu\)-calculus requires exponential time ⋮ A decidable class of problems for control under partial observation ⋮ Fuzzy alternating automata over distributive lattices ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ Distributed automata in an assumption-commitment framework ⋮ Relating word and tree automata ⋮ Complexity of weak acceptance conditions in tree automata. ⋮ Module checking ⋮ Fair simulation ⋮ On the complexity of verifying concurrent transition systems ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Uniform strategies, rational relations and jumping automata ⋮ Synthesis of succinct systems
Uses Software
This page was built for publication: An automata-theoretic approach to branching-time model checking
