Local abstraction refinement for probabilistic timed programs

DOI10.1016/j.tcs.2013.07.013zbMath1359.68187MaRDI QIDQ2453108

Yanyan Li

Publication date: 6 June 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2013.07.013

zbMATH Keywords

abstraction refinement; probabilistic verification

Mathematics Subject Classification ID

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

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Uses Software

• PRISM
• PASS
• CEGAR
• MathSAT

Cites Work

• Unnamed Item
• Unnamed Item
• A game-based abstraction-refinement framework for Markov decision processes
• The existence of refinement mappings
• Performance analysis of probabilistic timed automata using digital clocks
• Automatic verification of real-time systems with discrete probability distributions.
• Symbolic model checking for probabilistic timed automata
• Efficient generation of craig interpolants in satisfiability modulo theories
• Probabilistic CEGAR
• A Framework for Verification of Software with Time and Probabilities
• Abstraction Refinement for Probabilistic Software
• Stochastic Games for Verification of Probabilistic Timed Automata
• Best Probabilistic Transformers
• Markov Chains
• Lectures on Concurrency and Petri Nets