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...
Main Authors: | Hahn, E, Hermanns, H, Wachter, B, Zhang, L |
---|---|
Formato: | Journal article |
Publicado: |
2009
|
Títulos similares
-
INFAMY: An Infinite−State Markov Model Checker
por: Hahn, E, et al.
Publicado: (2009) -
Importance Sampling for Model Checking of Continuous Time Markov Chains
por: Barbot, B, et al.
Publicado: (2015) -
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
por: Taolue Chen, et al.
Publicado: (2011-03-01) -
Two Approaches to the Construction of Perturbation Bounds for Continuous-Time Markov Chains
por: Alexander Zeifman, et al.
Publicado: (2020-02-01) -
PASS: Abstraction Refinement for Infinite Probabilistic Models
por: Hahn, E, et al.
Publicado: (2010)