Linear Temporal Logic

ESBMC can check linear temporal logic properties — including liveness properties such as “whenever the button is pressed, the charge eventually exceeds the minimum” — over unmodified C programs. The approach is described in [1] and [4]: the negated formula is translated to a Büchi automaton, the automaton is emitted as a C monitor thread, and ESBMC checks the monitor interleaved with the program under analysis. Because bounded model checking explores only finite prefixes, the verdict is drawn from a four-valued lattice rather than true/false.

This page documents what the --ltl path does in ESBMC 8.4.0, including where the implementation diverges from [1].

Warning: LTL is a legacy, lightly maintained path. The missed-violation bug of #6546 is fixed, but the fix needs a libltl2ba built from master — the tagged v2.1 release does not contain it, and a monitor generated by v2.1 yields no verdict at all under ESBMC 8.4.0. Read Limitations before relying on any of it.

At a glance

The four-valued verdict

Standard LTL is interpreted over infinite traces, but a bounded model checker explores finite ones. ESBMC therefore evaluates the formula under the bounded trace semantics of [1, Def. 2], built on the four-valued deMorgan lattice {⊥, ⊥ᵖ, ⊤ᵖ, ⊤} of [2]. A finite prefix is stutter-extended — its final state repeated forever — and the verdict records whether every, some, or no infinite continuation satisfies the formula φ.

The lattice order is ⊥ ⊑ ⊥ᵖ ⊑ ⊤ᵖ ⊑ ⊤. ESBMC checks each interleaving separately and reports the least value seen across all of them (src/esbmc/bmc.cpp:1762), which is why the log line reads Final lowest outcome:.

For a liveness formula, ⊤ is generally unreachable: no finite prefix of G(p -> F q) can rule out a later violation, so the best attainable verdict is ⊤ᵖ [1, §7.1]. A LTL_SUCCEEDING result on a liveness property is therefore the expected success outcome, not a near-miss.

Checking an LTL property

1. Translate the negated formula

Build libltl2ba — ESBMC’s fork of ltl2ba [3], extended with a C output format — from master, and emit the monitor for the negation of the property you want to hold:

ltl2ba -O c -f '!(G({pressed} -> F {charge > min}))' > notphi.c

Note the negation: the automaton is a Spin-style never claim, so what you hand to ltl2ba is the complement of the property, and the reported verdict is about the property. Feeding !(φ) for a φ that holds yields ⊤ᵖ; feeding !(φ) for a φ that fails yields ⊥ᵖ.

C expressions over the program’s global variables are written inside curly brackets and act as the atomic propositions; they must be side-effect free and evaluate to something usable as a truth value.

Operators

All five LTL temporal operators are accepted, in both their letter and ASCII-art spellings:

Propositional syntax is true, false, {C expression}, a lowercase identifier, !, && (or /\), || (or \/), -> and <->. Precedence, highest first, is U/V (right-associative), &&, ||, <->, ->; unary operators bind tighter than binary ones, and libltl2ba wants spaces between symbols. See its README for the full grammar.

X is the one to be careful with. Its intended reading here is “φ holds after the next update of a global variable used in the propositions” [1, §3.1], which relies on the monitor being stepped at each such update — the directed scheduling restored in #6561. That backs X only for the updates the instrumentation actually sees, so the assignment forms it skips are invisible to it. [1, §3.2] recommends X-free, stutter-invariant formulas in any case, since X is awkward to interpret over finite traces at all.

The generated file contains one pure C accessor per proposition, plus a char __ESBMC_property_*[] marker that tells ESBMC which functions to treat as propositions:

char __ESBMC_property__ltl2ba_cexpr_0[] = "pressed";
int _ltl2ba_cexpr_0_status(void) { return pressed; }
char __ESBMC_property__ltl2ba_cexpr_1[] = "charge > min";
int _ltl2ba_cexpr_1_status(void) { return charge > min; }

2. Declare the variables the propositions read

libltl2ba does not know the types of the program’s globals, so the generated file needs declarations for them. Put them in a header:

extern int pressed;
extern int charge, min;

and have libltl2ba #include it directly with -H:

ltl2ba -O c -H '"tau.h"' -f '!(G({pressed} -> F {charge > min}))' > notphi.c

Alternatively, add the extern declarations to notphi.c by hand, or leave the header out of the monitor and pass it to ESBMC with --include-file:

esbmc program.c --ltl notphi.c --include-file tau.h -DLTL_PREFIX_BOUND=10

