Model checking Markov population models by stochastic approximations
From MaRDI portal
stochastic approximationmaximum entropymoment closurepopulation modelslinear noisefluid model checkingstochastic model checking
Applications of continuous-time Markov processes on discrete state spaces (60J28) Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Abstract: Many complex systems can be described by population models, in which a pool of agents interacts and produces complex collective behaviours. We consider the problem of verifying formal properties of the underlying mathematical representation of these models, which is a Continuous Time Markov Chain, often with a huge state space. To circumvent the state space explosion, we rely on stochastic approximation techniques, which replace the large model by a simpler one, guaranteed to be probabilistically consistent. We show how to efficiently and accurately verify properties of random individual agents, specified by Continuous Stochastic Logic extended with Timed Automata (CSL-TA), and how to lift these specifications to the collective level, approximating the number of agents satisfying them using second or higher order stochastic approximation techniques.
Recommendations
- Checking individual agent behaviours in Markov population models by fluid approximation
- Model checking single agent behaviours by fluid approximation
- Fluid model checking
- Central limit model checking
- \textsf{FlyFast}: a scalable approach to probabilistic model-checking based on mean-field approximation
Cites work
- scientific article; zbMATH DE number 1670788 (Why is no real title available?)
- scientific article; zbMATH DE number 1817650 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 2237386 (Why is no real title available?)
- Abstraction Refinement for Probabilistic Software
- Approximation and inference methods for stochastic biochemical kinetics -- a tutorial review
- Approximation of probabilistic reachability for chemical reaction networks using the linear noise approximation
- Checking individual agent behaviours in Markov population models by fluid approximation
- Differential equation approximations for Markov chains
- Fluid computation of passage-time distributions in large Markov models
- Fluid model checking
- Fluid model checking of timed properties
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Gaussian processes for machine learning.
- Handbook of stochastic methods for physics, chemistry and the natural sciences.
- Markov Chains
- Model Reconstruction for Moment-Based Stochastic Chemical Kinetics
- Model checking single agent behaviours by fluid approximation
- Model-checking continuous-time Markov chains
- On the approximation of stochastic concurrent constraint programming by master equation
- Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
- Smoothed model checking for uncertain continuous-time Markov chains
- Stochastic epidemic models and their statistical analysis
- Stochastic processes in physics and chemistry.
- The multidimensional maximum entropy moment problem: a review on numerical methods
Cited in
(17)- Mean-field analysis of hybrid Markov population models with time-inhomogeneous rates
- Abstraction of Markov population dynamics via generative adversarial nets
- On-the-fly fast mean-field model-checking
- A Markov embedding approximation for a stochastic population model with exogenous disturbances
- Fluid analysis of spatio-temporal properties of agents in a population model
- Analysis of Markov jump processes under terminal constraints
- Formalisms for specifying Markovian population models
- Fluid model checking
- Fluid model checking of timed properties
- Approximation of large probabilistic networks by structured population protocols
- Checking individual agent behaviours in Markov population models by fluid approximation
- Central limit model checking
- Predicting the population growth and structure of China based on grey fractional-order models
- Bayesian Abstraction of Markov Population Models
- \textsf{FlyFast}: a scalable approach to probabilistic model-checking based on mean-field approximation
- A logical framework for reasoning about local and global properties of collective systems
- Formalisms for Specifying Markovian Population Models
This page was built for publication: Model checking Markov population models by stochastic approximations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1784959)
