The paper introduces the concept of *timed Büchi automata* (TBAs) to model the behavior of finite-state asynchronous real-time systems. TBAs are extended Büchi automata that can express constant bounds on timing delays between system events, accepting languages of *timed traces* where each event has an associated real-valued time of occurrence. The authors demonstrate that the class of languages accepted by TBAs is closed under union, intersection, and projections, but not under complementation, making the language inclusion problem undecidable. However, a significant subclass, *deterministic timed Muller automata* (DTMA), is closed under all boolean operations, allowing for automatic verification of systems modeled by TBAs against specifications given as DTMA. The paper also discusses the limitations of previous approaches to modeling real-time systems and proposes a more accurate and flexible model using timed automata.The paper introduces the concept of *timed Büchi automata* (TBAs) to model the behavior of finite-state asynchronous real-time systems. TBAs are extended Büchi automata that can express constant bounds on timing delays between system events, accepting languages of *timed traces* where each event has an associated real-valued time of occurrence. The authors demonstrate that the class of languages accepted by TBAs is closed under union, intersection, and projections, but not under complementation, making the language inclusion problem undecidable. However, a significant subclass, *deterministic timed Muller automata* (DTMA), is closed under all boolean operations, allowing for automatic verification of systems modeled by TBAs against specifications given as DTMA. The paper also discusses the limitations of previous approaches to modeling real-time systems and proposes a more accurate and flexible model using timed automata.