Coming from UPPAAL-SMC

UPPAAL-SMC estimates the probability that a property holds over the runs of a stochastic timed automaton. SENTIL does statistical model checking too, and on the shared benchmarks the two agree on the probability. The difference is the input. UPPAAL reads a model written in its own formalism and samples its runs. SENTIL works from either side: it can lift a recorded trace into a noisy ensemble through a fitted noise model, and it can also simulate a stochastic system.

You rewrite the UPPAAL-SMC automaton as a SENTIL stochastic system or as a lifted trace, and you rewrite each Pr[...] query as a PrSTL formula. The query mapping is small, and the two probabilistic operators you use most, reachability and invariance, work straight out of the box.

Query and model mapping

The E[...] expectation queries have no probability-estimate counterpart because they ask a different question and are out of scope for this mapping. For sequential decisions, UPPAAL's hypothesis-testing mode corresponds to SENTIL's SPRT and Bayesian regimes, covered in running SPRT.

Translating a query

The UPPAAL reachability query asks whether the activator protein reaches 100 within 20 time units.

Pr[<=20] (<> activator >= 100)

In SENTIL you estimate the same probability over a trace ensemble. The base trace is lifted into candidate trajectories by the registered noise model, the inner formula scores each, and the statistical layer reports the fraction that satisfy it with a confidence interval.

sentil smc -f 'P>=0.5(F[0,20] (activator >= 100))' \
  -t activator.csv --noise 'activator=gaussian:0,5' --samples 1e4

import sentil
from sentil import Formula

trace = sentil.Trace.from_path("activator.csv")
lifting = sentil.LiftingRegistry()
lifting.register("activator", sentil.NoiseModel.gaussian(0.0, 5.0))
phi = Formula.parse("P>=0.5(F[0,20] (activator >= 100))")
result = phi.check(trace, lifting)   # result.probability, result.interval, result.holds

use sentil::{Formula, Trace, LiftingRegistry, NoiseModel, NoiseInteraction, SmcConfig};

let trace = Trace::from_path("activator.csv")?;
let mut lifting = LiftingRegistry::new();
lifting.register("activator", NoiseModel::gaussian(0.0, 5.0)?, NoiseInteraction::Additive);
let phi = Formula::parse("P>=0.5(F[0,20] (activator >= 100))")?;
let result = phi.check(&trace, &lifting, &SmcConfig::default())?;   // result.probability, result.interval, result.holds

The threshold in P>=0.5(...) sets the pass or fail verdict. The estimated probability is UPPAAL's Pr[...] analogue. To simulate a model directly rather than lift a recorded trace, the same benchmark uses a stochastic system stepped by Gillespie's direct method, which is how the circadian comparison below is run.

Comparisons

In the Barkai-Leibler circadian CTMC, the property asks the activator to reach 100 within 20 time units, an event near probability 0.04. SENTIL simulates the same CTMC and estimates the same probability by direct Monte Carlo.

On the circadian model SENTIL is roughly 19 times faster with an agreeing estimate and on the same model, it is about 27 times ahead of PRISM and about 72 times ahead of Modest. On the tandem queue, the margin is wider, about 67 times.

Two further models in the suite, the biodiesel reactor and the powertrain controller, are continuous-state recurrences. UPPAAL runs them as stochastic hybrid automata, holding the reactor state in rate-zero clocks and stepping the Euler recurrence one interval at a time, and estimates 0.194 and 0.497, agreeing with SENTIL and Modest. PRISM cannot express either.

The numbers come from benchmarks/results/sentil_smc.jsonl and uppaal_smc.jsonl, with the reproduction commands, the rebuilt models under benchmarks/baselines/uppaal, and the tolerances in the claims document. For the full cross-tool picture see how SENTIL compares and smc comparisons, and for rare events below what a flat Monte Carlo run reaches, rare-event splitting.