Exploiting Implicit Representations in Timed Automaton Verification for Controller Synthesis
Exploiting Implicit Representations in Timed Automaton Verification for Controller Synthesis
复制标题
利用定时自动机验证中的隐式表示进行控制器合成
DOI：
10.1007/3-540-45873-5_19
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Michael J. S. Pelican
中科院分区：
文献类型：
--
作者：
R. Goldman;D. Musliner;Michael J. S. Pelican
自动控制器合成和验证技术有望彻底改变高可信度软件的构建。然而，基于显式状态机模型的方法受到极端状态空间爆炸和随之而来的规模限制的影响。在本文中，我们描述了如何在控制器综合中利用隐式的、基于过渡的时间自动机表示。CIRCA控制器综合模块（CSM）使用基于转换的隐式状态空间表示自动合成硬实时、响应式控制器。通过在搜索控制器和自定义模型检查验证器中利用这种隐式表示，CSM能够有效地为具有非常大状态空间的问题构建控制器。我们提供的实验结果显示，在探索的状态空间中，有实质性的加速和数量级的减少。这些结果可以应用于其他验证问题，无论是在控制器综合的背景下还是在更传统的验证问题中。
Automatic controller synthesis and verification techniques promise to revolutionize the construction of high-confidence software. However, approaches based on explicit state-machine models are subject to extreme state-space explosion and the accompanying scale limitations. In this paper, we describe how to exploit an implicit, transition-based, representation of timed automata in controller synthesis. The CIRCA Controller Synthesis Module (CSM) automatically synthesizes hard realtime, reactive controllers using a transition-based implicit representation of the state space. By exploiting this implicit representation in search for a controller and in a customized model checking verifier, the CSM is able to efficiently build controllers for problems with very large state spaces. We provide experimental results that show substantial speed-up and orders-of-magnitude reductions in the state spaces explored. These results can be applied to other verification problems, both in the context of controller synthesis and in more traditional verification problems.