Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Specification and verification of systems using model checking and Markov reward models
Includes bibliographical references.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
Department of Computer Science
2014
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867614362729971712 |
|---|---|
| access_status_str | Open Access |
| author | Lifson, Farrel |
| author2 | Kritzinger, Pieter S |
| author_browse | Kritzinger, Pieter S Lifson, Farrel |
| author_facet | Kritzinger, Pieter S Lifson, Farrel |
| author_sort | Lifson, Farrel |
| collection | Thesis |
| description | Includes bibliographical references. |
| format | Thesis |
| id | oai:open.uct.ac.za:11427/6412 |
| institution | University of Cape Town (South Africa) |
| language | eng |
| last_indexed | 2026-06-10T12:50:50.687Z |
| license_str | Not specified — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from UCTD — University of Cape Town Open Access Repository |
| publishDate | 2014 |
| publishDateRange | 2014 |
| publishDateSort | 2014 |
| publisher | Department of Computer Science |
| publisherStr | Department of Computer Science |
| record_format | dspace |
| source_str | UCTD — University of Cape Town Open Access Repository |
| spelling | oai:open.uct.ac.za:11427/6412 Specification and verification of systems using model checking and Markov reward models Lifson, Farrel Kritzinger, Pieter S Computer Science Includes bibliographical references. 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. 2014-08-13T19:31:18Z 2014-08-13T19:31:18Z 2004 Master Thesis Masters MSc http://hdl.handle.net/11427/6412 eng application/pdf Department of Computer Science Faculty of Science University of Cape Town |
| spellingShingle | Computer Science Lifson, Farrel Specification and verification of systems using model checking and Markov reward models |
| thesis_degree_str | Master's |
| title | Specification and verification of systems using model checking and Markov reward models |
| title_full | Specification and verification of systems using model checking and Markov reward models |
| title_fullStr | Specification and verification of systems using model checking and Markov reward models |
| title_full_unstemmed | Specification and verification of systems using model checking and Markov reward models |
| title_short | Specification and verification of systems using model checking and Markov reward models |
| title_sort | specification and verification of systems using model checking and markov reward models |
| topic | Computer Science |
| url | http://hdl.handle.net/11427/6412 |
| work_keys_str_mv | AT lifsonfarrel specificationandverificationofsystemsusingmodelcheckingandmarkovrewardmodels |