Model Checking Probabilistic Pushdown Automata

DOI10.2168/LMCS-2(1:2)2006zbMath1126.68053MaRDI 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

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

03B44: Temporal logic

Related Items

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