Fluid model checking
From MaRDI portal
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Abstract: In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC which depends on the environment and on the other agents only through the solution of the fluid differential equation. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae and of reachability probabilities. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.
Recommendations
- Model checking single agent behaviours by fluid approximation
- Checking individual agent behaviours in Markov population models by fluid approximation
- Fluid model checking of timed properties
- Model Checking for a Class of Performance Properties of Fluid Stochastic Models
- Model checking Markov population models by stochastic approximations
Cited in
(20)- Model checking Markov population models by stochastic approximations
- Fluid approximation of broadcasting systems
- Model checking single agent behaviours by fluid approximation
- Hybrid behaviour of Markov population models
- On-the-fly fast mean-field model-checking
- Model checking functional and performability properties of stochastic fluid models
- Applying mean-field approximation to continuous time Markov chains
- Fluid model checking of timed properties
- Model Checking for a Class of Performance Properties of Fluid Stochastic Models
- Fluid analysis of spatio-temporal properties of agents in a population model
- Central limit model checking
- \textsf{FlyFast}: a scalable approach to probabilistic model-checking based on mean-field approximation
- Model checking of biological systems
- Checking individual agent behaviours in Markov population models by fluid approximation
- Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
- Fluid approximation-based analysis for mode-switching population dynamics
- Algorithms for Markov binomial chains
- Design and optimisation of the FlyFast front-end for attribute-based coordination
- Efficient checking of individual rewards properties in Markov population models
- Stochastically timed predicate-based communication primitives for autonomic computing
This page was built for publication: Fluid model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2912688)
