Fluid Model Checking of Timed Properties
Title | Fluid Model Checking of Timed Properties |
Publication Type | Conference Paper |
Year of Publication | 2015 |
Authors | Bortolussi L, Lanciani R |
Conference Name | Formal Modeling and Analysis of Timed Systems (FORMATS) |
Volume | 9268 |
Series | LNCS |
Pages | 172–188 |
Publisher | Springer International Publishing |
Keywords | Delay differential equations; Deterministic timed automata, fluid approximation, Fluid model checking, Stochastic model checking, Time-inhomogeneous markov renewal processes |
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. |
DOI | 10.1007/978-3-319-22975-1_12 |