clarke@csri.toronto.edu (Jim Clarke) (01/02/89)
COLLOQUIUM - Tuesday, January 10, 11 a.m. in Room SF 1105 (SF = Sandford Fleming Building, 10 King's College Road) Amir Pnueli The Weizmann Institute of Science "Specification and Verification of Reactive Systems by Temporal Logic" We will survey the application of temporal logic to the specification and verification of reactive systems, i.e., systems whose role is to maintain some ongoing interaction with their environment, rather than to produce some final result. The talk will introduce the abstract computational model of Fair Transition System, and the language of temporal logic, including the past operators. We will briefly discuss a hierarchical classification of the properties expressible by temporal logic, and illustrate the type of properties falling in each class. Then, we will mention the main methods of verifying that a given program satisfies a certain property, showing the proof principles appropriate to each class. If time permits, we will also mention alternative formalisms such as predicate automata, and touch upon the extensions necessary for reasoning about real time. -- Jim Clarke -- Dept. of Computer Science, Univ. of Toronto, Canada M5S 1A4 (416) 978-4058 BITNET,CSNET: clarke@csri.toronto.edu CDNNET: clarke@csri.toronto.cdn UUCP: {allegra,cornell,decvax,linus,utzoo}!utcsri!clarke