| Speaker | Jeremy Sproston, University Turin, Italy |
| Title | Model checking CSLTA: Using timed automata to specify properties of stochastic systems |
| Where | 5056 |
| When | 19.03.2008, 10:00 |
| 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. |
| Slides | download |
Event calendar
- Subscribe to the ics feed.
Upcoming Events
- No Events