zbMATH — the first resource for mathematics

Temporal assertions with parametrized propositions. (English) Zbl 1203.68103
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.

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI