Institutional Repository
| model checking: a coalgebraic approach | |
| Gao Jianhua; Jiang Ying | |
| 2011 | |
| Conference Name | 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011 |
| Source | Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011 |
| Pages | 235-238 |
| Conference Date | August 29, |
| Conference Place | Xi'an, Shaanxi, China |
| Indexed Type | EI |
| ISBN | 9780769545066 |
| Department | (1) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China; (2) Graduate University Chinese Academy of Sciences China |
| English Abstract | State explosion problem is the main obstacle of model checking. In this work, we address this problem from a co algebraic point of view. We establish an effective method to prove uniformly the existence of the smallest Kripke structure with respect to bisimilarity, which describes all behaviors of the Kripke structures with no redundancy. We show this smallest Kripke structure generates a minimal one for each given finite Kripke structure and some kind of infinite ones. This method is based on the existence of the final co algebra of a suitable endofunctor and can be generalized smoothly to other co algebraic structures. A naive implementation of this method is developed in Ocaml. © 2011 IEEE.; State explosion problem is the main obstacle of model checking. In this work, we address this problem from a co algebraic point of view. We establish an effective method to prove uniformly the existence of the smallest Kripke structure with respect to bisimilarity, which describes all behaviors of the Kripke structures with no redundancy. We show this smallest Kripke structure generates a minimal one for each given finite Kripke structure and some kind of infinite ones. This method is based on the existence of the final co algebra of a suitable endofunctor and can be generalized smoothly to other co algebraic structures. A naive implementation of this method is developed in Ocaml. © 2011 IEEE. |
| Keyword | Algebra Software Engineering |
| Sponsorship | IEEE CS; IFIP |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16220 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Gao Jianhua,Jiang Ying. model checking: a coalgebraic approach[C],2011:235-238. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment