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.