Smoothed model checking for uncertain continuous-time Markov chains

DOI10.1016/j.ic.2016.01.004zbMath1336.68162arXiv1402.1450OpenAlexW2157413433MaRDI QIDQ259074

Dimitrios Milios, Luca Bortolussi, Guido Sanguinetti

Publication date: 10 March 2016

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

Full work available at URL: https://arxiv.org/abs/1402.1450

zbMATH Keywords

uncertaintyGaussian processesmodel checkingcontinuous-time Markov chains

Mathematics Subject Classification ID

Gaussian processes (60G15) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of continuous-time Markov processes on discrete state spaces (60J28) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (12)

Active and sparse methods in smoothed model checking ⋮ Precise parameter synthesis for stochastic biochemical systems ⋮ Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference ⋮ Parameter synthesis in Markov models: a gentle survey ⋮ A formal approach for tuning stochastic oscillators ⋮ Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes ⋮ Sampling-Based Verification of CTMCs with Uncertain Rates ⋮ Sequential Convex Programming for the Efficient Verification of Parametric MDPs ⋮ Automaton-ABC: a statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models ⋮ Geometric fluid approximation for general continuous-time Markov chains ⋮ Model checking Markov population models by stochastic approximations ⋮ Deniable Functional Encryption

Uses Software

• PRISM
• Bio-PEPA
• MRMC
• PARAM
• STOCKS
• PROPhESY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constraint Markov chains
• Stochastic epidemic models and their statistical analysis
• Bio-PEPA: A framework for the modelling and analysis of biological systems
• System design of stochastic models using robustness of temporal properties
• Statistical probabilistic model checking with a focus on time-bounded properties
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• 10.1162/153244302760185252
• Bayesian statistical model checking with application to Simulink/Stateflow verification
• Model Repair for Probabilistic Systems
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Markov Chains
• LTL Model Checking of Interval Markov Chains
• Three-Valued Abstraction for Continuous-Time Markov Chains
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Data-Driven Statistical Learning of Temporal Logic Properties
• Theoretical Aspects of Computing - ICTAC 2004
• Essentials of Stochastic Processes

This page was built for publication: Smoothed model checking for uncertain continuous-time Markov chains