Statistical probabilistic model checking with a focus on time-bounded properties

DOI10.1016/j.ic.2006.05.002zbMath1110.68077OpenAlexW2067971887MaRDI QIDQ2509358

Håkan L. S. Younes, Reid G. Simmons

Publication date: 19 October 2006

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2006.05.002

zbMATH Keywords

stochastic processeshypothesis testingtemporal logictransient analysisacceptance samplingprobabilistic verification

Mathematics Subject Classification ID

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

Related Items (20)

Abstraction of Markov population dynamics via generative adversarial nets ⋮ Probabilistic verification of a biodiesel production system using statistical model checking ⋮ On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets ⋮ Twenty years of rewriting logic ⋮ Generative abstraction of Markov population processes ⋮ Distribution estimation for probabilistic loops ⋮ Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference ⋮ Decoding Output Sequences for Discrete-Time Linear Hybrid Systems. ⋮ Poster Abstract: Decoding Output Sequences for Discrete-Time Linear Hybrid Systems. ⋮ Sampling-Based Verification of CTMCs with Uncertain Rates ⋮ Statistical Verification of Probabilistic Properties with Unbounded Until ⋮ Automaton-ABC: a statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models ⋮ Bayesian statistical model checking with application to Stateflow/Simulink verification ⋮ Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement ⋮ Faster statistical model checking for unbounded temporal properties ⋮ On simulation-based probabilistic model checking of mixed-analog circuits ⋮ Statistical Model Checking Using Perfect Simulation ⋮ Statistical verification of PCTL using antithetic and stratified samples ⋮ Read atomic transactions with prevention of lost updates: ROLA and its formal analysis ⋮ Smoothed model checking for uncertain continuous-time Markov chains

Uses Software

• PRISM
• Ymer

Cites Work

• Model-checking in dense real-time
• Numerical transient analysis of Markov models
• Nearly optimal sequential tests of composite hypotheses
• A theory of timed automata
• A logic for reasoning about time and reliability
• Model-checking large structured Markov chains.
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Discrete time methods for simulating continuous time Markov chains
• Fast simulation of rare events in queueing and reliability models
• Computer Aided Verification
• Asymptotic Shapes of Bayes Sequential Testing Regions
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Model-checking continuous-time Markov chains
• Optimum Character of the Sequential Probability Ratio Test
• On Designing Single Sampling Inspection Plans
• Sequential Tests of Statistical Hypotheses
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Statistical probabilistic model checking with a focus on time-bounded properties