| 一种基于时间自动机的时钟等价性优化方法 |
| |
| 引用本文： | 钱俊彦,赵岭忠,古天龙.一种基于时间自动机的时钟等价性优化方法[J].计算机工程,2005,31(18):71-73. |
| |
| 作者姓名： | 钱俊彦 赵岭忠 古天龙 |
| |
| 作者单位： | 桂林电子工业学院计算机系,桂林,541004;桂林电子工业学院计算机系,桂林,541004;桂林电子工业学院计算机系,桂林,541004 |
| |
| 基金项目： | “十五”国防预研基金资助项目;广西自然科学基金资助项目（0141046）致谢：刘园、史亮、张迎周同学为本文提出宝贵意见,在此表示衷心感谢. |
| |
| 摘 要： | 提出了一种优化模型检验时间自动机的时钟等价规则,通过优化的时钟等价规则,使时间自动机等价后的域自动机状态数尽可能少,并在此基础上定义了适合于优化时钟等价规则的域自动机.优化时钟等价规则,在一定程度上有效地解决了状态空间爆炸问题.
|
| 关 键 词： | 模型检验 时间自动机 域自动机 时态逻辑 |
| 文章编号： | 1000-3428（2005）18-0071-03 |
| 收稿时间： | 08 15 2004 12:00AM |
| 修稿时间： | 2004-08-15 |
Optimization Clock Equivalence for Timed Automaton |
| |
| QIAN Junyan,ZHAO Lingzhong,Gu Tianlong.Optimization Clock Equivalence for Timed Automaton[J].Computer Engineering,2005,31(18):71-73. |
| |
| Authors: | QIAN Junyan ZHAO Lingzhong Gu Tianlong |
| |
| Affiliation: | Computer Department, Guilin University of Electronic Technology, Guilin 541004 |
| |
| 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. |
| |
| Keywords: | Model checking Timed automaton Region automaton Temporal logic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
