{"@context":"http://iiif.io/api/presentation/2/context.json","@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/manifest.json","@type":"sc:Manifest","label":"Verification of Probabilistic Branching Time Systems","metadata":[{"label":"dc.description.sponsorship","value":"This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree."},{"label":"dc.format","value":"Monograph"},{"label":"dc.format.medium","value":"Electronic Resource"},{"label":"dc.identifier.uri","value":"http://hdl.handle.net/11401/77237"},{"label":"dc.language.iso","value":"en_US"},{"label":"dc.publisher","value":"The Graduate School, Stony Brook University: Stony Brook, NY."},{"label":"dcterms.abstract","value":"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."},{"label":"dcterms.available","value":"2017-09-20T16:52:15Z"},{"label":"dcterms.contributor","value":"Cleaveland, Rance."},{"label":"dcterms.creator","value":"Gorlin, Andrey"},{"label":"dcterms.dateAccepted","value":"2017-09-20T16:52:15Z"},{"label":"dcterms.dateSubmitted","value":"2017-09-20T16:52:15Z"},{"label":"dcterms.description","value":"Department of Computer Science"},{"label":"dcterms.extent","value":"115 pg."},{"label":"dcterms.format","value":"Application/PDF"},{"label":"dcterms.identifier","value":"http://hdl.handle.net/11401/77237"},{"label":"dcterms.issued","value":"2016-12-01"},{"label":"dcterms.language","value":"en_US"},{"label":"dcterms.provenance","value":"Made available in DSpace on 2017-09-20T16:52:15Z (GMT). No. of bitstreams: 1\nGorlin_grad.sunysb_0771E_13118.pdf: 934016 bytes, checksum: b926248c9831c17a2254afe6919a704b (MD5)\n  Previous issue date:    1"},{"label":"dcterms.publisher","value":"The Graduate School, Stony Brook University: Stony Brook, NY."},{"label":"dcterms.subject","value":"Computer science"},{"label":"dcterms.title","value":"Verification of Probabilistic Branching Time Systems"},{"label":"dcterms.type","value":"Dissertation"},{"label":"dc.type","value":"Dissertation"}],"description":"This manifest was generated dynamically","viewingDirection":"left-to-right","sequences":[{"@type":"sc:Sequence","canvases":[{"@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/canvas/page-1.json","@type":"sc:Canvas","label":"Page 1","height":1650,"width":1275,"images":[{"@type":"oa:Annotation","motivation":"sc:painting","resource":{"@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/63%2F03%2F68%2F63036870887993975896479882787802796102/full/full/0/default.jpg","@type":"dctypes:Image","format":"image/jpeg","height":1650,"width":1275,"service":{"@context":"http://iiif.io/api/image/2/context.json","@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/63%2F03%2F68%2F63036870887993975896479882787802796102","profile":"http://iiif.io/api/image/2/level2.json"}},"on":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/canvas/page-1.json"}]}]}]}