Rate Reduction for State-labelled Markov Chains with Upper Time-bounded CSL Requirements

Bharath Siva Kumar Tati
Markus Siegle
(UniBw)

This paper presents algorithms for identifying and reducing a dedicated set of controllable transition rates of a state-labelled continuous-time Markov chain model. The purpose of the reduction is to make states to satisfy a given requirement, specified as a CSL upper time-bounded Until formula. We distinguish two different cases, depending on the type of probability bound. A natural partitioning of the state space allows us to develop possible solutions, leading to simple algorithms for both cases.

In Thomas Brihaye, Benoît Delahaye, Loïg Jezequel, Nicolas Markey and Jiří Srba: Proceedings Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd International Workshop on Synthesis of Complex Parameters (Cassting'16/SynCoP'16), Eindhoven, The Netherlands, April 2-3, 2016, Electronic Proceedings in Theoretical Computer Science 220, pp. 77–89.
Published: 31st July 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.220.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org