h1

000051706 001__ 51706
000051706 005__ 20220422215714.0
000051706 020__ $$a978-3-86853-408-5
000051706 0247_ $$2Laufende Nummer$$a30208
000051706 0247_ $$2URN$$aurn:nbn:de:hbz:82-opus-32124
000051706 0247_ $$2HSB$$ahsb910019682
000051706 0247_ $$2OPUS$$a3212
000051706 037__ $$aRWTH-CONV-113970
000051706 041__ $$aEnglish
000051706 082__ $$a004
000051706 0847_ $$2rvk$$aST 130
000051706 1001_ $$0P:(DE-82)022208$$aKlink, Daniel$$b0$$eAuthor
000051706 245__ $$aThree-valued abstraction for stochastic systems$$cvorgelegt von Daniel Klink$$honline, print
000051706 246_3 $$aDreiwertige Abstraktion für stochastische Systeme$$yGerman
000051706 260__ $$aMünchen$$bHut$$c2010
000051706 300__ $$aVIII, 223 S. : graph. Darst.
000051706 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000051706 3367_ $$02$$2EndNote$$aThesis
000051706 3367_ $$2DRIVER$$adoctoralThesis
000051706 3367_ $$2BibTeX$$aPHDTHESIS
000051706 3367_ $$2DataCite$$aOutput Types/Dissertation
000051706 3367_ $$2ORCID$$aDISSERTATION
000051706 500__ $$aZsfassung in engl. und dt. Sprache
000051706 502__ $$aAachen, Techn. Hochsch., Diss., 2010$$gFak01$$o2010-03-11
000051706 520__ $$aFormal 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.$$leng
000051706 5203_ $$aDer Begriff der Formalen Methoden umfasst diverse Techniken zur mathematischen Modellierung und Verifikation von qualitativen und quantitativen Eigenschaften unterschiedlichster Systeme. Besonders hervorzuheben ist das Model Checking, ein automatisiertes Verfahren zur Verifikation von Systemen bezüglich gegebener formaler Spezifikationen. Die zugrunde liegenden Analyseverfahren basieren auf einer systematischen und vollständigen Untersuchung aller Konfigurationen des Systems, was zu einem hohen Speicherbedarf führt. Die hierzu entwickelten Gegenmaßnahmen reichen von der Verwendung effizienter Datenstrukturen bis zu einer breiten Palette von Reduktionstechniken. Diese Arbeit beschäftigt sich mit der Abstraktion – der Reduktion der über das System verfügbaren Informationsmenge – sowie mit der Frage nach den durch Abstraktion präservierten Eigenschaften. Wir konzentrieren uns auf die komplexeren quantitativen Eigenschaften probabilistischer (Echt-)Zeit Systeme, die in PCTL und CSL, probabilistischer Varianten der Computation Tree Logik (CTL), ausgedrückt werden können. Wir betrachten dazu zeitdiskrete und zeitkontinuierliche Markov-Ketten (DTMCs, CTMCs) sowie interaktive Markov-Ketten (IMCs), die das Spektrum von CTMCs um funktionales Verhalten erweitern und für die kompositionelle Modellierung von komplexen Systemen geeignet sind. Die verschiedenen Varianten von Markov-Ketten bilden die mathematische Grundlage vieler Modellierungssprachen, unter anderem aus den Bereichen der verl¨asslichen Systeme, der Leistungsbewertung und der Systembiologie. In dieser Arbeit wird die Abstraktion durch das Zusammenlegen beliebig vieler Systemkonfigurationen zu abstrakten Zuständen erreicht. Durch die Zusammenlegung von Konfigurationen mit unterschiedlichem Systemverhalten muss jedoch zusätzlicher Nichtdeterminismus in das abstrakte Modell integriert werden, um die Unbestimmtheit bezüglich des konkreten Verhaltens zum Ausdruck zu bringen. Dieser zusätzliche Nichtdeterminismus führt dazu, dass das abstrakte System ein Verhalten zeigen kann, welches im konkreten System nicht zugelassen ist; das Verhalten des konkreten Systems kann allerdings in der Abstraktion nachempfunden werden. Daher können im abstrakten Modell gewisse Eigenschaften des konkreten Modells unter bzw. überapproximiert werden. Das bedeutet, dass auch dann Schlüsse über die Eigenschaften des konkreten Modells gezogen werden können, wenn das konkrete Modell aufgrund seiner Größe nicht analysiert werden kann. Andererseits kann nicht ausgeschlossen werden, dass interessante Eigenschaften im abstrakten System weder verifiziert noch falsifiziert werden können, falls zu viele Informationen durch Abstraktion verloren gegangen sind. Um mit solchen ergebnislosen Analysen von (Teil-)Eigenschaften umgehen zu können, basiert das hier entwickelte Model Checking für abstrakte Modelle auf einer dreiwertigen Logik mit den Wahrheitswerten ja, nein und unbekannt. Bei der Generalisierung des Abstraktionsverfahrens für CTMCs hin zu den kompositionellen IMCs verfolgen wir den Ansatz, die Abstraktion bereits auf Komponentenebene statt auf Systemebene durchzuführen. Dies hat den Vorteil, dass der Speicherbedarf bei der Analyse eines abstrakten kompositionellen Modells bedeutend reduziert wird. Wir untersuchen die formale Beziehung zwischen konkreten Modellen und ihren Abstraktionen und zeigen weiterhin, dass durch die Abstraktion verschiedener Komponenten Symmetrien entstehen können, die eine weitere drastische Reduktion des Speicherbedarfs ermöglichen. Neben den theoretischen Grundlagen für Abstraktion und Model Checking von stochastischen Systemen entwickeln wir effiziente Algorithmen zur Analyse der abstrakten Modelle und zeigen an einer Fallstudie inwieweit Abstraktion die etablierten Techniken aus der Warteschlangentheorie bereichern können. Außerdem entwickeln wir ein erweitertes Abstraktionsverfahren, mit dem wir ein wohlbekanntes aber schwierig zu analysierendes Modell zur kinetischen Beschreibung von Enzymreaktionen untersuchen können.$$lger
000051706 591__ $$aGermany
000051706 650_7 $$2SWD$$aAbstraktion
000051706 650_7 $$2SWD$$aModel Checking
000051706 650_7 $$2SWD$$aMarkov-Kette mit stetiger Zeit
000051706 650_7 $$2SWD$$aVerteiltes System
000051706 650_7 $$2SWD$$aIntervallwahrscheinlichkeit
000051706 650_7 $$2SWD$$aPrioritätswarteschlange
000051706 650_7 $$2SWD$$aSystembiologie
000051706 650_7 $$2SWD$$aErlang-Verteilung
000051706 653_7 $$aInformatik
000051706 653_7 $$2eng$$aabstraction
000051706 653_7 $$2eng$$acontinuous-time Markov chain
000051706 653_7 $$2eng$$aconcurrency
000051706 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor
000051706 8564_ $$uhttps://publications.rwth-aachen.de/record/51706/files/3212.pdf
000051706 909CO $$ooai:publications.rwth-aachen.de:51706$$pVDB$$pdriver$$purn$$popen_access$$popenaire$$pdnbdelivery
000051706 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000051706 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)$$x0
000051706 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000051706 961__ $$c2013-10-25$$x2010-05-21$$z2012-02-20
000051706 970__ $$aHT016369862
000051706 980__ $$aphd
000051706 980__ $$aI:(DE-82)121310_20140620
000051706 980__ $$aI:(DE-82)120000_20140620
000051706 980__ $$aVDB
000051706 980__ $$aUNRESTRICTED
000051706 980__ $$aConvertedRecord
000051706 9801_ $$aFullTexts
000051706 980__ $$aFullTexts