Personal tools
You are here: Home Events Abstract Archives 2004 Towards Compositional CSL Model-checking

Towards Compositional CSL Model-checking

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

Document Actions