Invited talk from Amir Pnuel

Abstract: A central component in model checking temporal properties of systems is the translation of a temporal formula, expressing a property of interest, into a corresponding automaton. According to the standard translation, automaton A corresponds to Temporal formula f if the set of sequences accepted by A is precisely the set of sequences that satisfy f. This implies that the correspondence between A and f is required only at the initial position of each sequence.
In this talk we consider a stronger notion of translation, in which the automaton A_f, called the TEMPORAL TESTER of formula f, has a Boolean output variable x such that x=1 at position j of a sequence s iff (s,j) |= f. Thus, we can view a tester as a TRANSDUCER which, at any position in a behavior, tells us whether the formula f holds at that position. We will describe several advantages of the temporal tester construct. The construction of temporal testers is modular. That is, the temporal tester of a formula "f op g", where "op" can be any Boolean or temporal operator applied to arbitrary temporal formulas f and g, can be constructed by combining the temporal testers of f, g, and "op". As a result, we can outline a model-checking algorithm for LTL formulas which is compositional in the structure of the formula. This type of compositionality has been long considered to be a unique feature of CTL. Based on this approach to LTL model checking, we can obtain a compositional method for model-checking arbitrary CTL* formulas.
We will show how the notion of temporal testers is easily and naturally extended to deal with past formulas and many of the new operators introduced in the Hardware Property Specification language PSL. Another development, relevant to the workshop, is the use of temporal testers for the modular translation of Metric Interval Temporal Logic (MITL) formulas into Timed Automata.
The results for MITL have been obtained jointly with Oded Maler and Dejan Nickovic.