"Temporal Logic for Verification of Reactive Systems: Achievements and Challenges"

Last year (1997) marked the 20th anniversary of the introduction of Temporal Logic (TL) into Computer Science as a language proposed for the specification and verification of Reactive Systems.

The talk will present a personal view of the main contributions and achievements of TL over the last two decades, emphasizing the recent increase of acceptance and adoption of the temporal methodology by industry, and the extensions of the formalism to deal with real-time and hybrid systems. We will then proceed to identify future challenges and directions that may extend the applicability of TL to wider classes of systems and the treatment of ever larger designs.