Generating counterexamples for quantitative safety specifications in probabilistic B

DOI10.1016/J.JLAP.2011.06.001MaRDI QIDQ652160zbMATH OpenOpenAlexWikidataFDO

Authors 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

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

Recommendations

• Counterexamples in Probabilistic Model Checking
• High-level counterexamples for probabilistic automata
• Bounded model checking for probabilistic programs
• Verification of Probabilistic Programs
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3776540 (Why is no real title available?)
• scientific article; zbMATH DE number 2013586 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• A logic for reasoning about time and reliability
• Abstraction, Refinement and Proof for Probabilistic Systems
• An axiomatic basis for computer programming
• Borel determinacy
• Counterexamples in Probabilistic Model Checking
• Finding the k Shortest Paths
• Formal Modeling and Analysis of Timed Systems
• Modeling in Event B. System and software engineering.
• Optimal control of diffusion processes with reflection
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Stochastic model checking
• The B-Book

Describes a project that uses

Uses Software

• CESAR
• ProB
• Rodin
• PRISM

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

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