{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:23:50Z","timestamp":1777645430183,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2009,8]]},"abstract":"<jats:p>The design of complex concurrent systems often involves intricate\n\t\t\t performance and dependability considerations. Continuous-time Markov chains\n\t\t\t (CTMCs) are a widely used modeling formalism that captures such performance and\n\t\t\t dependability properties, and makes them analyzable by model checking. In this\n\t\t\t paper, we focus on time-bounded probabilistic properties of infinite-state\n\t\t\t CTMCs, expressible in a subset of continuous stochastic logic (CSL). This\n\t\t\t comprises important dependability measures, such as time-bounded probabilistic\n\t\t\t reachability, performability, survivability, and various availability measures\n\t\t\t like instantaneous, conditional instantaneous and interval availabilities.\n\t\t\t Conventional model checkers explore the given model exhaustively, which is\n\t\t\t often costly, due to state explosion, and sometimes impossible because the \n\t\t\t model is infinite. This paper presents a method that only explores the model up\n\t\t\t to a finite depth. The required depth is determined on the fly by an algorithm \n\t\t\t that is configurable in order to adapt to the characteristics of different\n\t\t\t classes of models. We provide experimental evidence showing that our method is\n\t\t\t effective.<\/jats:p>","DOI":"10.3233\/fi-2009-145","type":"journal-article","created":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T22:53:52Z","timestamp":1575327232000},"page":"129-155","source":"Crossref","is-referenced-by-count":9,"title":["Time-Bounded Model Checking of Infinite-State Continuous-Time\t\t\t Markov Chains"],"prefix":"10.1177","volume":"95","author":[{"given":"E. Moritz","family":"Hahn","sequence":"first","affiliation":[{"name":"Department of Computer Science Saarland University\r\t\t\t Saarbr\u00fccken, Germany. E-mail: {zhang,emh,hermanns,bwachter}@cs.uni-sb.de"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Department of Computer Science Saarland University\r\t\t\t Saarbr\u00fccken, Germany. E-mail: {zhang,emh,hermanns,bwachter}@cs.uni-sb.de"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bj\u00f6rn","family":"Wachter","sequence":"additional","affiliation":[{"name":"Department of Computer Science Saarland University\r\t\t\t Saarbr\u00fccken, Germany. E-mail: {zhang,emh,hermanns,bwachter}@cs.uni-sb.de"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Department of Computer Science Saarland University\r\t\t\t Saarbr\u00fccken, Germany. E-mail: {zhang,emh,hermanns,bwachter}@cs.uni-sb.de"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2009,1]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2009-145","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2009-145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:32:12Z","timestamp":1777444332000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-2009-145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["10.3233\/FI-2009-145"],"URL":"https:\/\/doi.org\/10.3233\/fi-2009-145","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]}}}