Automatic verification of competitive stochastic systems

DOI10.1007/S10703-013-0183-7zbMath1291.68252OpenAlexW2899043600MaRDI QIDQ2248068

Yanyan Li

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-013-0183-7

zbMATH Keywords

quantitative verificationprobabilistic model checkingprobabilistic temporal logicstochastic multi-player games

Mathematics Subject Classification ID

Probability and inductive logic (03B48) Stochastic games, stochastic differential games (91A15) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (16)

Model Checking Probabilistic Systems ⋮ A computationally grounded, weighted doxastic logic ⋮ Compositional strategy synthesis for stochastic games with multiple objectives ⋮ Automatic verification of concurrent stochastic systems ⋮ Modeling and analysis of the obstacle-avoidance strategies for a mobile robot in a dynamic environment ⋮ Value iteration for simple stochastic games: stopping criterion and learning algorithm ⋮ Automated Verification of Concurrent Stochastic Games ⋮ Symbolic verification and strategy synthesis for turn-based stochastic games ⋮ Optimistic and topological value iteration for simple stochastic games ⋮ Formal modelling and verification of probabilistic resource bounded agents ⋮ Model Checking Exact Cost for Attack Scenarios ⋮ Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability games ⋮ A uniformization-based algorithm for continuous-time stochastic games model checking ⋮ Unnamed Item ⋮ Comparison of algorithms for simple stochastic games ⋮ Verification of multiplayer stochastic games via abstract dependency graphs

Uses Software

• PRISM
• MCMAS
• GIST
• MOCHA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A logic for reasoning about time and reliability
• An Algorithm for Probabilistic Alternating Simulation
• Automatic Verification of Competitive Stochastic Systems
• Model checking of probabilistic and nondeterministic systems
• Verifying Team Formation Protocols with Probabilistic Model Checking
• On Probabilistic Alternating Simulations
• Computationally Sound Analysis of a Probabilistic Contract Signing Protocol
• Alternating-time temporal logic
• Value Iteration
• The determinacy of Blackwell games
• The complexity of probabilistic verification
• Results on the quantitative μ-calculus qM μ
• Formal Modeling and Analysis of Timed Systems
• On the Expressiveness and Complexity of ATL

This page was built for publication: Automatic verification of competitive stochastic systems