Time−Bounded Model Checking of Infinite−State Continuous−Time Markov Chains
The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties, and makes them analyzable by model checking. In this...
Главные авторы: | Hahn, E, Hermanns, H, Wachter, B, Zhang, L |
---|---|
Формат: | Journal article |
Опубликовано: |
2009
|
Схожие документы
-
INFAMY: An Infinite−State Markov Model Checker
по: Hahn, E, и др.
Опубликовано: (2009) -
Importance Sampling for Model Checking of Continuous Time Markov Chains
по: Barbot, B, и др.
Опубликовано: (2015) -
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
по: Taolue Chen, и др.
Опубликовано: (2011-03-01) -
Two Approaches to the Construction of Perturbation Bounds for Continuous-Time Markov Chains
по: Alexander Zeifman, и др.
Опубликовано: (2020-02-01) -
PASS: Abstraction Refinement for Infinite Probabilistic Models
по: Hahn, E, и др.
Опубликовано: (2010)