Abstract
Abstract
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.