Temporal Verification of Reactive Systems

The family of reactive systems includes many classes of programs whose correct and reliable construction is con sidered to be particularly challenging, including concurrent programs, embedded and process control programs, and operating systems.