Generating counterexamples for quantitative safety specifications in probabilistic B

DOI10.1016/j.jlap.2011.06.001zbMath1269.68047OpenAlexW2126704329WikidataQ124807099 ScholiaQ124807099MaRDI QIDQ652160

Ukachukwu Ndukwu

Publication date: 19 December 2011

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2011.06.001

zbMATH Keywords

expectationscounterexamplesfailuresprobabilistic Bquantitative safety

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Uses Software

• PRISM
• Rodin
• ProB
• CESAR

Cites Work

• Borel determinacy
• Optimal control of diffusion processes with reflection
• A logic for reasoning about time and reliability
• Stochastic Model Checking
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• The B-Book
• Finding the k Shortest Paths
• Abstraction, Refinement and Proof for Probabilistic Systems
• An axiomatic basis for computer programming
• Counterexamples in Probabilistic Model Checking
• Formal Modeling and Analysis of Timed Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Generating counterexamples for quantitative safety specifications in probabilistic B