Repair of timed automata for non-vacuous satisfaction of requirements

Date

2023-9-09

Author

Taytak, Mert Alp

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

46
views

31
downloads

Cite This

In the field of formal verification, timed automata are used to formalize real-time systems and their requirements. Modeling a system with a timed automaton enables the use of formal methods to analyze the model for the existence or lack of certain characteristics. One such characteristic is the property of vacuity. In simplified terms, vacuity is the existence of a subset of the requirements which can be replaced with a simpler counterpart without altering the logical valuation of the set of the requirements. In this thesis, we propose algorithms to identify and remove causes of vacuity from timed automata so that the resulting automata will not be vacuous.

Subject Keywords

Vacuity, Timed automata, Repair, Reduction

URI

https://hdl.handle.net/11511/105607

Collections

Graduate School of Natural and Applied Sciences, Thesis