Local abstraction refinement for probabilistic timed programs

DOI10.1016/J.TCS.2013.07.013MaRDI QIDQ2453108zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 6 June 2014

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

abstraction refinementprobabilistic verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstraction Refinement for Probabilistic Software
• Modal stochastic games. Abstraction-refinement of probabilistic automata
• Variable probabilistic abstraction refinement
• scientific article; zbMATH DE number 1884411
• Stochastic games for verification of probabilistic timed automata

Cites work

• scientific article; zbMATH DE number 3543391 (Why is no real title available?)
• scientific article; zbMATH DE number 1884411 (Why is no real title available?)
• A framework for verification of software with time and probabilities
• A game-based abstraction-refinement framework for Markov decision processes
• Abstraction Refinement for Probabilistic Software
• Automatic verification of real-time systems with discrete probability distributions.
• Best probabilistic transformers
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Lectures on Concurrency and Petri Nets
• Markov Chains
• Performance analysis of probabilistic timed automata using digital clocks
• Probabilistic CEGAR
• Stochastic games for verification of probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• The existence of refinement mappings

Cited in

(3)

• Abstraction Refinement for Probabilistic Software
• Variable probabilistic abstraction refinement
• Refinement of trace abstraction for real-time programs

Describes a project that uses

Uses Software

• MathSAT
• CEGAR
• PASS
• PRISM

This page was built for publication: Local abstraction refinement for probabilistic timed programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2453108)