Diagnosis, synthesis and analysis of probabilistic models [Elektronische Ressource] / vorgeelgt von Tingting Han

Berteun

Sujets

• Informatik
• Mathematics

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2009
• Nombre de lectures: 48
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

Diagnosis, Synthesis and Analysis
of Probabilistic Models
Tingting HanGraduation committee:
prof. dr. ir. L. van Wijngaarden University of Twente, The Netherlands
(chairman)
prof. dr. ir. J.-P. Katoen RWTH Aachen University / University of Twente,
(promotor) Germany / The Netherlands
prof. dr. P. R. D’Argenio Universidad Nacional de Co´rdoba, Argentina
prof. dr. ir. B. R. Haverkort University of Twente, The Netherlands
prof. dr. S. Leue University of Konstanz, Germany
prof. dr. J. C. van de Pol University of Twente, The Netherlands
prof. dr. R. J. Wieringa University of Twente, The Netherlands
prof. dr. F. W. Vaandrager Radboud University Nijmegen, The Netherlands
IPA Dissertation Series 2009-21.
CTIT Ph.D.-Thesis Series No. 09-149, ISSN 1381-3617.
ISBN: 978-90-365-2858-0.
TheresearchreportedinthisdissertationhasbeencarriedoutundertheauspicesoftheInstitute
for Programming Research and Algorithmics (IPA) and within the context of the Center for
Telematics and Information Technology (CTIT). The research funding was provided by the
NWO Grant through the project: Verifying Quantitative Properties of Embedded Software
(QUPES).
Translation of the Dutch abstract: Viet Yen Nguyen.
Translation of the German abstract: Martin R. Neuh¨außer.
ATypeset by LT X.E
Cover design: Tingting Han. Picture from www.vladstudio.com.
Publisher: Wo¨hrmann Printing Service - www.wps.nl.
Copyrightc 2009 by Tingting Han, Aachen, Germany.DIAGNOSIS, SYNTHESIS AND ANALYSIS
OF PROBABILISTIC MODELS
PROEFSCHRIFT
ter verkrijging van
de graad van doctor aan de Universiteit Twente,
op gezag van de rector magnificus
prof. dr. H. Brinksma,
volgens besluit van het College voor Promoties,
in het openbaar te verdedigen
op vrijdag 25 september 2009 om 13:15 uur
door
Tingting Han
geboren op 27 december 1980
te Hangzhou, Volksrepubliek ChinaDit proefschrift is goedgekeurd door
de promotor, prof. dr. ir. Joost-Pieter Katoen.DIAGNOSIS, SYNTHESIS AND ANALYSIS
OF PROBABILISTIC MODELS
Von der Fakult at fur Mathematik, Informatik und
Naturwissenschaften der Rheinisch-Westf alischen Technischen
Hochschule Aachen zur Erlangung des akademischen Grades
einer Doktorin der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Tingting Han, M.Eng
aus
Hangzhou, Volksrepublik China
Berichter: Prof. Dr. Ir. Joost-Pieter Katoen
Prof. Dr. Marta Z. Kwiatkowska
Tag der mundlic hen Prufung: 16. Oktober 2009
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online verfugbar.Acknowledgements
I still remember the summer back in 2005 when I took this PhD position. Four
years were just like a snap of fingers, leaving me this booklet and many vivid pieces of
snapshots deep and clear in my mind.
I was a “risk” four years ago when Joost-Pieter Katoen, my promotor and supervi-
sor, decided to offer me this job. After all, to Joost-Pieter at that time, I was nothing
more than a two-page CV and a short international call. I do appreciate this trust,
which in these years keeps urging me to make progress and “make profits”:). His ex-
pertise, insights and far-reaching interests broadened my views and helped me find
“shorter (if not the shortest:) paths” at each crossroad. I am grateful for his endur-
ing guidance, his great support, understanding and flexibility. I am also thankful for
his big effort and contribution going to China in 2008, visiting different universities
and institutes, giving both tutorials and more advanced invited talks, attracting more
Chinese students and researchers to the field of formal verification.
Many resultspresentedinthisthesisareaproductofjointwork. ApartfromJoost-
Pieter, I am grateful to Berteun Damman, Alexandru Mereacre and Taolue Chen, who
shared ideas, had (usually long and fruitful) discussions and transferred their expertise
to me. I am also thankful to Christel Baier, David N. Jansen and Jeremy Sproston
for their useful remark and insightful discussion on my papers. The peer review and
exchange of ideas inside the group, usually by/with Henrik Bohnenkamp, Daniel Klink
andMartinNeuh¨außerhaveprovidedmewiththeirpreciouscommentsandenlightening
thoughts. Besides, I would like to thank Prof. Marta Kwiatkowska for inviting me to
visithergroupinBirmingham. Ialsoenjoyed thevisit(s)fromHusainAljazzar, Miguel
Andr´es, Lars Grunske, Ralf Wimmer and Lijun Zhang for the interesting talks and
discussions. Besides, the regular VOSS and QUASIMODO meetings made me feel like
being in a big and happy family.
I would like also to thank my reading and defense committee in Twente: Prof.
PedroD’Argenio, Prof.BoudewijnHaverkort, Prof.StefanLeue, Prof.Jaco vandePol,
Prof.FritsVaandrager, Prof.RoelWieringaandProf. LeenvanWijngaardenaswellas
the examiners in Aachen: Prof. Gerhard Lakemeyer, Prof. Marta Kwiatkowska, Prof.
Stefan Kowalewski and Prof. Wolfgang Thomas.
AlthoughIalreadyknewinthebeginningthatIwouldmovewithJoost-Pieter from
Twente to Aachen, I had never anticipated what this “double identity” would mean to
me. Actually I always feel proud when I can fill in two affiliations. I also feel lucky
that I can get to know both top research groups. (Of course this acknowledgement will
become twice as long as it would have been.:)
iFirst,IreallyappreciatethelibertythatTwenterenderedmeduringmyPhDstudy.
TheFMTgroupissosupportive,helpfulandflexiblethatIdofeelindebttoit. Iwould
like to thank Ed Brinksma for introducing me to Joost-Pieter; and Jaco van de Pol for
his understanding and support; also many thanks to Axel Belinfante, Rom Langerak,
Arend Rensink, Theo Ruys, Mari¨elle Stoelinga, Mark Timmer, Michael Weber and
the former members Hichem Boudali and Ivan Zapreev. Special thanks go to Joke
Lammerink for everything she has done for me. Bedankt!
On the other hand, I witnessed the growth and fast developments of the MOVES
group,whichoffersmearelaxedandproductiveworkingatmosphere. Asmyroommate,
Martin Neuha¨ußer is always there and ready to help in every respect. I owe you a lot!
I am also very lucky to have Haidi Yue, Viet Yen Nguyen, Alexandru Mereacre and
Henrik Bohnenkamp around who make my laughters loud and lasting. Martin and
Viet Yen are specially thanked for translating the abstract. Also many thanks to Erika
´Abr´aham, Xin Chen, Fabian Emmes, Carsten (Fuhs|Kern|Otto), Arnd Gehrmann,
Ju¨rgen Giesl, Jonathan Heinen, Nils Jansen, Daniel Klink, Ulrich Loup, Thomas Noll,
Elke Ohlenforst and Stefan Rieger and the former members Ren´e Thiemann, Peter
Schneider-KampandStephanSwiderski. Youmademytimeinthegroupmorecolorful!
Dank sehr!
My life in Aachen would have not been as pleasant if there were no cheerful com-
pany and encouragements from friends in and outside Aachen. Just to name a few:
Sebastian Bitzen, Andreas Brand, Yiwei Cao, Qingxia Gong, Olivier Guillard, Jianwei
Han, Yingchun He, Xuan Li, Fang Liu, Leiqin Lu, Mikhail Pletyukhov, Kuangyu Shi,
Leyi Shi, Hailin Wang, Wei Wang, Yan Wang, Yutian Wang, Shaochen Wei, Wei Wu,
Ping Yu, Haidi Yue, Yuqi Zhang, Ziyun Zhang and many other friends.
I am forever indebted to my family, especially my parents in China. Without their
unconditional love, encouragement and support, I won’t reach this far.awwåå!
Also many thanks go to my little grandpa and my cousins Bin, Jian and Xiaoyun, who
share experience, give advices and send me many pictures of my lovely little nephew
and nieces.a¤k|±'%·[<Ú*l!
Finally, to Taolue, well, due to the small space here, we can do this offline...:)
Tingting Han (¸xx) Amsterdam, May 2, 2009
iiAbstract
Thisdissertation considersthreeimportantaspectsofmodelcheckingMarkov mod-
els: diagnosis — generating counterexamples, synthesis — providing valid parameter
values and analysis — verifying linear real-time properties. The three aspects are rela-
tively independentwhile 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 coun-
terexamples 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,