@inproceedings{FORMATS '07: Undecidability of Universality for Timed Automata with Minimal Resources,
  abstract = "Timed automata were introduced by Alur and Dill in the early 1990s and have since become the most prominent modelling formalism for real-time systems. A fundamental limit to the algorithmic analysis of timed automata, however, results from the undecidability of the universality problem: does a given timed automaton accept every timed word? As a result, much research has focussed on attempting to circumvent this difficulty, often by restricting the class of automata under consideration, or by altering their semantics. In this paper, we study the decidability of universality for classes of timed automata with minimal resources. More precisely, we consider restrictions on the number of states and clock constants, as well as the size of the event alphabet. Our main result is that universality remains undecidable for timed automata with a single state, over a single-event alphabet, and using no more than three distinct clock constants.",
  author = "Sara Adams and Joel Ouaknine and James Worrell",
  booktitle = "Formal Modeling and Analysis of Timed Systems 2007",
  isbn = "978-3-540-75453-4",
  pages = "25-37",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  title = "Undecidability of Universality for Timed Automata with Minimal Resources",
  url = "http://www.sara-adams.de/files/formats07.pdf",
  volume = "4763",
  year = "2007",
}


    
      @inproceedings{FMCAD '07: Automatic Abstraction in STE,
  abstract = "Symbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single model-checking run. This provides a flexible way to achieve partitioned data abstraction. It is usually called `symbolic indexing' and is widely used in memory verification, but has seen relatively limited adoption elsewhere, primarily because users typically have to create the right indexed family of abstractions manually. This work provides the first known algorithm that automatically computes these partitioned abstractions given a reference-model specification. Our experimental results show that this approach not only simplifies memory verification, but also enables handling completely different designs fully automatically.",
  author = "Sara Adams and Magnus Bj�rk and Tom Melham and Carl-Johan Seger",
  booktitle = "FMCAD '07: Proceedings of the 7th International Conference on Formal Methods in Computer Aided Design",
  isbn = "0-7695-3023-0",
  pages = "127--135",
  publisher = "IEEE Computer Society",
  title = "Automatic Abstraction in Symbolic Trajectory Evaluation",
  url = "http://www.sara-adams.de/files/fmcad07.pdf",
  year = "2007",
}


    
      @misc{MSc Thesis: On the Undecidability of Universality for Timed Automata with Minimal Resources,
  abstract = "In 1994 Alur and Dill introduced timed automata and showed that universality was undecidable there. Since then it has been shown that under certain restrictions the problem becomes decidable. But the frontier between decidability and undecidability is still vast. We aim at narrowing this gap considerably. Our main accomplishment is to prove that universality stays undecidable over weakly monotonic time when restricting to a single state, a single symbol and clock comparisons to 0 and 1 only. We further propose that over strongly monotonic time the problem stays undecidable for timed automata with one state and one symbol only.",
  affiliation = "University of Oxford",
  author = "Sara Adams",
  howpublished = "MSc Thesis",
  title = "On the Undecidability of Universality for Timed Automata with Minimal Resources",
  url = "http://www.sara-adams.de/files/dissertation.pdf",
  year = "2006",
}