Fluid model checking
From MaRDI portal
Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
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)- Hybrid behaviour of Markov population models
- Algorithms for Markov binomial chains
- Applying mean-field approximation to continuous time Markov chains
- Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
- Model checking functional and performability properties of stochastic fluid models
- On-the-fly fast mean-field model-checking
- Model checking Markov population models by stochastic approximations
- Fluid approximation-based analysis for mode-switching population dynamics
- Fluid analysis of spatio-temporal properties of agents in a population model
- 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
- Model checking of biological systems
- Model Checking for a Class of Performance Properties of Fluid Stochastic Models
- Fluid model checking of timed properties
- Model checking single agent behaviours by fluid approximation
- Checking individual agent behaviours in Markov population models by fluid approximation
- Central limit model checking
- \textsf{FlyFast}: a scalable approach to probabilistic model-checking based on mean-field approximation
- Fluid approximation of broadcasting systems
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)
