@Article{alur_theory_1994,
  Title                    = {A Theory of Timed Automata},
  Author                   = {Alur, Rajeev and Dill, David L.},
  Journal                  = {Theoretical Computer Science},
  Year                     = {1994},
  Pages                    = {183--235},
  Volume                   = {126},

  Abstract                 = {. We propose timed (finite) automata to model the behavior of realtime systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many realvalued clocks . A timed automaton accepts timed words --- infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Buchi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an ({PSPACE}) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also p...},
  File                     = {Citeseer - Full Text PDF:C\:\\Users\\wimme_000\\AppData\\Roaming\\Zotero\\Zotero\\Profiles\\p676id6w.default\\zotero\\storage\\RX7I4M4V\\Alur and Dill - 1994 - A Theory of Timed Automata.pdf:application/pdf;Citeseer - Snapshot:C\:\\Users\\wimme_000\\AppData\\Roaming\\Zotero\\Zotero\\Profiles\\p676id6w.default\\zotero\\storage\\BSZXS5TB\\Alur and Dill - 1994 - A Theory of Timed Automata.html:text/html}
}

@InProceedings{alur_automata_1990,
  Title                    = {Automata for Modeling Real-time Systems},
  Author                   = {Alur, Rajeev and Dill, D. L.},
  Booktitle                = {Proceedings of the Seventeenth International Colloquium on Automata, Languages and Programming},
  Year                     = {1990},

  Address                  = {New York, {NY}, {USA}},
  Pages                    = {322--335},
  Publisher                = {Springer-Verlag New York, Inc.},

  ISBN                     = {0-387-52826-1},
  Url                      = {http://dl.acm.org/citation.cfm?id=90397.90438},
  Urldate                  = {2014-11-30}
}

@InCollection{dill_timing_1990,
  Title                    = {Timing assumptions and verification of finite-state concurrent systems},
  Author                   = {Dill, David L.},
  Booktitle                = {Automatic Verification Methods for Finite State Systems},
  Publisher                = {Springer Berlin Heidelberg},
  Year                     = {1990},
  Month                    = jan,
  Number                   = {407},
  Pages                    = {197--212},
  Series                   = {Lecture Notes in Computer Science},

  Abstract                 = {We have described a scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties. The obvious extension is to be able to prove timing properties, not just assume them. This would provide a verification framework for finite-state hard real-time systems. We conjecture that the method presented can, in fact, be extended in this way. Another major question is practicality. We believe that, with some simple program optimizations, the proposed method can be useful for certain small but tricky systems, such as asynchronous control circuits. For larger systems, approximate and heuristic methods will be needed.},
  Copyright                = {\<copyright>1990 Springer-Verlag},
  File                     = {Snapshot:C\:\\Users\\wimme_000\\AppData\\Roaming\\Zotero\\Zotero\\Profiles\\p676id6w.default\\zotero\\storage\\6C8HVQDG\\10.html:text/html},
  ISBN                     = {978-3-540-52148-8, 978-3-540-46905-6},
  Keywords                 = {Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Software Engineering, Special Purpose and Application-Based Systems},
  Language                 = {en},
  Url                      = {http://link.springer.com/chapter/10.1007/3-540-52148-8_17},
  Urldate                  = {2014-11-26}
}

@Article{Bou_Forward_Analysis2,
  author="Bouyer, Patricia",
  title="Forward Analysis of Updatable Timed Automata",
  journal="Formal Methods in System Design",
  volume="24",
  number="3",
  pages="281--320",
  abstract="Timed automata are a widely studied model. Its decidability has been proved using the so-called region automaton construction. This construction provides a correct abstraction for the behaviours of timed automata, but it suffers from a state explosion and is thus not used in practice. Instead, algorithms based on the notion of zones are implemented using adapted data structures like DBMs. When we focus on forward analysis algorithms, the exact computation of all the successors of the initial configurations does not always terminate. Thus, some abstractions are often used to ensure termination, among which, a widening operator on zones.",
  issn="1572-8102",
  doi="10.1023/B:FORM.0000026093.21513.31",
  url="https://doi.org/10.1023/B:FORM.0000026093.21513.31"
}

@article{Bou_Forward_Analysis,
  author    = {Patricia Bouyer},
  title     = {Forward Analysis of Updatable Timed Automata},
  journal   = {Formal Methods in System Design},
  volume    = {24},
  number    = {3},
  pages     = {281--320},
  year      = {2004},
  url       = {https://doi.org/10.1023/B:FORM.0000026093.21513.31},
  doi       = {10.1023/B:FORM.0000026093.21513.31},
  timestamp = {Wed, 25 May 2011 16:32:09 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/fmsd/Bouyer04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{Bou_Updatable,
  author    = {Patricia Bouyer and
               Catherine Dufourd and
               Emmanuel Fleury and
               Antoine Petit},
  title     = {Are Timed Automata Updatable?},
  booktitle = {Computer Aided Verification, 12th International Conference, {CAV}
               2000, Chicago, IL, USA, July 15-19, 2000, Proceedings},
  pages     = {464--479},
  year      = {2000},
  url       = {https://doi.org/10.1007/10722167_35},
  doi       = {10.1007/10722167_35},
  timestamp = {Tue, 21 Jun 2011 16:38:39 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/BouyerDFP00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@Inbook{Bou_Untameable,
  author="Bouyer, Patricia",
  editor="Alt, Helmut
  and Habib, Michel",
  chapter="Untameable Timed Automata!",
  title="STACS 2003: 20th Annual Symposium on Theoretical Aspects of Computer Science Berlin, Germany, February 27 -- March 1, 2003 Proceedings",
  year="2003",
  publisher="Springer Berlin Heidelberg",
  address="Berlin, Heidelberg",
  pages="620--631",
  isbn="978-3-540-36494-8",
  doi="10.1007/3-540-36494-3_54",
  url="https://doi.org/10.1007/3-540-36494-3_54"
}

@Article{Larsen1997,
  author="Larsen, G. Kim
  and Pettersson, Paul
  and Yi, Wang",
  title="Uppaal in a nutshell",
  journal="International Journal on Software Tools for Technology Transfer",
  year="1997",
  volume="1",
  number="1",
  pages="134--152",
  issn="1433-2779",
  doi="10.1007/s100090050010",
  url="https://doi.org/10.1007/s100090050010"
}

@Article{Henzinger97hytech,
    author = {Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-toi},
    title = {HyTech: A Model Checker for Hybrid Systems},
    journal = {Software Tools for Technology Transfer},
    year = {1997},
    volume = {1},
    pages = {460--463}
}

@inproceedings{Chronos95,
  author    = {Conrado Daws and
               Alfredo Olivero and
               Stavros Tripakis and
               Sergio Yovine},
  title     = {The Tool {KRONOS}},
  booktitle = {Hybrid Systems {III:} Verification and Control, Proceedings of the
               {DIMACS/SYCON} Workshop, October 22-25, 1995, Ruttgers University,
               New Brunswick, NJ, {USA}},
  pages     = {208--219},
  year      = {1995},
  url       = {https://doi.org/10.1007/BFb0020947},
  doi       = {10.1007/BFb0020947},
  timestamp = {Wed, 15 Jun 2011 15:38:51 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hybrid/DawsOTY95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{Kronos97,
  author    = {Sergio Yovine},
  title     = {{KRONOS:} {A} Verification Tool for Real-Time Systems},
  journal   = {{STTT}},
  volume    = {1},
  number    = {1-2},
  pages     = {123--133},
  year      = {1997},
}

@inproceedings{BengtssonY03,
  author    = {Johan Bengtsson and
               Wang Yi},
  title     = {Timed Automata: Semantics, Algorithms and Tools},
  booktitle = {Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This
               tutorial volume originates from the 4th Advanced Course on Petri Nets,
               {ACPN} 2003, held in Eichst{\"{a}}tt, Germany in September 2003.
               In addition to lectures given at {ACPN} 2003, additional chapters
               have been commissioned]},
  pages     = {87--124},
  year      = {2003},
  url       = {https://doi.org/10.1007/978-3-540-27755-2_3},
  doi       = {10.1007/978-3-540-27755-2_3},
  timestamp = {Fri, 07 Dec 2012 11:52:52 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ac/BengtssonY03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}