Institutional Repository
| model checking conditional csl for continuous-time markov chains | |
| Gao Yang; Xu Ming; Zhan Naijun; Zhang Lijun | |
| 2013 | |
| Source | Information Processing Letters
 |
| ISSN | 0020-0190 |
| Volume | 113Issue:1-2Pages:44-50 |
| English Abstract | In this paper, we consider the model-checking problem of continuous-time Markov chains (CTMCs) with respect to conditional logic. To the end, we extend Continuous Stochastic Logic introduced in Aziz et al. (2000) [1] to Conditional Continuous Stochastic Logic (CCSL) by introducing a conditional probabilistic operator. CCSL allows us to express a richer class of properties for CTMCs. Based on a parameterized product obtained from the CTMC and an automaton extracted from a given CCSL formula, we propose an approximate model checking algorithm and analyse its complexity. Crown Copyright © 2012 Elsevier B.V. All rights reserved.; In this paper, we consider the model-checking problem of continuous-time Markov chains (CTMCs) with respect to conditional logic. To the end, we extend Continuous Stochastic Logic introduced in Aziz et al. (2000) [1] to Conditional Continuous Stochastic Logic (CCSL) by introducing a conditional probabilistic operator. CCSL allows us to express a richer class of properties for CTMCs. Based on a parameterized product obtained from the CTMC and an automaton extracted from a given CCSL formula, we propose an approximate model checking algorithm and analyse its complexity. Crown Copyright © 2012 Elsevier B.V. All rights reserved. |
| Indexed Type | EI |
| Keyword | Automata Theory Formal Methods Stochastic Systems |
| Department | (1) State Key Lab. of Comp. Sci. Institute of Software Chinese Academy of Sciences China; (2) Department of Computer Science and Technology East China Normal University China; (3) Technical University of Denmark DTU Informatics Denmark |
| Language | 英语 |
| WOS ID | WOS:000312175200009 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15206 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Gao Yang,Xu Ming,Zhan Naijun,et al. model checking conditional csl for continuous-time markov chains[J]. Information Processing Letters,2013,113(1-2):44-50. |
| APA | Gao Yang,Xu Ming,Zhan Naijun,&Zhang Lijun.(2013).model checking conditional csl for continuous-time markov chains.Information Processing Letters,113(1-2),44-50. |
| MLA | Gao Yang,et al."model checking conditional csl for continuous-time markov chains".Information Processing Letters 113.1-2(2013):44-50. |
| 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