Department of Computer Science
University of Liverpool
4pm 1 June 2004
Room 6301, JCMB, King's Buildings
The Continuous Stochastic Logic (CSL) is a powerful formalism for stating properties of systems modelled in terms of Continuous Time Markov Chains (CMTCs). CSL formulae are then checked against a CTMC's model, by means of appropriate model-checking algorithms. When the considered model can be decomposed in a number of sub-models, it is of interest to search for the existence of relevant semantic equivalences which could reduce the complexity of the model-checking problem.
In this presentation I will show that for a specific sub-class of (bi-dimensional) CTMCs (the bi-dimensional Boucherie product-processes) a decomposed semantics can be determined for a fragment of the original CSL syntax.