Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
On the Merits of Temporal Testers
verfasst von : A. Pnueli, A. Zaks
Erschienen in: 25 Years of Model Checking
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The paper discusses the merits of
temporal testers
, which can serve as a compositional basis for automata construction corresponding to temporal formulas in the context of
ltl
,
psl
, and
mitl
logics. 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 asBüchi automata) is their compositionality. Namely, a tester for a compound formula can be constructed out of the testers for its sub-formulas. Besides providing the construction of testers for formulas specified in
ltl
,
psl
, and
mitl
, the paper also presents a general overview of the tester methodology, and highlights some of the unique features and applications of transducers including compositional deductive verification of
ltl
properties.