Type
Text
Type
Dissertation
Advisor
Ramakrishnan, C. R. | Stoller, Scott D | Smolka, Scott A | Cleaveland, Rance.
Date
2016-12-01
Keywords
Computer science | branching time, logic programming, model checking, probabilistic systems
Department
Department of Computer Science
Language
en_US
Source
This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree.
Identifier
http://hdl.handle.net/11401/77237
Publisher
The Graduate School, Stony Brook University: Stony Brook, NY.
Format
application/pdf
Abstract
This thesis deals with verification of complex systems, which involve probabilistic choices. In total, we explore three interrelated problems. First, we explore probabilistic extensions of mu-calculus. GPL extends mu-calculus by having all the probabilistic choices made first; this keeps the model checking procedure decidable for any property. We extend GPL to a logic, XPL, which is undecidable, in general. We define a syntactic property of an XPL formula, separability, as a sufficient condition for model checking. Second, we can frame the problem of probabilistic model checking as query evaluation over probabilistic logic programs. We have developed an inference algorithm, PIP, using tabled logic programming, which is sufficiently powerful to verify GPL and separable XPL properties. PIP uses finite generative structures, called FEDs, to represent families of explanations. Finally, we explore an alternative paradigm for verification of temporal models: compositional or partial model checking. In particular, we employ a technique called quotienting, where we take a mu-calculus formula and a process and return another formula that must be satisfied by the remainder of the system. | 115 pages
Recommended Citation
Gorlin, Andrey, "Verification of Probabilistic Branching Time Systems" (2016). Stony Brook Theses and Dissertations Collection, 2006-2020 (closed to submissions). 3064.
https://commons.library.stonybrook.edu/stony-brook-theses-and-dissertations-collection/3064