3. Run ESBMC

esbmc program.c --ltl notphi.c -DLTL_PREFIX_BOUND=10

LTL_PREFIX_BOUND bounds the monitor’s own transition loop. Its default of 2147483648 is not tractable — a run left at the default does not finish — so pass an explicit bound. libltl2ba emits an assert(num_iters == iters, "Unwind bound on ltl2ba_fsm insufficient") to catch a bound that is too small, but --ltl masks that assertion along with every other non-LTL property, so an inadequate bound is not reported.

Taking regression/ltl/basic as the worked example — a program that presses the button twice but only tops up the charge when pressed:

int pressed, charge, min;

int main()
{
	charge = nondet_int();
	min = nondet_int() % 1024;
	for (int i = 0; i < 2; i++) {
		pressed = nondet_int();
		if (pressed)
			charge = min + 1;
	}
}

ESBMC reports:

Checking for LTL_BAD
WARNING: Couldn't find LTL_BAD assertion
Checking for LTL_FAILING
Found trace satisfying LTL_FAILING
...
Final lowest outcome: LTL_FAILING

VERIFICATION FAILED

⊥ᵖ is the correct answer: the loop can exit with pressed true and charge not yet topped up, and stuttering that final state forever violates F {charge > min} — but a longer trace could still satisfy it. The ⊥ᵖ verdict maps onto the process result, so the run prints the satisfying trace as a [Counterexample] and exits non-zero.

How it works

Given the program and the generated monitor, ESBMC:

1. Finds the propositions. add_property_monitors (src/esbmc/parseoptions/property_monitors.cpp:20) scans the symbol table for __ESBMC_property_<name> markers and, for each, extracts the returned expression from the matching <name>_status function.
2. Makes proposition updates atomic. Every assignment whose target is one of the globals a proposition reads is wrapped in ATOMIC_BEGIN / ATOMIC_END (property_monitors.cpp:162), so the monitor cannot observe a half-updated state.
3. Starts and stops the monitor. Calls to ltl2ba_start_monitor and ltl2ba_finish_monitor are injected at the top of the entry function and before each of its return instructions (property_monitors.cpp:97). ltl2ba_start_monitor spawns the automaton as a pthread and registers it via the __ESBMC_register_monitor intrinsic (src/goto-symex/symex_main.cpp:609).
4. Explores the automaton symbolically. The monitor keeps the current automaton state in a single nondeterministic-but-constrained integer, with each transition guarded by __ESBMC_assume. The automaton is never determinised; the solver explores the alternatives [1, §6.2.1].
5. Evaluates the prefix at the end. ltl2ba_finish_monitor kills the monitor and asserts three properties against the precomputed reachability tables _ltl2ba_bad_prefix_states, _ltl2ba_stutter_accept_table and _ltl2ba_good_prefix_excluded_states, labelled LTL_BAD, LTL_FAILING and LTL_SUCCEEDING.
6. Solves once per lattice level. bmct::ltl_run_thread (src/esbmc/bmc.cpp:2122) first checks the monitor’s preconditions — every assertion that is not a prefix assertion, so unwinding assertions and libltl2ba’s own bound guard included — and yields no verdict if any can be violated, since a truncated automaton supports no prefix claim. It then masks all but one of the three prefix assertions and runs a separate solver call for each, from ⊥ upwards, returning the first level for which a trace exists. If none is satisfiable it returns LTL_GOOD, or no verdict when no prefix assertion was present to prove.

Two smaller accommodations: the context-switch threshold is raised from 2 to 3 under --ltl (src/goto-symex/execution_state.cpp:106), and the assertion cache is disabled (src/esbmc/bmc.cpp:118) because the LTL assertions are re-checked with different maskings.

Limitations

Note: Everything below was reproduced against ESBMC 8.4.0 paired with libltl2ba at b810033. The --ltl path has no dedicated issue label.

Violations were missed (fixed in 8.4.0)

