Towards a Unified Theory of Timed Automata

Simple item page
dc.contributor.advisorCleaveland, Ranceen_US
dc.contributor.authorFontana, Peter Christopheren_US
dc.contributor.departmentComputer Scienceen_US
dc.contributor.publisherDigital Repository at the University of Marylanden_US
dc.contributor.publisherUniversity of Maryland (College Park, Md.)en_US
dc.date.accessioned2014-06-24T05:52:58Z
dc.date.available2014-06-24T05:52:58Z
dc.date.issued2014en_US
dc.description.abstractTimed automata are finite-state machines augmented with special clock variables that reflect the advancement of time. Able to both capture real-time behavior and be verified algorithmically (model-checked), timed automata are used to model real-time systems. These observations have led to the development of several timed-automata verification tools that have been successfully applied to the analysis of a number of different systems; however, the practical utility of timed automata is undermined by the theories underlying different tools differing in subtle but important ways. Since algorithmic results that hold for the variant used by one tool may not apply to another variant, this complicates the application of different tools to different models. The thesis of this dissertation is this: the theory of timed automata can be unified, and a practical unified approach to timed-automata model checking can be built around the paradigm of proof search. First, this dissertation establishes the mutual expressivity of timed automata variants, thereby providing precise characterizations of when theoretical results of one variant apply to other variants. Second, it proves powerful expressive properties about different logics for timed behavior, and as a result, enlarges the set of verifiable properties. Third, it discusses an implementation of a verification tool for an expressive fixpoint-based logic, demonstrating an application of this newly developed theory. The tool is based on a proof-search paradigm; verifying timed automata involves constructing proofs using proof rules that enable verification problems to be translated into subproblems that must be solved. The tool's performance is optimized by using derived proof rules, thereby providing a theoretically sound basis for faster model checking. Last, this dissertation utilizes the proofs generated during verification to gain additional information about the vacuous satisfaction of certain formulae: whether the automaton satisfied a formula by never satisfying certain premises of that specification. This extra information is often obtained without significantly decreasing the verifier's performance.en_US
dc.identifier.urihttp://hdl.handle.net/1903/15232
dc.language.isoenen_US
dc.subject.pqcontrolledComputer scienceen_US
dc.subject.pquncontrolledModel Checkingen_US
dc.subject.pquncontrolledReal-Time Model Checkingen_US
dc.subject.pquncontrolledTimed Automataen_US
dc.subject.pquncontrolledTimed Logicsen_US
dc.subject.pquncontrolledTimed Mu-Calculusen_US
dc.titleTowards a Unified Theory of Timed Automataen_US
dc.typeDissertationen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Fontana_umd_0117E_15027.pdf
Size:
3.07 MB
Format:
Adobe Portable Document Format
Download

Collections

UMD Theses and Dissertations
Computer Science Theses and Dissertations