摘要： 提出了一种优化模型检验时间自动机的时钟等价规则,通过优化的时钟等价规则,使时间自动机等价后的域自动机状态数尽可能少,并在此基础上定义了适合于优化时钟等价规则的域自动机。优化时钟等价规则,在一定程度上有效地解决了状态空间爆炸问题。

关键词: 模型检验, 时间自动机, 域自动机, 时态逻辑

Abstract: An optimization definition of clock equivalence,the key to model checking real-time,is described for model checking timed automaton.Based on its equivalent finite-state clock valuation,region automaton that the finite-state model resulted from timed automaton is redefined.By new equivalent formulae,the size of the states is given as few as possible after equivalence.The results suggest that reduction of the state space is efficient in new clock equivalence.

中图分类号: 

• TP301