Model Checking Probabilistic Pushdown Automata

DOI10.2168/LMCS-2(1:2)2006zbMath1126.68053OpenAlexW3099666054MaRDI QIDQ5310649

Javier Esparza, Richard Mayr, Antonín Kučera

Publication date: 11 October 2007

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2168/lmcs-2(1:2)2006

Mathematics Subject Classification ID

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

Related Items (25)

Polynomial Time Algorithms for Branching Markov Decision Processes and Probabilistic Min(Max) Polynomial Bellman Equations ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ Greatest fixed points of probabilistic min/max polynomial equations, and reachability for branching Markov decision processes ⋮ Querying probabilistic business processes for sub-flows ⋮ On the Existence and Computability of Long-Run Average Properties in Probabilistic VASS ⋮ Branching-time model-checking of probabilistic pushdown automata ⋮ Recursive stochastic games with positive rewards ⋮ Satisfiability of quantitative probabilistic CTL: rise to the challenge ⋮ Model Checking Temporal Properties of Recursive Probabilistic Programs ⋮ Probabilistic total store ordering ⋮ A Polynomial Time Algorithm for Computing Extinction Probabilities of Multitype Branching Processes ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Model checking probabilistic systems against pushdown specifications ⋮ Derivation Tree Analysis for Accelerated Fixed-Point Computation ⋮ Deciding Fast Termination for Probabilistic VASS with Nondeterminism ⋮ Model checking with probabilistic tabled logic programming ⋮ Derivation tree analysis for accelerated fixed-point computation ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Stochastic Games with Lossy Channels ⋮ Verification of probabilistic systems with faulty communication

This page was built for publication: Model Checking Probabilistic Pushdown Automata