Temporal Assertions with Parametrized Propositions
Journal of Logic and Computation2008Vol. 20(3), pp. 743–757
Citations Over TimeTop 15% of 2008 papers
Abstract
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.
Related Papers
- → Alternating-time temporal logic(2002)313 cited
- → Regular Linear Temporal Logic(2007)60 cited
- → SEQUENCE-INDEXED LINEAR-TIME TEMPORAL LOGIC: PROOF SYSTEM AND APPLICATION(2010)13 cited
- → Temporal logic control of discrete-time piecewise affine systems(2009)10 cited
- → Temporal Logic Model Checking via Probe Machine(2020)1 cited