THE PRELIMINARY ORAL EXAMINATION FOR THE DEGREE OF Ph.D. IN COMPUTER SCIENCE FOR

                             Peter Fontana

Timed automata are real-time system models that can both express real-time constraints and be model-checked (verified) in practice. Many timed automata verification tools exist, but timed automata theory lags behind them. For instance, tools use different timed automata variants but do not always make clear which theoretical results carry over to these variants. The thesis of my dissertation proposal is to develop a unified theory of timed automata for enhancing the use of timed automata in practice.

First, I plan to formalize and equate many of these variants. Additionally, I plan to provide conversions between equivalent variants. Equating variants allows theoretical results of one variant to apply to equivalent variants, unifying their theory. Second, I plan to prove powerful expressive properties about different logics for timed behavior, and as a result, enlarge the set of verifiable properties. Third, I plan to take experimental design and analysis techniques from multiple research areas to improve the experimental analysis of timed automata tools. Last, I plan to implement a verification tool for an expressive fixpoint-based logic, demonstrating another application of this newly developed theory.

Examining Committee:

Dr. Rance Cleaveland                    -          Chair

Dr. William Gasarch                        -          Dept’s Representative

Dr. Michael Hicks                             -          Committee Member 

EVERYBODY IS INVITED TO ATTEND THE PRESENTATION