Fluid model checking of timed properties
From MaRDI portal
delay differential equationsdeterministic timed automatafluid approximationfluid model checkingstochastic model checkingtime-inhomogeneous Markov renewal processes
Stochastic functional-differential equations (34K50) Applications of Markov renewal processes (reliability, queueing networks, etc.) (60K20) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Abstract: We address the problem of verifying timed properties of Markovian models of large populations of interacting agents, modelled as finite state automata. In particular, we focus on time-bounded properties of (random) individual agents specified by Deterministic Timed Automata (DTA) endowed with a single clock. Exploiting ideas from fluid approximation, we estimate the satisfaction probability of the DTA properties by reducing it to the computation of the transient probability of a subclass of Time-Inhomogeneous Markov Renewal Processes with exponentially and deterministically-timed transitions, and a small state space. For this subclass of models, we show how to derive a set of Delay Differential Equations (DDE), whose numerical solution provides a fast and accurate estimate of the satisfaction probability. In the paper, we also prove the asymptotic convergence of the approach, and exemplify the method on a simple epidemic spreading model. Finally, we also show how to construct a system of DDEs to efficiently approximate the average number of agents that satisfy the DTA specification.
Recommendations
- Fluid model checking
- Model checking single agent behaviours by fluid approximation
- Checking individual agent behaviours in Markov population models by fluid approximation
- Model checking Markov population models by stochastic approximations
- Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Cites work
- A theory of timed automata
- Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
- Differential equation approximations for Markov chains
- Efficient CTMC Model Checking of Linear Real-Time Objectives
- Fluid model checking
- scientific article; zbMATH DE number 1629917 (Why is no real title available?)
- scientific article; zbMATH DE number 3532286 (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?)
- Implementing Radau IIA methods for stiff delay differential equations
- Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
- Model checking single agent behaviours by fluid approximation
- Observing continuous-time MDPs by 1-clock timed automata
- On-the-fly fast mean-field model-checking
- Stochastic epidemic models and their statistical analysis
- Verification of linear duration properties over continuous-time Markov chains
Cited in
(7)- Model checking Markov population models by stochastic approximations
- Fluid approximation of broadcasting systems
- Mean-field limits beyond ordinary differential equations
- Fluid model checking
- Fluid analysis of spatio-temporal properties of agents in a population model
- Checking individual agent behaviours in Markov population models by fluid approximation
- Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
This page was built for publication: Fluid model checking of timed properties
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945594)
