• xmlui.mirage2.page-structure.header.title
    • français
    • English
  • Help
  • Login
  • Language 
    • Français
    • English
View Item 
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Browse

BIRDResearch centres & CollectionsBy Issue DateAuthorsTitlesTypeThis CollectionBy Issue DateAuthorsTitlesType

My Account

LoginRegister

Statistics

Most Popular ItemsStatistics by CountryMost Popular Authors
Thumbnail

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

View/Open
QEST2007.PDF (4.031Mb)
Type
Communication / Conférence
Date
2007
Conference title
4th International Conference on the Quantitative Evaluation of SysTems (QEST 2007)
Conference date
2007-09
Conference city
Edinburgh
Conference country
Royaume-Uni
Book title
Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007)
Publisher
IEEE Press
ISBN
0-7695-2883-X
Pages
31-40
Publication identifier
http://doi.ieeecomputersociety.org/10.1109/QEST.2007.40
Metadata
Show full item record
Author(s)
Donatelli, Susanna
Haddad, Serge
Sproston, Jeremy
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 / Keywords
Model-checking; CSLTA; continuous-time Markov chains

Related items

Showing items related by title and author.

  • Thumbnail
    Structured Characterization of the Markov Chain of Phase-Type SPN 
    Donatelli, Susanna; Haddad, Serge; Moreaux, Patrice (1998) Communication / Conférence
  • Thumbnail
    Continuous Petri Nets: Expressive Power and Decidability Issues 
    Recalde, Laura; Haddad, Serge; Silva, Manuel (2007) Communication / Conférence
  • Thumbnail
    Robust No Arbitrage Condition for Continuous-Time Models with Transaction Costs 
    Lépinette, Emmanuel (2011) Communication / Conférence
  • Thumbnail
    Limit theorems for some continuous-time random walks 
    Jara, Milton; Komorowski, Tomasz (2011) Article accepté pour publication ou publié
  • Thumbnail
    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é
Dauphine PSL Bibliothèque logo
Place du Maréchal de Lattre de Tassigny 75775 Paris Cedex 16
Phone: 01 44 05 40 94
Contact
Dauphine PSL logoEQUIS logoCreative Commons logo