guest ::
| 001 | 51706 | ||
| 005 | 20220422215714.0 | ||
| 020 | _ | _ | |a 978-3-86853-408-5 |
| 024 | 7 | _ | |2 Laufende Nummer |a 30208 |
| 024 | 7 | _ | |2 URN |a urn:nbn:de:hbz:82-opus-32124 |
| 024 | 7 | _ | |2 HSB |a hsb910019682 |
| 024 | 7 | _ | |2 OPUS |a 3212 |
| 037 | _ | _ | |a RWTH-CONV-113970 |
| 041 | _ | _ | |a English |
| 082 | _ | _ | |a 004 |
| 084 | 7 | _ | |2 rvk |a ST 130 |
| 100 | 1 | _ | |0 P:(DE-82)022208 |a Klink, Daniel |b 0 |e Author |
| 245 | _ | _ | |a Three-valued abstraction for stochastic systems |c vorgelegt von Daniel Klink |h online, print |
| 246 | _ | 3 | |a Dreiwertige Abstraktion für stochastische Systeme |y German |
| 260 | _ | _ | |a München |b Hut |c 2010 |
| 300 | _ | _ | |a VIII, 223 S. : graph. Darst. |
| 336 | 7 | _ | |a Dissertation / PhD Thesis |0 PUB:(DE-HGF)11 |2 PUB:(DE-HGF) |b phd |m phd |
| 336 | 7 | _ | |a Thesis |0 2 |2 EndNote |
| 336 | 7 | _ | |a doctoralThesis |2 DRIVER |
| 336 | 7 | _ | |a PHDTHESIS |2 BibTeX |
| 336 | 7 | _ | |a Output Types/Dissertation |2 DataCite |
| 336 | 7 | _ | |a DISSERTATION |2 ORCID |
| 500 | _ | _ | |a Zsfassung in engl. und dt. Sprache |
| 502 | _ | _ | |o 2010-03-11 |a Aachen, Techn. Hochsch., Diss., 2010 |g Fak01 |
| 520 | _ | _ | |a 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. |l eng |
| 520 | 3 | _ | |a Der 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. |l ger |
| 591 | _ | _ | |a Germany |
| 650 | _ | 7 | |a Abstraktion |2 SWD |
| 650 | _ | 7 | |a Model Checking |2 SWD |
| 650 | _ | 7 | |a Markov-Kette mit stetiger Zeit |2 SWD |
| 650 | _ | 7 | |a Verteiltes System |2 SWD |
| 650 | _ | 7 | |a Intervallwahrscheinlichkeit |2 SWD |
| 650 | _ | 7 | |a Prioritätswarteschlange |2 SWD |
| 650 | _ | 7 | |a Systembiologie |2 SWD |
| 650 | _ | 7 | |a Erlang-Verteilung |2 SWD |
| 653 | _ | 7 | |a Informatik |
| 653 | _ | 7 | |a abstraction |2 eng |
| 653 | _ | 7 | |a continuous-time Markov chain |2 eng |
| 653 | _ | 7 | |a concurrency |2 eng |
| 700 | 1 | _ | |a Katoen, Joost-Pieter |0 P:(DE-82)IDM00048 |b 1 |e Thesis advisor |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/51706/files/3212.pdf |
| 909 | C | O | |o oai:publications.rwth-aachen.de:51706 |p openaire |p open_access |p urn |p driver |p VDB |p dnbdelivery |
| 915 | _ | _ | |0 StatID:(DE-HGF)0510 |2 StatID |a OpenAccess |
| 920 | 1 | _ | |0 I:(DE-82)121310_20140620 |k 121310 |l Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) |x 0 |
| 920 | 1 | _ | |0 I:(DE-82)120000_20140620 |k 120000 |l Fachgruppe Informatik |x 1 |
| 970 | _ | _ | |a HT016369862 |
| 980 | _ | _ | |a phd |
| 980 | _ | _ | |a I:(DE-82)121310_20140620 |
| 980 | _ | _ | |a I:(DE-82)120000_20140620 |
| 980 | _ | _ | |a VDB |
| 980 | _ | _ | |a UNRESTRICTED |
| 980 | _ | _ | |a ConvertedRecord |
| 980 | 1 | _ | |a FullTexts |
| 980 | _ | _ | |a FullTexts |
| Library | Collection | CLSMajor | CLSMinor | Language | Author |
|---|