Pushdown processes: Games and model-checking

DOI10.1006/inco.2000.2894zbMath1003.68072OpenAlexW3022006420MaRDI QIDQ1854405

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.2000.2894

Mathematics Subject Classification ID

2-person games (91A05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

On the positional determinacy of edge-labeled games ⋮ Reactive synthesis from visibly register pushdown automata ⋮ Abstraction in Fixpoint Logic ⋮ A Branching Time Variant of CaRet ⋮ Hyperplane separation technique for multidimensional mean-payoff games ⋮ μ-Bicomplete Categories and Parity Games ⋮ Model-checking structured context-free languages ⋮ Modular strategies for recursive game graphs ⋮ DP lower bounds for equivalence-checking and model-checking of one-counter automata ⋮ Model-checking CTL* over flat Presburger counter systems ⋮ Marking shortest paths on pushdown graphs does not preserve MSO decidability ⋮ Model Checking Procedural Programs ⋮ Graph Games and Reactive Synthesis ⋮ Infinite games specified by 2-tape automata ⋮ Inverse monoids: decidability and complexity of algebraic questions. ⋮ Deciding Parity Games in Quasi-polynomial Time ⋮ Weighted Automata on Infinite Words in the Context of Attacker-Defender Games ⋮ Games for active XML revisited ⋮ Unnamed Item ⋮ Branching-time logics with path relativisation ⋮ Finite-state strategies in delay games ⋮ Automatic verification of recursive procedures with one integer parameter. ⋮ Model checking of pushdown systems for projection temporal logic ⋮ A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct ⋮ Improved model checking of hierarchical systems ⋮ Complete SAT-Based Model Checking for Context-Free Processes ⋮ Fixpoint logics over hierarchical structures ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On effective construction of the greatest solution of language inequality $XA\subseteq BX$ ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Operator precedence temporal logic and model checking ⋮ Reachability in recursive Markov decision processes ⋮ Bounding Average-Energy Games ⋮ Unnamed Item ⋮ Krivine machines and higher-order schemes ⋮ COMPLETE SAT-BASED MODEL CHECKING FOR CONTEXT-FREE PROCESSES ⋮ Krivine Machines and Higher-Order Schemes ⋮ Visibly pushdown modular games ⋮ Partially commutative inverse monoids. ⋮ The Church problem for expansions of $(\mathbb{N},<)$ by unary predicates ⋮ On decidability and complexity of low-dimensional robot games ⋮ Weighted automata on infinite words in the context of attacker-defender games ⋮ Decidability of model checking with the temporal logic EF ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Unnamed Item ⋮ Three notes on the complexity of model checking fixpoint logic with chop ⋮ On the complexity of checking semantic equivalences between pushdown processes and finite-state processes ⋮ Games on Multi-stack Pushdown Systems ⋮ Topological properties of omega context-free languages ⋮ Free $\mu$-lattices ⋮ On Robot Games of Degree Two ⋮ Simplification Problems for Deterministic Pushdown Automata on Infinite Words ⋮ PDL with intersection and converse: satisfiability and infinite-state model checking ⋮ Note on winning positions on pushdown games with $\omega$-regular conditions ⋮ Automata, Logic and Games for the $$\lambda $$ -Calculus ⋮ Optimally Resilient Strategies in Pushdown Safety Games ⋮ Model Checking FO(R) over One-Counter Processes and beyond ⋮ Games on Higher Order Multi-stack Pushdown Systems ⋮ Linear-time temporal logics with Presburger constraints: an overview ★ ⋮ Automata on infinite trees ⋮ THE COMPLEXITY OF COVERAGE ⋮ Domains for Higher-Order Games ⋮ Simulation preorder over simple process algebras ⋮ Automated formal analysis and verification: an overview ⋮ Games with winning conditions of high Borel complexity

Cites Work