The verification of continuous-time Markov Chains (CTMC's) against continuous stochastic logic
(CSL), a stochastic branching time temporal logic, is considered. Among other logics
CSL is the logic which provides us with the specification of steady-state properties
and the specification of probabilistic timing properties of the form P<p(F U^I G), F and G are 

different state formulas, U is the until operator  known from the Linear Time Logic (LTL),
I a real time interval, < is a comparison operator, and p is a probability.
The verification of such properties can be done with some suitable algorithms.
In this Master's Thesis, presented algorithms for model-checking CTMC's with CSL are
also made possible with C++ programming using Möbius environment.
The Möbius tool is an environment for supporting multiple modeling formalisms.
The goal of this is to developing a robust, easy to use, reliable and efficient
CSL model checker for stochastic models as specified in Möbius.