Bisimulation Relations Between Automata, Stochastic Differential Equations and Petri Nets
Bisimulation Relations Between Automata, Stochastic Differential Equations and Petri Nets
复制标题
自动机、随机微分方程和Petri网之间的互模拟关系
DOI：
10.4204/eptcs.20.1
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
H. Blom
中科院分区：
文献类型：
--
作者：
M. Everdij;H. Blom
如果两个形式随机模型的解作为随机过程是概率等价的，则称它们是双相似的。两种随机模型形式之间的双相似性意味着一种随机模型形式的优点可以被另一种随机模型形式所利用。本文的目的是解释随机混杂自动机、混杂空间上的随机微分方程和随机混杂Petri网之间的双相似关系。这些双相似关系使得联合收割机将自动机的形式验证能力与随机微分方程的分析能力和Petri网的组合规范能力结合起来成为可能。的关系和它们的综合优势，说明了空中交通的例子。
Two formal stochastic models are said to be bisimilar if their solutions as a stochastic process are probabilistically equivalent. Bisimilarity between two stochastic model formalisms means that the strengths of one stochastic model formalism can be used by the other stochastic model formalism. The aim of this paper is to explain bisimilarity relations between stochastic hybrid automata, stochastic differential equations on hybrid space and stochastic hybrid Petri nets. These bisimilarity relations make it possible to combine the formal verification power of automata with the analysis power of stochastic differential equations and the compositional specification power of Petri nets. The relations and their combined strengths are illustrated for an air traffic example.