Temporal assertions with parametrized propositions. (English) Zbl 1203.68103

Stolz, Volker

J. Log. Comput. 20, No. 3, 743-757 (2010).

Summary: We extend our previous approach to run-time verification of a single finite path against a formula in next-free Linear-Time Logic (LTL) with free variables and quantification. We discuss the design space of quantification and introduce a binary operator that binds values based on the current state. The binding semantics of propositions containing quantified variables is a pure top-down evaluation. The alternating binding automaton corresponding to a formula is evaluated in a breadth-first manner, allowing us to detect refuted formulae during execution.

MSC:

68Q60

Specification and verification (program logics, model checking, etc.)

Keywords:

run-time verification; Linear-Time Logic; alternating binding automaton