Reference · Algorithm guarantees

rainbow.algorithms.proofs.robustness-objective

Algorithm guaranteessrc/rainbow/algorithms/proofs/robustness_objective.clj1 definitions, 2 theorems

The robustness-based falsification objective over signed rationals. Signal temporal logic robustness is positive when a trajectory satisfies a specification and negative when it violates it. The falsification objective negates the robustness, so a satisfying trajectory has a negative objective and a violating trajectory has a positive one -- maximizing the objective drives the search toward the most-violating trajectory (AHoF V13). Negating twice recovers the robustness, so the objective loses no information.

validation/falsification-objective :
  (x₁ : ℚ)
  → ℚ

validation/falsification-objective-unfold :
  (robustness : ℚ)
  → validation/falsification-objective robustness = signed/negate robustness

validation/falsification-objective-involution :
  (robustness : ℚ)
  → validation/falsification-objective (validation/falsification-objective robustness) = robustness