Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes

Neuhausser, M. and Katoen, J.P. (2007) Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. In: 18th International Conference on Concurrency Theory, CONCUR 2007, September 3-8, 2007, Lisbon, Portugal.

PDF
Restricted to UT campus only: Request a copy
257Kb

Abstract:	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.
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/64519
Official URL:	http://dx.doi.org/10.1007/978-3-540-74407-8_28
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 245846