使用 z3 python API 编码线性混合自动机答案

【问题标题】：Encoding linear hybrid automata using z3 python API使用 z3 python API 编码线性混合自动机
【发布时间】：2012-08-05 13:31:09
【问题描述】：

我正在尝试将线性混合自动机编码为一阶公式的结合，如下所示：

s.add(Or(Or(And(off,Not(on),Not(S1),Not(S2),(10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)<=(10*x)-(t2-t1),x_next>=18,(t2-t1)>0,Implies(),
And(Not(off),on,Not(S2),Not(S1),(10*x_next)>=(t2-t1)+(10*x),(5*x_next)<=(5*x)+(t2-t1),x_next<=22,(t2-t1)>0)),    
Or(And(x<19,(t2-t1)==0,S1,Not(off),Not(on),Not(S2),(x-x_next)==0),
And(x>21,(t2-t1)==0,Not(on),Not(off),S2,Not(S1),(x-x_next)==0))))

问题是需要采用跳转条件（例如，如果 x

【问题讨论】：

跳转条件是什么意思？你能提供更多细节吗？
混合自动机由不同的模式组成。每种模式都必须满足一定的线性算术约束。但是如果特定模式下状态变量的值达到某个值（例如 x
在这种情况下只有模式（关闭，打开）。如果 (x
两种模式（开、关）。 HA 以关闭模式启动。

标签： python python-2.7 z3

【解决方案1】：

寻找或构建可以编码的工具可能很有用来自更高级别描述的 HA 公式。他们可以帮助调试一些细节。比如你说有“开”和“关”两种模式。这些似乎被编码为命题变量。通常使用程序计数器来编码自动机的状态，因此例如会有一个程序计数器“状态”，其值可以是“开”或“关”。您可以在 Z3 中使用标量来编码状态变量的可能值，或者您可以使用整数、位向量或在本例中为布尔标志。然后是编码转换关系的问题。您通常需要在不被转换改变的变量上编码帧条件。

【讨论】：

确实这两种模式都被编码为提议变量。
让我再澄清一点。实际上，每种模式都有两组线性算术约束（它们可以表示为一阶公式的析取）。我面临的真正问题是如何在这两组（或两种模式）的约束之间进行切换。切换必须是最终公式的一个组成部分。
s.add(off,Not(on),(10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)=18,(t2-t1)>0 这就是我为“关闭”模式实现 consriants 的方式