University of Twente Student Theses
Exclusion of Non-Divergence in Probabilistic Timed Automata Model Checking
Vreman, S. (2024) Exclusion of Non-Divergence in Probabilistic Timed Automata Model Checking.
|
PDF
836kB |
| Abstract: | Model checking is a method to check the correctness of a model of a system. It is important that a model representing a real world system is verified in a meaningful way, only considering behaviour the real system can exhibit. In probabilistic timed automata, time divergence should always occur, an example of this not happening is infinitely many actions being taken in a finite amount of time, which does not correspond to any real-world system. Digital clocks are often used for model checking but a check for time divergence is required for their result to be meaningful. We show how existing algorithms can be adapted to check for this using a digital clocks approach for model checking. After this, we show the performance impact of this new implementation in terms of runtime. Finally, we show the result of this check on existing benchmark models. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science BSc (56964) |
| Link to this item: | https://purl.utwente.nl/essays/100755 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page