INFAMY: An Infinite-State Markov Model Checker
In Computer Aided Verification, 21st International Conference (CAV)
, pages 641-647, Springer
, Lecture Notes in Computer Science 5643, 2009.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-02658-4_49
Abstract. 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.