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 条

[1] Trace Relations and Logical Preservation for Continuous-Time Markov Decision Processes
Sharma, Arpit
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2017, 2017, 10580 : 192 - 209
[2] Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes
Song, Lei
Zhang, Lijun
Godskesen, Jens Chr.
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION: (VMCAI 2014), 2014, 8318 : 98 - 117
[3] Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes
Desharnais, J
Panangaden, P
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2003, 56 (1-2): : 99 - 115
[4] BISIMULATION METRICS FOR CONTINUOUS MARKOV DECISION PROCESSES
Ferns, Norm
Panangaden, Prakash
Precup, Doina
SIAM JOURNAL ON COMPUTING, 2011, 40 (06) : 1662 - 1714
[5] The Transformation Method for Continuous-Time Markov Decision Processes
Piunovskiy, Alexey
Zhang, Yi
JOURNAL OF OPTIMIZATION THEORY AND APPLICATIONS, 2012, 154 (02) : 691 - 712
[6] Impulsive control for continuous-time Markov decision processes
Université Bordeaux, IMB, INRIA Bordeaux Sud-Ouest, 200 Avenue de la Vieille Tour, Talence Cedex
33405, France
不详
L69 7ZL, United Kingdom
Adv Appl Probab, 1 (106-127):
[7] IMPULSIVE CONTROL FOR CONTINUOUS-TIME MARKOV DECISION PROCESSES
Dufour, Francois
Piunovskiy, Alexei B.
ADVANCES IN APPLIED PROBABILITY, 2015, 47 (01) : 106 - 127
[8] Continuous-Time Markov Decision Processes with Controlled Observations
Huang, Yunhan
Kavitha, Veeraruna
Zhu, Quanyan
2019 57TH ANNUAL ALLERTON CONFERENCE ON COMMUNICATION, CONTROL, AND COMPUTING (ALLERTON), 2019, : 32 - 39
[9] Continuous-Time Markov Decision Processes with Exponential Utility
Zhang, Yi
SIAM JOURNAL ON CONTROL AND OPTIMIZATION, 2017, 55 (04) : 2636 - 2660
[10] REALIZABLE STRATEGIES IN CONTINUOUS-TIME MARKOV DECISION PROCESSES
Piunovskiy, Alexey
SIAM JOURNAL ON CONTROL AND OPTIMIZATION, 2018, 56 (01) : 473 - 495

← 1 2 3 4 5 →