| LTL公式到自动机的转换 |
| |
| 引用本文： | 郭建,边明明,韩俊岗.LTL公式到自动机的转换[J].计算机科学,2008,35(7):241-243. |
| |
| 作者姓名： | 郭建 边明明 韩俊岗 |
| |
| 作者单位： | 1. 西安电子科技大学微电子学院,西安710071
2. 西安邮电学院计算机系,西安710061 |
| |
| 基金项目： | 国家自然科学基金，陕西省教育厅资助项目 |
| |
| 摘 要： | 在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法.该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机.此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动机的转换.
|
| 关 键 词： | 模型检验 Buchi自动机 选择Buchi自动机 LTL公式 |
Translation from LTL Formula into Automata |
| |
| GUO Jian,BIAN Ming-ming,HAN Jun-gang.Translation from LTL Formula into Automata[J].Computer Science,2008,35(7):241-243. |
| |
| Authors: | GUO Jian BIAN Ming-ming HAN Jun-gang |
| |
| Affiliation: | GUO Jian1 BIAN Ming-ming 2 HAN Jun-gang 2 (Microelectronics Institute,Xi'dian University,Xi'an 710071,China)1 (Computer Department,Xi'an Institute Post , Telecommunications,Xi'an 710061,China)2 |
| |
| Abstract: | On the basis of introduction to LTL formula and theory of automata,we present a algorithm which can transfer LTL formulae into Buchi automata.In this algorithm,the LTL formula is simplified first,then transferred into an alternating Buchi automaton,before further transferred and then transforms it into a Buchi automaton.Compared to others,this algorithm has certain extensibility,so we can translate PSL into automata. |
| |
| Keywords: | Model checking Buchi automata Alternating buchi automata Linear temporal logic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
