Rate Reduction for State-labelled Markov Chains with Upper Time-bounded CSL Requirements
Systems and Control
2016-08-03 v1 Logic in Computer Science
Performance
Abstract
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.
Keywords
Cite
@article{arxiv.1608.00658,
title = {Rate Reduction for State-labelled Markov Chains with Upper Time-bounded CSL Requirements},
author = {Bharath Siva Kumar Tati and Markus Siegle},
journal= {arXiv preprint arXiv:1608.00658},
year = {2016}
}
Comments
In Proceedings Cassting'16/SynCoP'16, arXiv:1608.00177