Fluid Model Checking of Timed Properties

TitleFluid Model Checking of Timed Properties
Publication TypeConference Paper
Year of Publication2015
AuthorsBortolussi L, Lanciani R
Conference NameFormal Modeling and Analysis of Timed Systems (FORMATS)
PublisherSpringer International Publishing
KeywordsDelay differential equations; Deterministic timed automata, fluid approximation, Fluid model checking, Stochastic model checking, Time-inhomogeneous markov renewal processes

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.