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

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...

Full description

Bibliographic Details
Main Authors: Bharath Siva Kumar Tati, Markus Siegle
Format: Article
Language:English
Published: Open Publishing Association 2016-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1608.00658v1