The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism, where performance and dependability properties are analyzable by model checking. We present INFAMY, a model checker for arbitrarily structured infinite-state CTMCs. It checks probabilistic timing properties expressible in continuous stochastic logic (CSL). Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and impossible if the model is infinite. INFAMY only explores the model up to a finite depth, with the depth bound being computed on-the-fly. The computation of depth bounds is configurable to adapt to the characteristics of different classes of models. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Hahn, E. M., Hermanns, H., Wachter, B., & Zhang, L. (2009). INFAMY: An infinite-state markov model checker. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5643 LNCS, pp. 641–647). https://doi.org/10.1007/978-3-642-02658-4_49
Mendeley helps you to discover research relevant for your work.