Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Application of Concurrency to System Design
Article type: Research Article
Authors: Hahn, E. Moritz | Hermanns, Holger | Wachter, Björn | Zhang, Lijun
Affiliations: Department of Computer Science Saarland University Saarbrücken, Germany. E-mail: {zhang,emh,hermanns,bwachter}@cs.uni-sb.de
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 that captures such performance and dependability properties, and makes them analyzable by model checking. In this paper, we focus on time-bounded probabilistic properties of infinite-state CTMCs, expressible in a subset of continuous stochastic logic (CSL). This comprises important dependability measures, such as time-bounded probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective.
Keywords: Markov chains, model checking, truncation, uniformization
DOI: 10.3233/FI-2009-145
Journal: Fundamenta Informaticae, vol. 95, no. 1, pp. 129-155, 2009
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl