Landsaat, Eelke (2022) A Model Checker for Game Logic via Parity Games. Bachelor's Thesis, Computing Science.
|
Text
bCS_2022_LandsaatE.pdf Download (2MB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf Restricted to Registered users only Download (126kB) |
Abstract
Model checking of logical models is establishing whether a formula is satisfied in a model under certain conditions. Logical models are the groundwork of many software protocols, and ensuring that these protocols work as intended is essential to building reliable applications. Automated model checkers are thus a valuable tool for verifying the correctness of such software protocols. Game logic is a branch of logic that focuses on strategic interactions between two agents. Although a theoretical foundation for the model checking of game models (models of game logic) already exists, a model checker for them remains absent. In this thesis, a model checker for game models is implemented through a conversion step to the solving of parity games. To this end, the state of the art around game logic, parity games and model checking is inspected, the procedures of the model checker are discussed, and the implementation is evaluated. Additionally, an experimental time complexity analysis is performed on the model checker based on existing literature on a theoretical time complexity bound for the model checking problem for game logic.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Hansen, H.H. and Perez Parra, J.A. |
| Degree programme: | Computing Science |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 26 Jul 2022 06:36 |
| Last Modified: | 26 Jul 2022 06:36 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/28126 |
Actions (login required)
 |
View Item |