Temporal Assertions with Parametrized Propositions
|Title||Temporal Assertions with Parametrized Propositions|
|Publication Type||Journal Article|
|Year of Publication||2010|
|Journal||Journal of Logic and Computation|
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.