Institutional Repository
| specification in pdl with recursion | |
| Liu Xinxin; Xue Bingtian | |
| 2012 | |
| Conference Name | 4th NASA Formal Methods Symposium, NFM 2012 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 181-194 |
| Conference Date | April 3, 2012 - April 5, 2012 |
| Conference Place | Norfolk, VA, United states |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642288906 |
| Department | (1) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences P.O. Box 8718 100190 Beijing China; (2) Graduate School Chinese Academy of Sciences P.O. Box 8718 100190 Beijing China |
| English Abstract | By extending regular Propositional Dynamic Logic (PDL) with simple recursive propositions, we obtain a language which has enough expressiveness to allow interesting applications while still enjoying a relatively simple decision procedure. More specifically, it is strictly more expressive than the regular PDL and not more expressive than the single alternation fragment of the modal μ-calculus. We present a decision procedure for satisfiability of a large class of so called simple formulas. The decision procedure has a time complexity which is polynomial in the size of the programs and exponential in the number of the sub-formulas. We show a way to solve process equations of weak bisimulation as an application. © 2012 Springer-Verlag.; By extending regular Propositional Dynamic Logic (PDL) with simple recursive propositions, we obtain a language which has enough expressiveness to allow interesting applications while still enjoying a relatively simple decision procedure. More specifically, it is strictly more expressive than the regular PDL and not more expressive than the single alternation fragment of the modal μ-calculus. We present a decision procedure for satisfiability of a large class of so called simple formulas. The decision procedure has a time complexity which is polynomial in the size of the programs and exponential in the number of the sub-formulas. We show a way to solve process equations of weak bisimulation as an application. © 2012 Springer-Verlag. |
| Keyword | Calculations Nasa Specifications |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15703 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Liu Xinxin,Xue Bingtian. specification in pdl with recursion[C],2012:181-194. |
| 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