Institutional Repository
| Bisimulations and logical characterizations on continuous-time markov decision processes | |
| Song, Lei (1); Zhang, Lijun (2); Godskesen, Jens Chr. (3) | |
| 2014 | |
| Conference Name | 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014 |
| Pages | 98-117 |
| Conference Date | January 20, 2014 - January 21, 2014 |
| Conference Place | San Diego, CA, United states |
| Indexed Type | EI |
| Publish Place | Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany |
| ISSN | 3029743 |
| ISBN | 9783642540127 |
| Department | (1) Max-Planck-Institut für Informatik, Saarland University, Saarbrücken, Germany; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China; (3) Programming, Logic, and Semantics Group, IT University of Copenhagen, Denmark |
| English Abstract | In this paper we study strong and weak bisimulation equivalences for continuous-time Markov decision processes (CTMDPs) and the logical characterizations of these relations with respect to the continuous-time stochastic logic (CSL). For strong bisimulation, it is well known that it is strictly finer than the CSL equivalence. In this paper we propose strong and weak bisimulations for CTMDPs and show that for a subclass of CTMDPs, strong and weak bisimulations are both sound and complete with respect to the equivalences induced by CSL and the sub-logic of CSL without next operator respectively. We then consider a standard extension of CSL, and show that it and its sub-logic without X can be fully characterized by strong and weak bisimulations respectively over arbitrary CTMDPs. © 2014 Springer-Verlag Berlin Heidelberg.; In this paper we study strong and weak bisimulation equivalences for continuous-time Markov decision processes (CTMDPs) and the logical characterizations of these relations with respect to the continuous-time stochastic logic (CSL). For strong bisimulation, it is well known that it is strictly finer than the CSL equivalence. In this paper we propose strong and weak bisimulations for CTMDPs and show that for a subclass of CTMDPs, strong and weak bisimulations are both sound and complete with respect to the equivalences induced by CSL and the sub-logic of CSL without next operator respectively. We then consider a standard extension of CSL, and show that it and its sub-logic without X can be fully characterized by strong and weak bisimulations respectively over arbitrary CTMDPs. © 2014 Springer-Verlag Berlin Heidelberg. |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16606 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Song, Lei ,Zhang, Lijun ,Godskesen, Jens Chr. . Bisimulations and logical characterizations on continuous-time markov decision processes[C]. Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany,2014:98-117. |
| 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