INDIGO Home University of Illinois at Urbana-Champaign logo uic building uic pavilion uic student center

Model Checking Open Probabilistic Systems Using Hierarchical Probabilistic Automata

Show full item record

Bookmark or cite this item: http://hdl.handle.net/10027/21539

Files in this item

File Description Format
PDF BEN-DISSERTATION-2016.pdf (5MB) (no description provided) PDF
Title: Model Checking Open Probabilistic Systems Using Hierarchical Probabilistic Automata
Author(s): Ben, Yue
Advisor(s): Sistla, Aravinda Prasad
Contributor(s): Buy, Ugo; Venkatakrishnan, Venkat; Zefran, Milos; Viswanathan, Mahesh; Sistla, Aravinda Prasad
Department / Program: Computer Science
Degree Granting Institution: University of Illinois at Chicago
Degree: PhD, Doctor of Philosophy
Genre: Doctoral
Subject(s): Model Checking Open Probabilistic System Hierarchical Probabilistic Automata Decidability Emptiness Problem Universality Problem
Abstract: In this report we will systematically introduce using 1-HPA for model checking failure-prone open concurrent systems with respect to the non-extremal threshold language emptiness decision problem and the universal robustness problem. We have proved such problems are undecidable for 2-HPA but decidable for 1-HPA. We have developed two EXPTIME algorithms - backward algorithm and forward algorithm, and a tool - HiPAM, to model check 1-HPA, which can be obtained via combining open concurrent systems and properties expressed as deterministic automata. Properties are defined on system executions as either safety properties or non-safety properties. For some domain areas such as web applications, we have designed and implemented complete model abstraction techniques. When data models can be extracted from system models, such as in the domain of business process management, we have outlined a methodology to obtain failure specifications more precisely. Other contributions include verifying acyclic 1-HPA and proving that their language non-emptiness decision problem is NP-complete in general.
Issue Date: 2016-11-07
Type: Thesis
URI: http://hdl.handle.net/10027/21539
Rights Information: Copyright 2017 Ben, Yue
Date Available in INDIGO: 2017-02-17
Date Deposited: December 2
 

This item appears in the following Collection(s)

Show full item record

Statistics

Country Code Views
China 57
United States of America 44
Russian Federation 11
Ukraine 5
Germany 2

Browse

My Account

Information

Access Key