The complexity of probabilistic verification
From MaRDI portal
Publication:4369884
DOI10.1145/210332.210339zbMath0885.68109OpenAlexW1972203711MaRDI QIDQ4369884
Mihalis Yannakakis, Costas Courcoubetis
Publication date: 28 January 1998
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/210332.210339
Related Items
On the power of finite ambiguity in Büchi complementation ⋮ Markov chains and unambiguous automata ⋮ An impossibility result in automata-theoretic reinforcement learning ⋮ Action and State Based Computation Tree Measurement Language and Algorithms ⋮ Satisfiability of quantitative probabilistic CTL: rise to the challenge ⋮ Optimal deterministic controller synthesis from steady-state distributions ⋮ Alternating good-for-MDPs automata ⋮ Operational causality -- necessarily sufficient and sufficiently necessary ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Combinations of Qualitative Winning for Stochastic Parity Games ⋮ On simulation-based probabilistic model checking of mixed-analog circuits ⋮ Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games ⋮ Unnamed Item ⋮ What is decidable about partially observable Markov decision processes with \(\omega\)-regular objectives ⋮ Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning ⋮ Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ A note on the verification of automata specifications of probabilistic real-time systems ⋮ Spanning the spectrum from safety to liveness ⋮ The Complexity of Synthesis from Probabilistic Components ⋮ Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ A logic for reasoning about time and reliability ⋮ On fairness and randomness ⋮ Model Checking Probabilistic Systems ⋮ State explosion in almost-sure probabilistic reachability ⋮ Model Checking of Biological Systems ⋮ Determinization and limit-determinization of Emerson-Lei automata ⋮ The Effect of Tossing Coins in Omega-Automata ⋮ Probabilistic Weighted Automata ⋮ Counterexamples in Probabilistic LTL Model Checking for Markov Chains ⋮ Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Strategy improvement for concurrent reachability and turn-based stochastic safety games ⋮ Metrics for labelled Markov processes ⋮ Symbolic model checking for probabilistic processes ⋮ Parallel local search ⋮ Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL ⋮ Learning deterministic probabilistic automata from a model checking perspective ⋮ Approximating labelled Markov processes ⋮ Model checking differentially private properties ⋮ On the use of MTBDDs for performability analysis and verification of stochastic systems. ⋮ Profile trees for Büchi word automata, with application to determinization ⋮ A survey of stochastic \(\omega \)-regular games ⋮ Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games ⋮ Value Iteration ⋮ Recurrence and transience for finite probabilistic tables ⋮ Moving in a network under random failures: a complexity analysis ⋮ Unnamed Item ⋮ Model checking probabilistic systems against pushdown specifications ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Probabilistic opacity for Markov decision processes ⋮ From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata ⋮ Optimal Translation of LTL to Limit Deterministic Automata ⋮ Decidable and expressive classes of probabilistic automata ⋮ The complexity of synchronizing Markov decision processes ⋮ Concurrent games with tail objectives ⋮ On relative and probabilistic finite counterability ⋮ Non-deterministic Weighted Automata on Random Words ⋮ Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components ⋮ Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives ⋮ Automatic verification of competitive stochastic systems ⋮ Preface to the special issue on probabilistic model checking ⋮ Bayesian statistical model checking with application to Stateflow/Simulink verification ⋮ Probabilistic verification and approximation ⋮ Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games ⋮ Model Checking Quantitative Linear Time Logic ⋮ Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking ⋮ Deciding probabilistic bisimilarity over infinite-state probabilistic systems ⋮ Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives ⋮ The well-designed logical robot: learning and experience from observations to the Situation Calculus ⋮ Non-deterministic weighted automata evaluated over Markov chains ⋮ Quantitative analysis of probabilistic lossy channel systems ⋮ Stochastic game logic ⋮ Probabilistic Acceptors for Languages over Infinite Words ⋮ Timed vacuity ⋮ Unnamed Item ⋮ Recursive Markov Decision Processes and Recursive Stochastic Games ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness ⋮ Computation tree measurement language (CTML) ⋮ On Decision Problems for Probabilistic Büchi Automata ⋮ Model-Checking ω-Regular Properties of Interval Markov Chains ⋮ Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths ⋮ A temporal negative normal form which preserves implicants and implicates ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ A novel learning algorithm for Büchi automata based on family of DFAs and classification trees ⋮ Carrying Probabilities to the Infinite World ⋮ Two Variable vs. Linear Temporal Logic in Model Checking and Games ⋮ Weighted versus Probabilistic Logics ⋮ Model-Free Reinforcement Learning for Stochastic Parity Games ⋮ OBLIGATION BLACKWELL GAMES AND P-AUTOMATA ⋮ Unnamed Item ⋮ Decision Problems for Nash Equilibria in Stochastic Games ⋮ LTL Model Checking of Time-Inhomogeneous Markov Chains ⋮ Quantitative Analysis under Fairness Constraints ⋮ \( \omega \)-automata ⋮ THE COMPLEXITY OF COVERAGE ⋮ Classes of Timed Automata and the Undecidability of Universality ⋮ The probability nesting game ⋮ Model Checking Omega-regular Properties for Quantum Markov Chains ⋮ A note on the attractor-property of infinite-state Markov chains ⋮ Measuring and Synthesizing Systems in Probabilistic Environments ⋮ Verification of probabilistic systems with faulty communication ⋮ On finite-state approximants for probabilistic computation tree logic ⋮ Bounds for synchronizing Markov decision processes ⋮ On probabilistic timed automata. ⋮ Comparison of algorithms for simple stochastic games ⋮ Complexity of model checking MDPs against LTL specifications ⋮ Testing preorders for probabilistic processes can be characterized by simulations ⋮ Optimal cost almost-sure reachability in POMDPs ⋮ Back to the future: a fresh look at linear temporal logic
