设计混合系统离散端的功能方法

Question

我正在用 Haskell 开发混合系统的控制器。

FRP 库（现在我正在使用netwire，但有几个很好的库，并且对未来的库进行了很多有趣的研究）为问题的连续时间方面提供了一个很好的解决方案。用信号名称、尺寸、首选单位等对它们进行扩充，可以得到一个具有模块化、自我描述性并且有一条直截了当的途径来确保正确性的系统。

我正在寻找为离散时间方面提供类似属性的信息、民间传说或论文。从某种意义上说，问题要容易得多，状态机经过充分研究且简单。在其他意义上它更难，我将简要解释一下。

正确性显然是最重要的，幸运的是它也很简单。

自我描述更成问题。您希望控制器不仅处于正确状态，而且能够告诉您它处于什么状态。以及它是如何到达那里的。以及它下一步可能去哪里。所以你可以给所有东西加上名字，它可以工作，但它与模块化有些冲突。您还希望能够从更简单的行为构建复杂的离散时间行为。但是当你问系统它处于什么状态时，一般来说，高层次的答案比低层次的答案更有趣（或者至少一样有趣）。你如何干净地得到这个？我尝试了一些幼稚的方法，并以几种不同的方式将自己包裹在意大利面条中，但似乎必须有优雅的解决方案？

我在自我描述方面遇到的另一个问题是我想要一个自我描述条件的列表（通常比较：已经 10 秒了吗？我是否在下一个航路点的 3 英尺范围内？有电池电量低于 15%？等）正在被监控，这可能会触发下一个状态转换。这里有一些棘手的问题是什么是理想的语义，因为似乎其中一些事件“从下到上”处理得更好（例如，您正在执行的任何低级别步骤的预期终止条件）和一些“从顶部down”（例如设备故障检测、地理围栏……）。即使您放松自我描述的目标，这也可能导致自己的意大利面。

除了诊断之外，此处准确的自我描述信息对于抽象解释也非常有用，通过猜测哪些事件可能在何时发生，将系统的状态投射到未来。许多事件条件会导致自己做出相当简单的猜测（例如，使用良好的速度、燃料消耗率、计时器）。其他更复杂，但可能仍然值得为某些应用程序开发预测（例如，来自运营商的预期订单、天气预报、移动感兴趣物体的预计轨迹）。如果能找到一种设计，不仅可以用名称注释条件，还可以用这类东西的函数来注释条件。

有没有人愿意分享这方面的经验？

Answer 1

好的，所以我会说你的问题的“真正”答案是你所要求的一些东西是开放的研究领域 --- 特别是我认为你想要的一些自我描述的功能可能是必要的某种程度的“意大利面”仅仅是因为你试图解决的问题本质上是复杂的。

话虽如此，您对模块化的关注正是正确的方法。我想说，看看Keymaera，因为我相信它具有您正在寻找的功能，尽管它是在 Java 中。我还建议您查看 Keymaera 网站上的出版物页面，因为这应该可以为您提供对一般问题的宝贵见解。

如果您不喜欢 Keymaera 的方法，您也可以考虑使用 Timed Automata，这是另一个建模方向，应该足以描述您的问题。