Safety Verification Based on Fluidification of Discrete Dynamics

对于具有指数分布射击延迟的广义随机Petri网，我们提出了一种通过在流体模型上引入间隔射击速度来逼近每个地方概率分布方差的方法。接下来，我们证明了这些模型等价地表示为具有区间参数的分段线性系统。对于模型的仿真，提出了两种方法：一种是对常微分方程的区间方法的扩展，另一种是对连续状态系统的离散抽象技术——盒抽象的加速计算技术。

For generalized stochastic Petri nets with exponentially distributed firing delay, we propose a method for approximating variance of the probability distribution in each place by introducing interval firing speeds on the fluid model. We next show that the models are equivalently represented by piecewise linear systems with interval parameters. For simulation of the models, two methods are proposed : one is an extension of the interval methods for ordinary differential equations, and the other is acceleration technique for the computation in the box abstraction, a discrete abstraction technique for continuous-state systems.