h1

000051529 001__ 51529
000051529 005__ 20250616090926.0
000051529 020__ $$a978-90-365-2858-0
000051529 0247_ $$2HSB$$ahsb910018371
000051529 0247_ $$2ISSN$$a1381-3617
000051529 0247_ $$2Laufende Nummer$$a29920
000051529 0247_ $$2OPUS$$a3139
000051529 0247_ $$2URN$$aurn:nbn:de:hbz:82-opus-31398
000051529 037__ $$aRWTH-CONV-113814
000051529 041__ $$aEnglish
000051529 082__ $$a004
000051529 1001_ $$0P:(DE-82)020174$$aHan, Tingting$$b0$$eAuthor
000051529 245__ $$aDiagnosis, synthesis and analysis of probabilistic models$$cvorgelegt von Tingting Han$$honline, print
000051529 246_3 $$aDiagnose, Synthese und Analyse probabilistischer Modelle$$yGerman
000051529 260__ $$aEnschede$$bUniv. Twente$$c2009
000051529 300__ $$aXII, 191 S. : graph. Darst.
000051529 3367_ $$02$$2EndNote$$aThesis
000051529 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000051529 3367_ $$2BibTeX$$aPHDTHESIS
000051529 3367_ $$2DRIVER$$adoctoralThesis
000051529 3367_ $$2DataCite$$aOutput Types/Dissertation
000051529 3367_ $$2ORCID$$aDISSERTATION
000051529 3367_ $$0PUB:(DE-HGF)3$$2PUB:(DE-HGF)$$aBook$$mbook
000051529 4900_ $$aIPA dissertation series$$v2009-21
000051529 500__ $$aZsfassung in engl. und dt. Sprache. - Weitere Reihe: CTIT Ph. D. thesis series ; 09-149
000051529 502__ $$aZugl.: Aachen, Techn. Hochsch., Diss., 2009$$gFak01$$o2009-10-16
000051529 5203_ $$aIn dieser Dissertation werden drei wichtige Aspekte bei der Modellüberprüfung von Markov-Modellen betrachtet: Die Diagnose --- das Generieren von Gegenbeispielen, die Synthese --- das zur Verfügung stellen korrekter Parameterwerte und die Analyse --- das Verifizieren von linearen Realzeiteigenschaften. Die drei Aspekte sind vergleichsweise unabhängig, obwohl sie alle dem Zweck dienen, neue Theorie und Algorithmen für das Forschungsfeld der probabilistischen Modellüberprüfung zu entwickeln. Zu Beginn führen wir eine formale Definition von Gegenbeispielen im Bereich der probabilistische Modellüberprüfung ein. Wir transformieren das Problem, informative Gegenbeispiele zu finden, auf das Shortest-Path Problem. Es wird ein Framework untersucht und entwickelt um solche Gegenbeispiele zu erzeugen. Weiterhin untersuchen wir eine kompaktere Darstellung von Gegenbeispielen durch reguläre Ausdrücke. Algorithmen, die auf Heuristiken basieren, werden genutzt, um kurze reguläre Ausdruüke als Gegenbeispiele zu erhalten. Am Ende dieses Teils erweitern wir die Definition und die Algorithmen zum Generieren von Gegenbeispielen auf verschiedene Kombinationen von probabilistischen Modellen und Logiken. Danach betrachten wir das Problem, Werte für parametrisierte zeitkontinuierliche Markovketten (pCTMCs) bezüglich zeitbeschränkter Erreichbarkeitseigenschaften zu synthetisieren. Das Ziel hierbei ist es, alle Werte für die Ratenparameter (die eine Syntheseregion bilden) zu finden, die die Spezifikation erfüllen können; hierbei sind die Ratenausdrücke Polynome über den reellen Zahlen. Zuerst stellen wir einen symbolischen Ansatz vor, in dem zunächst die Schnittpunkte durch das Lösen von Polynomgleichungen berechnet und dann miteinander verbunden werden, um die Syntheseregion zu approximieren. Ein anderer, nicht symbolischer Ansatz, der auf Intervallarithmetik beruht und für den pCTMCs instanziiert werden, wird ebenfalls untersucht. Die Fehlerschranke, die Zeitkomplexität sowie einige experimentelle Resultate werden dargestellt, gefolgt von einem detaillierten Vergleich der beiden Ansätze. Im letzten Abschnitt steht das Verifizieren von linearen Realzeiteigenschaften auf CTMCs im Vordergrund, wobei die Eigenschaften als deterministische Zeitautomaten (DTA) gegeben sind. Das Modellüberprüfungsproblem zielt darauf ab, die Wahrscheinlichkeit der Menge aller Pfade einer CTMC C, die von einem DTA A akzeptiert werden, zu bestimmen. Wir betrachten DTAs mit Erreichbarkeits- (endliche, DTAr) und Muller- (unendliche, DTAo) Akzeptanzbedingungen. Es wird gezeigt, dass Paths^C(A) messbar ist und dass die Berechnung dieser Wahrscheinlichkeit im Falle von DTAr auf die Berechnung der Erreichbarkeitswahrscheinlichkeit in einem Piecewise Deterministic Markov Process (PDP) reduziert werden kann. Die Erreichbarkeitswahrscheinlichkeit wird charakterisiert als die kleinste Lösung eines Systems von Integralgleichungen und es wird gezeigt, dass sie durch Lösen eines Systems von PDEs approximiert werden kann. Weiterhin zeigen wir, dass der Spezialfall eines DTAr, der auf eine Uhrenvariable beschränkt ist, zu einem linearen Gleichungssystem vereinfacht werden kann. Zusätzlich betrachten wir DTAo Spezifikationen und zeigen, dass das Problem hier wie im Fall von DTAr auf das Erreichbarkeitsproblem reduziert werden kann.$$lger
000051529 520__ $$aThis dissertation considers three important aspects of model checking Markov models: diagnosis --- generating counterexamples, synthesis --- providing valid parameter values and analysis --- verifying linear real-time properties. The three aspects are relatively independent while all contribute to developing new theory and algorithms in the research field of probabilistic model checking. We start by introducing a formal definition of counterexamples in the setting of probabilistic model checking. We transform the problem of finding informative counterexamples to shortest path problems. A framework is explored and provided for generating such counterexamples. We then investigate a more compact representation of counterexamples by regular expressions. Heuristic based algorithms are applied to obtain short regular expression counterexamples. In the end of this part, we extend the definition and counterexample generation algorithms to various combinations of probabilistic models and logics. We move on to the problem of synthesizing values for parametric continuous-time Markov chains (pCTMCs) wrt. time-bounded reachability specifications. The rates in the pCTMCs are expressed by polynomials over reals with parameters and the main question is to find all the parameter values (forming a synthesis region) with which the specification is satisfied. We first present a symbolic approach where the intersection points are computed by solving polynomial equations and then connected to approximate the synthesis region. An alternative non-symbolic approach based on interval arithmetic is investigated, where pCTMCs are instantiated. The error bound, time complexity as well as some experimental results have been provided, followed by a detailed comparison of the two approaches. In the last part, we focus on verifying CTMCs against linear real-time properties specified by deterministic timed automata (DTAs). The model checking problem aims at computing the probability of the set of paths in CTMC C that can be accepted by DTA A, denoted Paths^C(A). We consider DTAs with reachability (finite, DTAr) and Muller (infinite, DTAo) acceptance conditions, respectively. It is shown that Paths^C(A) is measurable and computing its probability for DTAr can be reduced to computing the reachability probability in a piecewise deterministic Markov process PDP. The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of PDEs. Furthermore, we show that the special case of single-clock DTAr can be simplified to solving a system of linear equations. We also deal with DTAo specifications, where the problem is proven to be reducible to the reachability problem as in the DTAr case.$$leng
000051529 591__ $$aGermany
000051529 650_7 $$2SWD$$aModel Checking
000051529 650_7 $$2SWD$$aRichtigkeit von Ergebnissen
000051529 650_7 $$2SWD$$aStochastischer Automat
000051529 653_7 $$2eng$$acounterexamples
000051529 653_7 $$2eng$$alinear real-time properties
000051529 653_7 $$2eng$$aparameter synthesis
000051529 653_7 $$2eng$$aprobabilistic model checking
000051529 653_7 $$2eng$$averification
000051529 653_7 $$2ger$$aVerifikation
000051529 653_7 $$aInformatik
000051529 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor
000051529 8564_ $$uhttps://publications.rwth-aachen.de/record/51529/files/Han_Tingting.pdf
000051529 909CO $$ooai:publications.rwth-aachen.de:51529$$pdnbdelivery$$popenaire$$popen_access$$purn$$pdriver$$pVDB
000051529 9141_ $$y2009
000051529 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000051529 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)$$x0
000051529 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000051529 961__ $$c2013-11-21$$x2010-02-26$$z2012-02-20
000051529 970__ $$aHT016259336
000051529 9801_ $$aFullTexts
000051529 980__ $$aConvertedRecord
000051529 980__ $$aFullTexts
000051529 980__ $$aI:(DE-82)120000_20140620
000051529 980__ $$aI:(DE-82)121310_20140620
000051529 980__ $$aUNRESTRICTED
000051529 980__ $$aVDB
000051529 980__ $$aphd
000051529 980__ $$abook