Statistical probabilistic model checking with a focus on time-bounded properties
From MaRDI portal
Publication:2509358
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
stochastic processeshypothesis testingtemporal logictransient analysisacceptance samplingprobabilistic verification
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
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