guest ::
TY - THES AU - Klink, Daniel TI - Three-valued abstraction for stochastic systems CY - München PB - Hut M1 - RWTH-CONV-113970 SN - 978-3-86853-408-5 SP - VIII, 223 S. : graph. Darst. PY - 2010 N1 - Zsfassung in engl. und dt. Sprache N1 - Aachen, Techn. Hochsch., Diss., 2010 AB - Formal methods are a mathematical tool for modeling and verifying qualitative and quantitative aspects of systems of a wide variety of types. A most acknowledged technique in this context is the model checking approach that allows for an automated verification of system models with respect to sets of formal requirements. The underlying analysis techniques systematically and exhaustively explore all configurations of a system, resulting in a high memory consumption. To deal with this bottleneck, several solutions have been proposed, ranging from the use of efficient data structures to a number of reduction techniques. This thesis is concerned with abstraction, that is, with the reduction of available information in the system’s model, and the question of what properties are preserved when applying abstraction. We are focusing on the more intricate quantitative properties of probabilistic timed systems that can be expressed in PCTL and CSL, probabilistic variants of the computation tree logic (CTL). The models under consideration are discrete-time and continuous-time Markov chains (DTMCs, CTMCs) as well as interactive Markov chains (IMCs) that extend CTMCs with functional behavior and provide facilities for compositional modeling. Markov chains are the underlying low-level models for many modeling formalisms that are used, amongst others, in the area of reliability, dependability and performance analysis as well as in systems biology. In this thesis, abstraction is implemented by merging states of a system’s model; when states with different behavior are to be merged, nondeterminism is added to the corresponding abstract state to capture the uncertainty on what concrete state is occupied when looking at the abstract picture. Due to this newly introduced nondeterminism, we obtain abstractions that may contain more (but no less) possible behavior compared to the given concrete system; hence, when analyzing the abstraction, we obtain safe over- and underapproximations of the results for the concrete model. This allows us to derive conclusions from the abstraction where the concrete model is too large to be analyzed or even of infinite size. However, if too much information is discarded – resulting in a coarse abstraction – the analysis results may be inconclusive. In order to handle such inconclusive (partial) results, we develop a model checking framework based on three-valued logics with an additional truth value don’t know. When generalizing abstraction for CTMCs to the compositional framework of IMCs, we propose to perform abstraction at the component level instead of building a monolithic model of the system first. This approach allows for significant reductions of the peak memory requirements. We investigate the formal relation between the resulting abstract compositional model and the given concrete one. Further, we show that the abstraction of several distinct components can be used to introduce symmetries that are not present in the concrete model but facilitate enormous savings in the compositional abstraction. Besides the theoretical underpinnings of abstraction and model checking for stochastic systems, we also provide efficient algorithms for the analysis of abstract models and we show empirically that abstraction complements long-standing analysis techniques in queueing theory. Further, we present an extension of the abstraction framework that allows for the efficient analysis of a well-known, hard-to-solve case study from systems biology: enzyme catalyzed substrate conversion. KW - Abstraktion (SWD) KW - Model Checking (SWD) KW - Markov-Kette mit stetiger Zeit (SWD) KW - Verteiltes System (SWD) KW - Intervallwahrscheinlichkeit (SWD) KW - Prioritätswarteschlange (SWD) KW - Systembiologie (SWD) KW - Erlang-Verteilung (SWD) LB - PUB:(DE-HGF)11 UR - https://publications.rwth-aachen.de/record/51706 ER -