VERIFICATION USING TIMED AUTOMATA Finite automata and temporal logics have been used extensively to formally verify qualitative properties of concurrent systems. The properties include deadlock- or livelock-freedom, the eventual occurrence of an event, and the satisfaction of a predicate. The need to reason with absolute time is unnecessary in these applications, whose correctness depends only on the relative ordering of the associated events and actions. These automata-theoretic and temporal lo