Fluid Model Checking of Timed Properties
Fluid Model Checking of Timed Properties
复制标题
定时特性的流体模型检查
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Roberta Lanciani
中科院分区：
文献类型：
--
作者：
L. Bortolussi;Roberta Lanciani
我们讨论了用有限状态自动机建模的大量相互作用的智能体的马尔可夫模型的时间性质的验证问题。特别地，我们关注由赋予单个时钟的确定性时间自动机(DTA)指定的(随机)个体代理的时间有界性质。利用流体近似的思想，我们估计了DTA性质的满足概率，通过将其归结为一类具有指数和确定性时间转移的小状态空间的非齐次马尔可夫更新过程的瞬时概率的计算。对于这类模型，我们给出了一组延迟微分方程(DDE)，其数值解给出了满意概率的快速而准确的估计。在本文中，我们还证明了该方法的渐近收敛，并在一个简单的流行病传播模型上给出了该方法的例子。最后，我们还展示了如何构造一个DDES系统来有效地近似满足DTA规范的平均代理数量。
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.
影响因子：
7.4
作者：
R. A. Hayden;J. Bradley;Allan Clark
通讯作者：
R. A. Hayden;J. Bradley;Allan Clark