Towards compositional CSL model checking

摘要: The Continuous Stochastic Logic (CSL) is a powerful means to state properties which refer Time Markov Chains (CTMCs). verification of such on model can be achieved through suitable algorithm. In this doctoral thesis, the CSL logic has been considered and two major aspects have addressed: analysis its expressiveness study methods for decomposed formuale. Concerning expressiveness, we observed that syntax lead formulae with trivial semantics. As consequence idea well-formed formula introduced. Furthermore, simpler equivalent referring ergodic CMTCs defined as well brand new event-bounded Until operator. With respect compositionality, referred our specific type CTMCs, namely bidimensional Boucherie framework. A number basic concerning framework demonstrated and, relying this, compositional semantics subset derived. obtained by disallowing nesting probabilistic path-formulae, something whose impact ability useful low.