CSLTA: an Expressive Logic for Continuous-Time Markov Chains
Donatelli, Susanna; Haddad, Serge; Sproston, Jeremy (2007), CSLTA: an Expressive Logic for Continuous-Time Markov Chains, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), IEEE Press, p. 31-40. http://doi.ieeecomputersociety.org/10.1109/QEST.2007.40
TypeCommunication / Conférence
Conference title4th International Conference on the Quantitative Evaluation of SysTems (QEST 2007)
Book titleFourth International Conference on the Quantitative Evaluation of Systems (QEST 2007)
MetadataShow full item record
Abstract (EN)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.
Subjects / KeywordsModel-checking; CSLTA; continuous-time Markov chains
Showing items related by title and author.
Reversible jump, birth-and-death and more general continuous time Markov chain Monte Carlo samplers Cappé, Olivier; Robert, Christian P.; Ryden, Tobias (2003) Article accepté pour publication ou publié