Fluid Model Checking of Timed Properties

TL;DR

This paper presents a fluid approximation method for verifying timed properties of large populations modeled as Markovian automata, using Delay Differential Equations to efficiently estimate satisfaction probabilities.

Contribution

It introduces a novel fluid approximation approach that reduces the verification of timed properties to solving DDEs, with proven asymptotic convergence and practical exemplification.

Findings

The method accurately estimates satisfaction probabilities.

The approach converges asymptotically.

Efficiently approximates the average number of satisfying agents.

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.