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

TL;DR

This paper introduces algorithms for reducing controllable transition rates in state-labelled continuous-time Markov chains to ensure they meet specified upper time-bounded CSL requirements, simplifying model verification.

Contribution

It provides novel algorithms for rate reduction in CTMCs to satisfy CSL properties, addressing two probability bound cases with a natural state space partitioning.

Findings

Algorithms successfully reduce rates to meet CSL bounds

Approach simplifies model checking for time-bounded properties

Two case-specific solutions improve applicability

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.