Title: PSL Model Checking and Run-time Verification via Testers 


Authors: Amir Pnueli and Aleksandr Zaks

The paper introduces the construct of \emm{temporal
testers} as a compositional basis for the construction
of automata corresponding to temporal formulas in the
PSL logic. Temporal testers can be viewed as
(non-deterministic) transducers that, at any point,
output a boolean value which is 1 iff the
corresponding temporal formula holds starting at the
current position.

The main advantage of testers, compared to acceptors
(such as Buchi automata) is that they are
compositional. Namely, a tester for a compound formula
can be constructed out of the testers for its
sub-formulas. In this paper, we extend the application
of the testers method from LTL to the logic PSL.

Besides providing the construction of testers for PSL,
we indicate how the symbolic representation of the
testers can be directly utilized for efficient model
checking and run-time monitoring.