This paper introduces timed Büchi automata (TBA) for modeling finite-state asynchronous real-time systems. TBAs combine Büchi automata with a mechanism to express constant bounds on timing delays between events. They accept languages of timed traces, where each event has a real-valued time of occurrence. The class of languages accepted by TBAs is closed under union, intersection, and projections, and the projected trace language is ω-regular. However, TBAs are not closed under complement, and it is undecidable whether one TBA's language is a subset of another. This makes automatic verification challenging. A proper subclass, deterministic timed Muller automata (DTMA), is closed under all boolean operations, enabling automatic verification of systems modeled by TBAs against specifications given as DTMA. The paper discusses the need for formalisms for quantitative temporal reasoning in real-time systems, which must meet hard real-time constraints. Previous approaches used discrete-time models or fictitious clocks, but these are inaccurate for precise timing. The paper proposes a model using a dense domain for time, allowing unbounded environment events between system events and more accurate modeling of timing delays. Timed automata are defined as ω-automata with clocks to record time. Clocks can be reset with state transitions, and timing constraints are expressed by comparing clock values with time constants. Timed automata accept timed traces, sequences with real-valued times. The paper shows that the class of languages accepted by TBAs is closed under intersection and projections, enabling effective constructions for operations like parallel composition. The paper also defines determinism for timed automata and shows that deterministic timed automata can be complemented. This allows the use of timing information to verify qualitative temporal requirements. However, the language inclusion problem is undecidable, posing challenges for automatic verification of real-time requirements. The paper contributes to the development of formalisms for quantitative temporal reasoning in real-time systems.This paper introduces timed Büchi automata (TBA) for modeling finite-state asynchronous real-time systems. TBAs combine Büchi automata with a mechanism to express constant bounds on timing delays between events. They accept languages of timed traces, where each event has a real-valued time of occurrence. The class of languages accepted by TBAs is closed under union, intersection, and projections, and the projected trace language is ω-regular. However, TBAs are not closed under complement, and it is undecidable whether one TBA's language is a subset of another. This makes automatic verification challenging. A proper subclass, deterministic timed Muller automata (DTMA), is closed under all boolean operations, enabling automatic verification of systems modeled by TBAs against specifications given as DTMA. The paper discusses the need for formalisms for quantitative temporal reasoning in real-time systems, which must meet hard real-time constraints. Previous approaches used discrete-time models or fictitious clocks, but these are inaccurate for precise timing. The paper proposes a model using a dense domain for time, allowing unbounded environment events between system events and more accurate modeling of timing delays. Timed automata are defined as ω-automata with clocks to record time. Clocks can be reset with state transitions, and timing constraints are expressed by comparing clock values with time constants. Timed automata accept timed traces, sequences with real-valued times. The paper shows that the class of languages accepted by TBAs is closed under intersection and projections, enabling effective constructions for operations like parallel composition. The paper also defines determinism for timed automata and shows that deterministic timed automata can be complemented. This allows the use of timing information to verify qualitative temporal requirements. However, the language inclusion problem is undecidable, posing challenges for automatic verification of real-time requirements. The paper contributes to the development of formalisms for quantitative temporal reasoning in real-time systems.