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