# Temporal-logic falsification

Temporal-logic falsification searches for an input signal that drives a
system to break a requirement about its behavior *over time*. The
requirement is a temporal property: the temperature never exceeds a
limit, the output settles within two seconds of a setpoint change and
stays within a band, the brake response begins within a deadline. It is the
bug-finding dual of verification: the deliverable is a counterexample, not a
proof.

Its targets are control systems — an engine controller, an autopilot —
reached only as black boxes: a Simulink/Stateflow model, or a bench rig
with nonlinear dynamics and a learned component or two. There
is no tractable finite model to [model-check](https://quality.stereobooster.com/model-checking.md),
and the space of possible input signals is infinite, so proving the
requirement holds is out of reach. Where the Stateflow model is instead
white-box and finite, it can be formally verified or have tests generated
directly (see [state machines](https://quality.stereobooster.com/state-machines.md)).

## What it catches

- **Temporal-requirement violations that a point assertion cannot
  express.** Overshoot past a safety envelope, a settling time that
  misses its deadline, a transient spike that appears only under a
  specific input ramp. The requirement is a property of the whole
  trajectory, not of one output value.
- **Counterexamples as concrete, replayable input signals.** A
  falsifying run is an executable witness: the exact stimulus that made
  the system misbehave, ready to hand to a developer.
- **Failures in black-box and learned components** that formal
  verification cannot enter, because falsification only needs to *run*
  the system, not reason about its internals.

## Signal temporal logic

The requirement is written in **signal temporal logic** (STL), introduced
for monitoring continuous signals by Maler and Ničković (Maler and Ničković 2004)[^maler2004]. STL
combines atomic predicates over real-valued signals (`speed < 120`) with
boolean connectives and time-bounded temporal operators: `G[a,b]`
(*always* on the interval), `F[a,b]` (*eventually*), and `U[a,b]`
(*until*). An envelope requirement reads `G[0,30](https://quality.stereobooster.com/methods/domain/speed < 120)`; a
bounded-response requirement reads `G(brake → F[0,1](https://quality.stereobooster.com/methods/domain/decel > 0.5))`.
Unlike a plain assertion, STL states properties of behavior across an
interval of time, which is what control requirements actually are.

## Robustness: the quantitative semantics that makes search work

Boolean satisfaction gives an optimizer nothing to climb: almost every
input signal simply satisfies the property, a flat landscape with no
gradient. STL's decisive feature is a **robustness** semantics
(Fainekos and Pappas 2009)[^fainekos2009]: a real number that is positive when the signal satisfies
the requirement, with magnitude measuring the *margin*, and negative when
it violates, with magnitude measuring *how far* into violation. It is
defined recursively down the formula, a predicate `f(x) > 0` scoring
`f(x)`, conjunction becoming `min`, disjunction `max`, *always* an
infimum over its interval and *eventually* a supremum. Donzé and Maler
refined it with space and time robustness (Donzé and Maler 2010)[^donze2010].

Robustness turns falsification into **numeric optimization**: the search
drives the robustness below zero. That makes negative robustness a fitness
function and falsification a
[search-based test-generation](https://quality.stereobooster.com/search-based-software-testing.md)
problem.

## The search

Because the system is a black box and robustness is non-convex and
non-smooth, falsification uses **derivative-free global optimization**
over a finite-dimensional parameterization of the input signal (the
control points of a piecewise-constant or piecewise-linear input):
simulated annealing, CMA-ES, cross-entropy, and, when each simulation is
expensive, **Bayesian optimization** with a surrogate model to spend
simulations sparingly.

The recurring difficulty is that robustness can *mask* its own gradient:
the `min` and `inf` in a conjunctive, always-quantified requirement let a
comfortably-satisfied part hide a nearly-violated one. Alternative smooth
or cumulative robustness semantics are an active response to this.

## Tools and the benchmark

- [S-TaLiRo](https://github.com/cpslab-asu/PSY-TaLiRo) (Annpureddy et al. 2011)[^annpureddy2011] (originally MATLAB, now also
  a Python port) and [Breach](https://github.com/decyphir/breach) (MATLAB, Simulink-focused) are
  the two established tools; each monitors robustness and drives a
  falsification search, and Breach also does parameter synthesis.
- ARIsTEO layers surrogate modeling on S-TaLiRo for costly Simulink
  plants.
- Berkeley's VerifAI couples falsification to [Scenic](https://github.com/BerkeleyLearnVerify/Scenic)
  scenarios for systems with learned perception.
- The **ARCH-COMP falsification category** is an annual friendly
  competition that benchmarks these tools on shared models (automatic
  transmission, abstract fuel control, aircraft), the cyber-physical
  analogue of the verification competitions (Ernst et al. 2021)[^ernst2021].

## Where it sits among neighbors

- **The dual of [model checking](https://quality.stereobooster.com/model-checking.md).** Model
  checking proves no violation exists but needs a tractable model;
  falsification finds a violation and needs only to run the system.
  Reachability analysis (the over-approximating,
  [abstract-interpretation](https://quality.stereobooster.com/abstract-interpretation.md) style)
  is the sound counterpart that proves safety at the cost of conservatism.
- **Its oracle is a [runtime](https://quality.stereobooster.com/monitoring-and-observability.md)
  monitor.** Computing STL robustness over a trace is used offline inside
  the search and online as a runtime safety monitor; the
  Responsibility-Sensitive Safety envelope on the
  [autonomous-systems](https://quality.stereobooster.com/testing-autonomous-systems.md) page is a hand-built
  instance of exactly this.
- **A sibling of [fuzzing](https://quality.stereobooster.com/fuzzing.md) and
  [property-based testing](https://quality.stereobooster.com/property-based-testing.md).** All
  generate inputs to break a property; falsification's distinctive
  coordinates are that it generates continuous input *signals* and its
  oracle is a *quantitative temporal-logic* requirement over the
  resulting trajectory.

## When to use, when not

**Use:**

- **For reactive control and cyber-physical systems** whose requirements
  are temporal (deadlines, settling, envelopes), especially black-box
  Simulink plants and systems with learned components that formal
  verification cannot enter.
- **When a concrete failing input is worth more than a proof**, which is
  the usual case during development.
- **With a surrogate-model or Bayesian search** when each simulation is
  expensive.

**Don't:**

- **As a safety guarantee.** No counterexample found is not a proof; pair
  falsification with reachability analysis or model checking where a
  guarantee is required.
- **For requirements that are not temporal.** A stateless input-output
  check is a job for [example](https://quality.stereobooster.com/example-tests.md) or
  [property-based](https://quality.stereobooster.com/property-based-testing.md) tests; STL earns
  its cost when the property is about behavior over time.
- **Without attention to the robustness landscape.** A masked or flat
  robustness defeats a naive optimizer; the specification's shape, and
  the choice of semantics, decide whether the search converges.

## Evidence

- **Robustness semantics make falsification tractable**, converting a
  boolean pass/fail into an objective a black-box optimizer can minimize
  (Fainekos and Pappas 2009; Donzé and Maler 2010)[^fainekos2009] [^donze2010].
- **The tools falsify real requirements on shared benchmarks**, and the
  ARCH-COMP falsification reports track how reliably, across automotive
  and aerospace models (Ernst et al. 2021)[^ernst2021]. Effectiveness depends heavily on the
  input parameterization and the robustness landscape rather than being
  uniform across problems.
- **Scope.** Falsification is sound for finding bugs and silent on their
  absence. It reduces the uncertainty that a temporal requirement is
  violable; it does not certify that the requirement holds, and it checks
  only the requirements a person took the trouble to formalize.

## Classification

- **Quality dimensions:** Functionality (whether the system meets its temporal requirement), Reliability: safety (safety-envelope and robustness requirements that hold over time), Performance (signal temporal logic naturally encodes settling time, overshoot, and response-time bounds).
- **Area:** Cyber-physical, control, and hybrid systems with real-time temporal requirements: automotive and aerospace control (Simulink/Stateflow plants), medical devices, robotics, and any reactive system whose specification is about behavior over time.
- **Guarantee:** Empirical — a search for a counterexample; a falsifying trace is a real violation, but finding none is not a proof the requirement holds.

## Referenced by

- [Search-based software testing (SBST)](https://quality.stereobooster.com/search-based-software-testing.md) · Methods
- [Testing autonomous and cyber-physical systems](https://quality.stereobooster.com/testing-autonomous-systems.md) · Methods
- [Verifying safety-critical systems](https://quality.stereobooster.com/safety.md) · Methods
- [Conventional terminology](https://quality.stereobooster.com/terminology.md) · Conventional

## References

[^maler2004]: Maler, Oded, and Dejan Ničković. 2004. "[Monitoring Temporal Properties of Continuous Signals](https://www-verimag.imag.fr/~maler/Papers/monitor.pdf)." *Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (FORMATS/FTRTFT 2004)*, 152–66. [https://doi.org/10.1007/978-3-540-30206-3\\\_12](https://doi.org/10.1007/978-3-540-30206-3\_12).
[^fainekos2009]: Fainekos, Georgios E., and George J. Pappas. 2009. "[Robustness of Temporal Logic Specifications for Continuous-Time Signals](https://www.georgejpappas.org/wp-content/uploads/2024/04/TCS-FP09.pdf)." *Theoretical Computer Science* 410 (42): 4262–91. <https://doi.org/10.1016/j.tcs.2009.06.021>.
[^donze2010]: Donzé, Alexandre, and Oded Maler. 2010. "[Robust Satisfaction of Temporal Logic over Real-Valued Signals](https://www-verimag.imag.fr/~maler/Papers/sensiform.pdf)." *Formal Modeling and Analysis of Timed Systems (FORMATS 2010)*, 92–106. [https://doi.org/10.1007/978-3-642-15297-9\\\_9](https://doi.org/10.1007/978-3-642-15297-9\_9).
[^annpureddy2011]: Annpureddy, Yashwanth, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. 2011. "[S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems](https://link.springer.com/content/pdf/10.1007/978-3-642-19835-9_21.pdf)." *Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011)*, 254–57. [https://doi.org/10.1007/978-3-642-19835-9\\\_21](https://doi.org/10.1007/978-3-642-19835-9\_21).
[^ernst2021]: Ernst, Gidon, Paolo Arcaini, Georgios Fainekos, et al. 2021. "[ARCH-COMP 2021 Category Report: Falsification with Validation of Results](https://easychair.org/publications/open/F4kf)." *8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), EPiC Series in Computing* 80: 133–52. <https://doi.org/10.29007/xwl1>.

## Acronyms

- CMA-ES — covariance matrix adaptation evolution strategy
- SBST — search-based software testing
- STL — signal temporal logic