硕士开题报告-Model Checking Continuous-Time.pdf

Model Checking Continuous-Time
Markov Chains Against Conditional CSL
Gao Yang
Joint Work with Ming Xu,Naijun Zhan,Lijun Zhang
OUTLINE
• Introduction
• Related Work
• Model SL for CTMC
• Experiment
• Future Work
OUTLINE
• Introduction
• Related Work
• Model SL for CTMC
• Experiment
• Future Work
Introduction
Model Checking .
Probabilistic Model Checking
Introduction
Model Checking .
Probabilistic Model Checking

CTMC
CSL
Related Work
References
• Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-
checking continous-time Markov chains. ACM Trans.
Comput. Log. 1(1) (2000) 162–170
• Zhang, L., Jansen, ., Nielson, F., Hermanns, H.:
Automata-based CSL model checking. In: ICALP, Part II.
LNCS 6756, Springer (2011) 271–282
• Zhang, L., Jansen, ., Nielson, F., Hermanns, H.:
Efficient CSL model checking using stratification. Logical
Methods puter Science 8(2:17) (2012) 1–18
• Yang Gao, Ming Xu, Naijun Zhan, Lijun Zhang:
Model Checking Conditional CSL for Continuous-Time
Markov Chains.
Related Work [Aziz2000]
• Aziz et al. proposed Continuous-time Stochastic
Logic (CSL)
𝛷≔𝑎¬𝛷𝛷∧𝛷| 𝑃⋈(𝜑)
𝜑≔𝛷1𝑈𝐼1𝛷2𝑈𝐼2 …𝛷𝑛
• Theorem. CSL model checking is decidable.
Model Checking CSL [Zhang, L. ICALP2011]
• Exit Rate: 𝐸𝑠1 = 2
• Absorbing State: 𝑠3
Model Checking CSL [Zhang, L. ICALP2011]
Transient Probability:
• The probability that some
transition from 𝒔𝟏 will be
triggered within time t is
𝟏−𝒆−𝟐𝒕.
• The probability to take the
𝑹(𝒔𝟏,𝒔𝟐)
transition to 𝒔𝟐 is ∙
𝑬(𝒔𝟏)
−𝟐𝒕
𝟏−𝒆. −𝟐 2
• Starting with distribution 𝜶, the −𝟐 1 1
𝑄= 1 −𝟐 1
transition probability vector at 0
time 𝒕 is give by: 𝝅𝜶, 𝒕= 2 −𝟐
𝝅(𝜶, 𝟎)𝒆𝑸𝒕.