University of Twente Student Theses
As of Friday, 8 August 2025, the current Student Theses repository is no longer available for thesis uploads. A new Student Theses repository will be available starting Friday, 15 August 2025.
Extending Digital Clocks to Support Diagonal Constraints in Probabilistic Timed Automata
Vartic, Melania (2025) Extending Digital Clocks to Support Diagonal Constraints in Probabilistic Timed Automata.
|
PDF
539kB |
| Abstract: | Model-checking is a method used for verifying the temporal behaviour of a system and whether a model achieves its desired properties. This approach is often fully automated and is applied, among other areas, within the context of timed automata. Timed automata are a formalism that captures properties related to quantitative time, facilitating the modelling of real-time systems where time is a significant aspect. Probabilistic timed automata are an extension of classical timed automata, with the capacity to model the uncertainty of events along with timing constraints. The digital clock method in probabilistic timed automata abstracts real-valued clock variables into integer representations, resulting in a finite-state model that preserves the timing properties required in formal verification. This abstraction is typically sound for diagonal-free clocks, where the constraints of a clock can be only in relation to a constant, not to another clock. We analyse the behaviour of a digital clock abstraction algorithm developed in the Modest Toolset when presented with diagonal constraints and modify it to accommodate them. We used extended semantics to explore more states around the diagonal and changed the reset function to stay within the bounds, studying the correctness of the algorithm and how it behaves when presented with more clock variables. |
| 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/107357 |
| 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