[ont.events] U of Toronto Computer Science colloquium, January 10

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