How SENTIL compares

The tools SENTIL is measured against fall into two families. RTAMT and Breach are runtime monitors: they take a recorded or streaming trace and compute an STL verdict or robustness. UPPAAL-SMC, PRISM, and Modest are statistical model checkers: they take a stochastic model and estimate the probability that a property holds over its runs. SENTIL spans both duties. It monitors PrSTL over traces and ensembles the way a monitor does, and it estimates satisfaction probabilities over a stochastic system the way a statistical model checker does, with synthesis on top of that. So, we compare against each family of tools.

How the comparison is timed and the other results are set out in the claims ledger.

What each tool expresses

There are properties only some tools can express. PRISM checks Markov chains exactly, but it cannot express a continuous-state recurrence, so the biodiesel-reactor and powertrain models run on SENTIL, Modest, and UPPAAL but not on PRISM. Neither FIG nor Modest can express a continuous-score real-valued walk, so they can't represent the AR(1) crossing. RTAMT and Breach have no probabilistic operator at all, so a PrSTL formula has no counterpart there.

Against the STL monitors

On discrete-time STL, SENTIL and RTAMT compute the same thing and we measure the wall-clock time the full robustness signal takes on the nested formula G[0,100](F[0,10](x>5)), on one core of the same node.

Both are linear in trace length; SENTIL runs about two orders of magnitude faster across the range. Per formula at 2001 samples, the full-signal speedup ranges from about 80x to about 158x across the five benchmark formulas. Online, driven one sample at a time, and SENTIL's median per-update is 1.843 us against RTAMT's 39.614 us, about 21.5x.

Run on one EPYC 7763 core, SENTIL v0.3.0.

Breach works in dense time, so the comparison is on the dense robustness value. The robustness matches and on the monitoring question, SENTIL answers in microseconds where Breach needs milliseconds.

The dense-time monitoring question at time zero. Same node and same formulas as the discrete evaluation. log scale.

Against the statistical model checkers

Comparing against PRISM, Modest, and UPPAAL-SMC needs a model all four can simulate. The Barkai-Leibler circadian CTMC asks whether the activator reaches 100 within 20 time units, a rare-ish event near 0.04. The tandem queue asks whether either queue fills within 50 time units, a common event near 0.72. Both are estimated at 10,000 samples, except UPPAAL, which picks its own count from the requested half-width. The estimates agree across all four tools; the wall times differ by an order of magnitude. The results are Probability (time).

On the circadian model SENTIL runs about 27 times faster than PRISM, about 19 times faster than UPPAAL-SMC, and roughly 70 times faster than Modest; on the tandem queue it is about 17 times faster than PRISM. The speedup comes from the step being a few arithmetic operations against a general model engine, not from a looser estimate: the probabilities land on the same value. Two further models, the biodiesel reactor at 0.192 and the powertrain controller at 0.503, are continuous-state recurrences PRISM cannot express; SENTIL, Modest, and UPPAAL all run them and agree, and SENTIL finishes more than an order of magnitude sooner.

The circadian model at about 10,000 samples: every tool lands on the same probability and the wall times separate by an order of magnitude.

The tandem queue under the same setup; the estimates agree across the four tools.

For rare events too, the picture still holds. On a two-queue tandem overflow at 5.602e-6 and a three-queue tandem at 1.274e-5, PRISM computes the value exactly, FIG and Modest reach it by importance splitting, and SENTIL by adaptive multilevel splitting. All four reach the value within their stated precision. Among the simulation methods SENTIL is the fastest by a wide margin, tens of milliseconds against tens of seconds, and its estimate is also the tightest, within a fraction of a percent of the truth. PRISM's exact check is quick here only because the state space is small, and it stops being an option once the model is large or continuous, which is exactly where the splitters are needed.

The two-queue overflow at 5.6e-6: SENTIL estimates it in 12 ms against 18 s for Modest and 58 s for FIG, and lands on the exact value.

The three-queue overflow at 1.3e-5, where the gap to the other splitters is the same two orders of magnitude. PRISM's exact check comes in at 40 ms against SENTIL's 46 ms, which is because of the small state space rather than being faster.