Specification and verification of systems using model checking and Markov reward models

Simple item page
dc.contributor.advisorKritzinger, Pieter Sen_ZA
dc.contributor.authorLifson, Farrelen_ZA
dc.date.accessioned2014-08-13T19:31:18Z
dc.date.available2014-08-13T19:31:18Z
dc.date.issued2004en_ZA
dc.descriptionIncludes bibliographical references.en_ZA
dc.description.abstractThis thesis examines Markov reward models, a formalism based on continuous time Markov chains, and it's usage in the generation and analysis of service levels. The particular solution technique we employ in this thesis is model checking, using Continuous Reward Logic as a means to specify requirement and constraints on the model. We survey the current tools available allowing model checking to be performed on Markov reward models. Specifically we extended the Erlangen-Twente Markov Chain Checker to be able to solve Markov reward models by taking advantage of the Duality theorem of Continuous Stochastic Reward Logic, of which Continuous Reward Logic is a sub-logic. We are also concerned with the specification techniques available for Markov reward models, which have in the past merely been extensions to the available specification techniques for continuous time Markov chains.en_ZA
dc.identifier.apacitationLifson, F. (2004). <i>Specification and verification of systems using model checking and Markov reward models</i>. (Thesis). University of Cape Town ,Faculty of Science ,Department of Computer Science. Retrieved from http://hdl.handle.net/11427/6412en_ZA
dc.identifier.chicagocitationLifson, Farrel. <i>"Specification and verification of systems using model checking and Markov reward models."</i> Thesis., University of Cape Town ,Faculty of Science ,Department of Computer Science, 2004. http://hdl.handle.net/11427/6412en_ZA
dc.identifier.citationLifson, F. 2004. Specification and verification of systems using model checking and Markov reward models. University of Cape Town.en_ZA
dc.identifier.ris TY - Thesis / Dissertation AU - Lifson, Farrel AB - This thesis examines Markov reward models, a formalism based on continuous time Markov chains, and it's usage in the generation and analysis of service levels. The particular solution technique we employ in this thesis is model checking, using Continuous Reward Logic as a means to specify requirement and constraints on the model. We survey the current tools available allowing model checking to be performed on Markov reward models. Specifically we extended the Erlangen-Twente Markov Chain Checker to be able to solve Markov reward models by taking advantage of the Duality theorem of Continuous Stochastic Reward Logic, of which Continuous Reward Logic is a sub-logic. We are also concerned with the specification techniques available for Markov reward models, which have in the past merely been extensions to the available specification techniques for continuous time Markov chains. DA - 2004 DB - OpenUCT DP - University of Cape Town LK - https://open.uct.ac.za PB - University of Cape Town PY - 2004 T1 - Specification and verification of systems using model checking and Markov reward models TI - Specification and verification of systems using model checking and Markov reward models UR - http://hdl.handle.net/11427/6412 ER - en_ZA
dc.identifier.urihttp://hdl.handle.net/11427/6412
dc.identifier.vancouvercitationLifson F. Specification and verification of systems using model checking and Markov reward models. [Thesis]. University of Cape Town ,Faculty of Science ,Department of Computer Science, 2004 [cited yyyy month dd]. Available from: http://hdl.handle.net/11427/6412en_ZA
dc.language.isoengen_ZA
dc.publisher.departmentDepartment of Computer Scienceen_ZA
dc.publisher.facultyFaculty of Scienceen_ZA
dc.publisher.institutionUniversity of Cape Town
dc.subject.otherComputer Scienceen_ZA
dc.titleSpecification and verification of systems using model checking and Markov reward modelsen_ZA
dc.typeMaster Thesis
dc.type.qualificationlevelMasters
dc.type.qualificationnameMScen_ZA
uct.type.filetypeText
uct.type.filetypeImage
uct.type.publicationResearchen_ZA
uct.type.resourceThesisen_ZA
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
thesis_sci_2004_lifson_f.pdf
Size:
4.01 MB
Format:
Adobe Portable Document Format
Description:
Download
Collections
Masters