UPPAAL SMC激励实例

Question

我想了解1中讨论的UPPAAL SMC示例。

下面是UPPAAL-SMC示例：

​

​

三个时间自动机应该可视化UPPAAL SMC中的概率分布。文中指出，在6,12，4,12和[0，+∞]时间间隔内，三种TA的末端位置都可以达到。我在UPPAAL中建模了A1 TA，由于更新X=0和边缘的保护x >= 2，所以不可能到达终端位置。时间间隔是如何详细计算的？

1

Answer 1

A1：由四个州( s1, s2, s3, s4 = END )组成。在s1中可以花费的时间较低，由守卫x >= 2限制，而上界则由标签x <= 4所限制。s2和s3也是如此。因此，A1的时间间隔是[2 + 2 + 2, 4 + 4 + 4] = [6, 12]。

A2：由两条路径s1, s2, s3, s4, s5 = END和s1, s6, s7, s5 = END组成。第一条路径与A1相同。第二条路径的时间间隔是[4, 8]。总的来说，A2的时间间隔是[min(6, 4), max(12, 8)] = [4, 12]。

A3：没有时间标签或保护，因此时间间隔是[0, +oo]，假设存在某个时间变量。