Model checking CSLTA: Using timed automata to specify properties of stochastic systems

 

Jeremy Sproston, Univ. Turino, Italy

 

 

Abstract:

Continuous-time Markov chains are widely used to study the performance
of computer and telecommunication systems. Stochastic temporal logics
such as Continuous Stochastic Logic (CSL) and their associated
model-checking algorithms allow a formal and unified approach to the
verification of functional and performance properties of stochastic
systems.

In this talk the stochastic logic CSLTA will be introduced. The logic
CSLTA extends CSL by allowing timing properties to be expressed using
a restricted class of timed automata. This extension allows us to
specify a larger class of timing properties than in CSL. In
particular, and in contrast to CSL, the logic CSLTA permits the
specification of properties referring to the probability of a finite
sequence of timed events, such as "with probability at least 0.75, a
message sent at time t by a system A will be received before time t+5
by system B, and the acknowledgment will be back at A before time
t+7". A model-checking algorithm for verifying CSLTA properties will
also be introduced.