loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007)
CSL^TA: an Expressive Logic for Continuous-Time Markov Chains
Edinburgh, Scotland, UK
September 17-September 19
ISBN: 0-7695-2883-X
Susanna Donatelli, Universita di Torino, Italy
Serge Haddad, Universite Paris-Dauphine, France
Jeremy Sproston, Universita di Torino, Italy
The stochastic temporal logic CSL can be used to describe formally properties of continuous-time Markov chains, and has been extended with expressions over states and actions to obtain the logic asCSL. However, properties referring to the probability of a finite sequence of timed events (such as "with probability at least 0.75, the system will be in state set A at time 5, then in state set B at time 7, then in state set C at time 20") cannot be expressed in either CSL or asCSL. With the aim of increasing the expressive power of temporal logics for continuous-time Markov chains, we introduce the logic CSL^TA and its model-checking algorithm. CSL^TA extends CSL and asCSL by allowing the specification of timed properties through a deterministic one-clock timed automata.
Citation:
Susanna Donatelli, Serge Haddad, Jeremy Sproston, "CSL^TA: an Expressive Logic for Continuous-Time Markov Chains," qest, pp.31-40, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.