{"id":{"repo_id":"cape-town","oai_identifier":"oai:open.uct.ac.za:11427/6412"},"canonical_url":"https://search.dev.ndltd.org/etd/cape-town/oai:open.uct.ac.za:11427/6412","repository":{"repo_id":"cape-town","name":"University of Cape Town","base_url":"https://open.uct.ac.za/oai/request"},"display":{"title":"Specification and verification of systems using model checking and Markov reward models","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Lifson, Farrel"],"institution":"Department of Computer Science","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Kritzinger, Pieter S"],"committee_chairs":[],"committee_members":[],"year":2004,"date_issued":"2004","date_published":"2004","updated_at":"2026-07-22T22:23:46Z","subjects":[],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/11427/6412","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Kritzinger, Pieter S"]},{"key":"dc:creator","label":"Author","values":["Lifson, Farrel"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2014-08-13T19:31:18Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2014-08-13T19:31:18Z"]},{"key":"dc:date.issued","label":"Date","values":["2004"]},{"key":"dc:publisher.department","label":"Dc Publisher Department","values":["Department of Computer Science"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Cape Town"]},{"key":"dc:type","label":"Dc Type","values":["Master Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Masters"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["MSc"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/11427/6412"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Includes bibliographical references."]},{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Specification and verification of systems using model checking and Markov reward models"]}]}],"canonical_facts":{"dc:contributor.advisor":["Kritzinger, Pieter S"],"dc:creator":["Lifson, Farrel"],"dc:date.accessioned":["2014-08-13T19:31:18Z"],"dc:date.available":["2014-08-13T19:31:18Z"],"dc:date.issued":["2004"],"dc:description":["Includes bibliographical references."],"dc:description.abstract":["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."],"dc:identifier.uri":["http://hdl.handle.net/11427/6412"],"dc:language.iso":["eng"],"dc:publisher.department":["Department of Computer Science"],"dc:publisher.institution":["University of Cape Town"],"dc:title":["Specification and verification of systems using model checking and Markov reward models"],"dc:type":["Master Thesis"],"dc:type.qualificationlevel":["Masters"],"dc:type.qualificationname":["MSc"]},"updated_at":"2026-07-22T22:23:46Z"}