Institutional Repository
| probabilistic model checking on propositional projection temporal logic | |
| Yang Xiaoxiao | |
| 2011 | |
| Conference Name | International MultiConference of Engineers and Computer Scientists 2011, IMECS 2011 |
| Source | IMECS 2011 - International MultiConference of Engineers and Computer Scientists 2011 |
| Pages | 242-248 |
| Conference Date | March 16, |
| Conference Place | Kowloon, Hong kong |
| Indexed Type | EI |
| Publish Place | Hong Kong |
| ISBN | 9789881821034 |
| Department | (1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China |
| English Abstract | Prepositional Projection Temporal Logic (PPTL) is a useful formalism for reasoning about period of time in hardware and software systems and can handle both sequential and parallel compositions. In this paper, based on discrete time Markov chains, we investigate the probabilistic model checking approach for PPTL towards verifying arbitrary linear-time properties. We first define a normal form graph, denoted by NFGinf, to capture the infinite paths of PPTL formulas. Then we present an algorithm to generate the NFG inf. Since discrete-time Markov chains are the deterministic probabilistic models, we further give an algorithm to determinize and minimize the nondeterministic NFGinf following the Safra's construction. |
| Keyword | Algorithms Computer Hardware Computer Science Engineers Markov Processes Probabilistic Logics Temporal Logic |
| Sponsorship | IAENG Society of Artificial Intelligence; IAENG Society of Bioinformatics; IAENG Society of Computer Science; IAENG Society of Data Mining; IAENG Society of Electrical Engineering |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/14247 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | Yang Xiaoxiao. probabilistic model checking on propositional projection temporal logic[C]. Hong Kong,2011:242-248. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| probabilistic model （682KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment