乌帕尔时钟是如何进化的？我有两个位置 1 和 2 没有不变量。什么是时钟值？

Question

乌帕尔时钟是如何进化的？我有两个位置 1 和 2 没有不变性，一个时钟在转换到位置 1 时重置为零 (0)。在位置 1 和 2 之间的边缘，我怎么知道此时时钟的值？ （即位置2之前的两个位置之间的时钟值）。 时钟是否继续从位置 1 演化到位置 2 及以后，或者在新位置的入口处发生自动重置？

Answer 1

TLDR；答案。 如果自动机以

x==0

开始并在没有不变量的位置移动，那么自动机可能会延迟，比如

5

时间单位，然后用

x==5

移动到另一个位置，然后再次延迟，比如

3.141

时间单位，这将

x

移动到值

8.141

，依此类推。请注意，时钟

x

可以通过延迟和进行转换来达到任意 real 值（因此我的任意选择），这意味着需要分析所有这些可能性。 Uppaal 以约束的形式捕获所有这些可能的值（或者在没有不变量或守卫的情况下缺少它们，模拟器可能只显示

x==y

，因为所有时钟都是同步的）。

一些例子。假设我们有一个时间自动机，如下所述：

那么时钟

x

的值可以这样演化：

如果我们进行 1000 次模拟，那么

x

值的轨迹将如下所示：

如您所见，它慢慢地充满了平面的下半部分——一个区域。 UPPAAL 使用差分界矩阵来象征性地描述和分析这些区域。

上面的图是使用以下查询绘制的：

simulate [<=50] { x }
simulate [<=50; 1000] { x }

一些背景。 Uppaal 使用时钟变量实现时间自动机，时钟变量的值以

1

的速率（时间导数）连续变化。 因此，如果时钟重置为

0

并且自动机到达没有不变量的位置（也不紧急，也没有提交），那么时钟可以自由进化，因此可以具有从

0

到

infinity

的任意值。 Uppaal 使用打包到 差分界矩阵 (DBM) 中的约束（区间）以 符号形式 表示此类估值。如果自动机进行转换，那么 Uppaal 将立即分析所有满足约束的可能转换。例如，如果一个位置有一个不变的

x<=5

并且边缘有一个守卫

x>=2

，那么当

x

在

2

和

5

之间的任何地方时转换是可用的，因此Uppaal将采用带有约束的符号转换

 2<=x && x<=5

一次捕获所有这些可能的转换。这允许在有限的数据结构和有限的时间内分析无限多的转换。

一些新手容易混淆的常见情况 如果系统中有多个自动机，那么时间的流逝是全局分析的，即一个自动机中的不变量将对其他自动机中的其他时钟产生影响，因为所有时钟都通过全局时间同步.

时间自动机只允许守卫和不变量中的整数，原则上可以缩放以适应有理数的模型。 Uppaal 还用紧急、提交位置、选择语句、广播同步、整数变量、函数调用等扩展了时间自动机，这些在相同的时间自动机理论下仍然是可分析的，但使建模更具表现力和简洁。

您可以在 http://uppaal.org 的文档部分下的 Uppaal 教程中阅读更多内容： http://www.it.uu.se/research/group/darts/uppaal/documentation.shtml#tutorials