Until the directed monitor scheduling described under Divergences from the published algorithm was enabled, the monitor did not observe updates to the globals its propositions read, so a property that is definitively violated was reported as ⊤ᵖ, “presumably true” (#6546). For a program that assigns s = 1:

int s;

int main()
{
	s = 0;
	s = 1;
	s = 0;
	return 0;
}

the property G {s == 0} is definitively false — once s is 1 no continuation repairs a G — so the verdict should be ⊥. Instead:

ltl2ba -O c -H '"tau.h"' -f 'F {s != 0}' > safety.c
esbmc prog.c --ltl safety.c -DLTL_PREFIX_BOUND=6

Final lowest outcome: LTL_BAD

which is the expected ⊥. This case is pinned by regression/ltl/github_6546.

Before the fix the same run reported LTL_SUCCEEDING: the generated automaton does have a reachable bad-prefix state, but with the monitor free-running as an ordinary thread no interleaving was guaranteed to sample the state at the moment a proposition changed, and raising LTL_PREFIX_BOUND, --context-bound or --unwind did not help.

A monitor emitted by a libltl2ba older than #4 — including the v2.1 tag — emits __ESBMC_switch_to_monitor() and __ESBMC_switch_from_monitor() commented out. Since the monitor is never scheduled the ordinary way, such a monitor never steps at all, and every run reports VERIFICATION UNKNOWN rather than a wrong verdict. If a formula that should decide keeps coming back without a verdict, check the generated file for those two calls first.

Note that the monitor now advances one automaton step per monitored assignment, so a program has to be long enough for the automaton to reach a decisive state. A run too short for that leaves every path infeasible and produces no verdict — regression/ltl/basic-func and basic-success needed a second loop iteration for this reason, and an explicit --unwind bound has to cover the monitor’s steps as well as the program’s.

A missing assertion reports VERIFICATION UNKNOWN

“Not instrumented” and “definitively correct” are different answers, and only the second is ⊤. ltl_run_thread yields no verdict rather than LTL_GOOD when it finds no prefix assertion to prove, so one uninformative formula downgrades the whole run to VERIFICATION UNKNOWN instead of being reported as ⊤ (#6547). Three situations trigger it:

• --ltl with no monitor file. Warns No LTL outcome seen; the property was not checked and reports VERIFICATION UNKNOWN.
• A program that leaves main other than by returning. exit() and abort() bypass the injected ltl2ba_finish_monitor call, because it is only placed before return instructions. Every VCC is then simplified away and no prefix verdict is reached, so the run reports VERIFICATION UNKNOWN.
• An incompatible strategy — see below.

Do not combine --ltl with another strategy

--ltl is only meaningful for a plain single-shot BMC run. On regression/ltl/basic, whose correct verdict is ⊥ᵖ:

These combinations yield no verdict rather than a wrong one. The k-induction and incremental drivers restructure the program per iteration, so the automaton no longer runs to completion; an --unwind bound that is too small has the same effect, because the bound applies to the monitor’s transition loop as well as the program’s. Either way the monitor’s precondition check fails and the run reports VERIFICATION UNKNOWN. k-induction additionally logs k-induction does not support concurrency yet. Disabling inductive step, because the monitor is a thread.

Use plain --ltl, or --ltl --unwind N with an N large enough that the preconditions hold, if you want an actual verdict.

Other properties are masked

To isolate one lattice level at a time, ltl_run_thread masks every assertion that is not the one it is currently seeking into a SKIP. That includes all the ordinary ones: bounds and NULL checks, overflow checks, and user asserts. An --ltl run therefore still reports nothing about safety per se.

It does check them collectively: the precondition pass solves the equation with only the non-prefix assertions enabled, so a violated unwinding assertion or libltl2ba’s "Unwind bound on ltl2ba_fsm insufficient" guard downgrades the run to VERIFICATION UNKNOWN instead of being silently discarded. What it does not do is tell you which one failed. Re-running the same command without --ltl does:

✗ FAILED: 'unwinding assertion loop 3 at file notphi.c line 131 column 2 function ltl2ba_fsm'
✗ FAILED: 'unwinding assertion loop 4 at file program.c line 7 column 2 function main'

Check safety properties and bound adequacy in a separate run without --ltl.

Divergences from the published algorithm

• The dedicated monitor scheduler is enabled (it was disabled between commit 4146a8e387 and the fix for #6546). [1, §6.2.3] replaces general-purpose scheduling of the monitor with a directed context switch to it after each global-variable update, reported there as the change that made the analysis practical. Reviving it needed the __ESBMC_switch_to_monitor insertion in property_monitors.cpp and libltl2ba emitting the paired __ESBMC_switch_from_monitor() at the end of each automaton step (without it the monitor thread runs its whole prefix in one go and ends). The monitor is kept off the ordinary scheduler by check_thread_viable, and interleaving is blocked for the duration of a directed step so it cannot be abandoned half-way (#6585); the program’s own threads interleave normally, which the verdict is a minimum over [1, §7.2].
• Propositions are re-evaluated, not cached. [1, §6.2.2] describes inserting an update to a Boolean variable per proposition after each assignment. The current code only makes the assignment atomic; the automaton calls _ltl2ba_cexpr_N_status() directly each time it needs a proposition. This replaced an earlier scheme that stored the propositions as strings for ESBMC to parse, which the frontends no longer support.
• Only direct assignments to a named global are monitored. add_monitor_exprs returns immediately unless the assignment target is a plain symbol (property_monitors.cpp:182), so a write through a pointer, to an array element, or to a struct member does not count as a proposition update. This limitation is acknowledged in [1, §6.2.2].
• ⊤ᵖ is reported as a successful verification. [1, §6.2.1] reports only a good prefix (⊤) as success and every other classification as an assertion failure. ESBMC maps ⊤ᵖ to VERIFICATION SUCCESSFUL as well, since ⊤ is generally unreachable for a liveness formula [1, §7.1] and a run that reported every liveness property as failing would be useless.

Other restrictions

• C only. The property-monitor machinery keys on C symbol names (c:@F@<name>_status) and the monitor is a C file; no other frontend is wired up.
• ltl2ba is not bundled. libltl2ba must be built and installed separately, and from master — the newest tagged release, v2.1 (April 2024), predates the context-switch emission this version of ESBMC requires. Nothing checks the pairing, and the resulting VERIFICATION UNKNOWN does not name the cause.
• Test coverage is thin. regression/ltl/ holds eleven tests. The two automata shipped by the original three exercise only ⊥ᵖ, ⊤ᵖ and the no-verdict cases, because both formulas have an empty bad-prefix state set and mark every state as excluded from being a good prefix; github_6546 covers LTL_BAD. LTL_GOOD is still uncovered.
• Multi-threaded liveness checking remains practical only for small programs [1, §7.2]: liveness needs enough interleavings for every thread to complete whole loop iterations, whereas safety violations are typically shallow. The interleaving count climbs steeply — two program threads reach 34 schedules and three reach 366 on the regression/ltl/multithreaded* programs. Bound it with --context-bound, not --direct-interleavings, which suppresses the program’s own interleavings and re-creates #6585.

Checking the prefix assertions individually

The instrumentation is driven by the __ESBMC_property_* markers in the monitor file, not by --ltl (src/esbmc/parseoptions/process_goto_program.cpp:458). Passing the monitor without --ltl therefore checks the three prefix assertions as ordinary assertions, which gives per-claim results — useful when you want to see every lattice level at once rather than only the lowest.

esbmc program.c notphi.c -DLTL_PREFIX_BOUND=10 --multi-property

✓ PASSED: 'LTL_BAD at file notphi.c line 241 ...'
✗ FAILED: 'LTL_FAILING at file notphi.c line 243 ...'
✗ FAILED: 'LTL_SUCCEEDING at file notphi.c line 245 ...'

VERIFICATION FAILED

The lowest failing claim in the order LTL_BAD → LTL_FAILING → LTL_SUCCEEDING is the lattice verdict, and all three passing means ⊤. This reproduces the --ltl outcome on each of the shipped tests — LTL_FAILING for basic and basic-func, LTL_SUCCEEDING for basic-success. Without --multi-property ESBMC stops at the first violated assertion, which need not be the lowest one, so the exit code is usable but the reported claim is not the verdict.

Regression tests

All but one check the property G({pressed} -> F {charge > min}), or its negation, against the same small program; github_6546 checks G {s == 0} against the program in Limitations.

All eleven are CORE and pass:

ctest -R "regression/ltl/" --output-on-failure

Each pins the process verdict, and where one is produced, the Final lowest outcome: line or the warning that identifies why no verdict was reached.

References

[1] Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer: Model checking LTL properties over ANSI-C programs with bounded traces. Software and Systems Modeling 14(1):65–81, 2015. doi:10.1007/s10270-013-0366-0

[2] Andreas Bauer, Martin Leucker, Christian Schallhart: Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation 20(3):651–674, 2010. doi:10.1093/logcom/exn075

[3] Paul Gastin, Denis Oddoux: Fast LTL to Büchi Automata Translation. CAV 2001, LNCS 2102: 53–65. doi:10.1007/3-540-44585-4_6

[4] Jeremy Morse: Expressive and efficient bounded model checking of concurrent software. PhD thesis, University of Southampton, 2015. PDF