In this chapter, the authors discuss a number of formal tools collectively driving them to Hybrid Automata. Automata have a long and rich history in computer science, and they have been used in a variety of ways to render (formally) many basic and natural ideas. The authors introduce first-order languages and theories, and report on some decidability results over them. They also discuss possible usages of the simple formalism of finite state automata. A possible way to model real-world systems is to abstract all the quantitative part of their evolution and exclusively focus on the sequences of discrete events that they produce and that led to some outcome. The authors focus their attention on the use of hybrid automata for modelling quite "simple" biological systems. They also introduce the two final "ingredients" of their discussion: Time and Uncertainty. The initial time instants of simple, finite-state automata models are defined by the occurrence of events.
