Bisimulation and logical preservation for continuous-time Markov decision processes

被引：0
|
作者：
Neuhaeusser, Martin R. [1 ,2 ]
Katoen, Joost-Pieter [1 ,2 ]
机构：
[1] Univ Aachen, Rhein Westfal TH Aachen, Software Modeling & Verificat Grp, Aachen, Germany
[2] Univ Twente, Formal Methods & Tools Grp, NL-7500 AE Enschede, Netherlands
来源：
CONCUR 2007 - CONCURRENCY THEORY, PROCEEDINGS | 2007年 / 4703卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL. To that end, we interpret the semantics of CSL-a stochastic variant of CTL for continuous-time Markov chains-on CTMDPs and show its measure-theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.
引用
收藏
页码：412 / +
页数：4
相关论文
共 50 条
12345