Model Checking Probabilistic Pushdown Automata
From MaRDI portal
Publication:5310649
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
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