Source-linked AI summary
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
Peter Bulychev, Alexandre David, Kim Gulstrand Larsen, Marius Mikučionis, Danny Bøgsted Poulsen, Axel Legay, Zheng Wang
TL;DR
UPPAAL-SMC addresses the challenge of analyzing real-time stochastic systems when relevant model-checking problems can be undecidable. The paper surveys its priced-timed-automata semantics, statistical techniques, interface, engine, and applications, reporting a tool that handles real-time features and supports case studies beyond classical model checkers. Its scope remains bounded by implementation and modeling limitations, including inadequate general floating-point support and assumptions in the stochastic semantics.
Problem
Statistical model checking must address real-time systems and properties whose checking problems are undecidable, while rare properties remain challenging for simulation-based approaches.
Method
The paper surveys UPPAAL-SMC’s stochastic priced-timed-automata semantics, statistical algorithms, state-detection engine, user interface, and case-study applications.
Results
UPPAAL-SMC handles systems with real-time features and has been applied to case studies beyond the scope of classical model checkers.
Takeaways & Limitations
UPPAAL-SMC provides probability distributions and probability comparisons for analyzing performance properties of real-time priced timed-automata systems.
Takeaways & Limitations
Floating-point support is implemented by extending clock operations, and the paper states that better, more general support is needed.
Abstract
from arXiv · showhide
This paper offers a survey of uppaalsmc, a major extension of the real-time verification tool uppaal. uppaalsmc allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, uppaalsmc relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. uppaalsmc comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.
1 Introduction
Statistical model checking estimates stochastic-system properties by simulation rather than exact numerical computation. The survey presents UPPAAL-SMC as an extension for real-time priced timed automata, covering its formalisms, techniques, interface, and applications.
- Statistical model checking simulates finitely many runs and uses hypothesis testing to infer whether a specification is satisfied or violated.Samples are drawn according to the system’s probability distribution, allowing estimates of execution measures.
- Unlike exhaustive approaches, simulation-based checking does not guarantee certainty, but it can provide bounded statistical evidence.
- SMC is attractive because it is simple to use, requires no extra modeling effort, supports properties beyond classical temporal logics, and approximates undecidable problems.
- UPPAAL-SMC extends UPPAAL with statistical model checking for networks of priced timed automata under a natural stochastic semantics.The extension targets real-time systems and estimates undecidable problems.
- The tool provides a user interface for specifying complex problems, obtaining probability distributions, and comparing probabilities to analyze performance.
- The survey covers priced timed-automata modeling and specification formalisms, applied techniques, the graphical interface and engine, and case-study applications.
2 Modeling Formalism
UPPAAL-SMC models networks of priced timed automata with stochastic timing and transitions, enabling quantitative reachability and performance analysis. Its modeling language supports expressive rates, distributions, data structures, floating-point clock arithmetic, and case-study-specific constructs.
- NPTA semantics: Priced timed automata extend timed automata with clocks evolving at different rates, while networks communicate through broadcast channels and shared variables.The resulting NPTA model supports stochastic analysis, although general reachability is undecidable because NPTAs match the expressive power of linear hybrid automata.
- Stochastic semantics: UPPAAL-SMC assigns probability distributions to state delays and transitions, using uniform bounded delays, exponential indefinite delays, and independent component races.These choices induce quantitative properties such as the probability of reaching T3 within a specified cost bound.
- Case-study models: In the Hammer Game, stochastic delays make winning probabilities depend on time and energy bounds rather than only on the players’ deterministic task descriptions.Axel wins with unbounded time at 59% versus Alex’s 41%, but Alex becomes more likely under a 50-second deadline or a 52-energy-unit limit.
- Modeling language: The extended language permits arbitrary integer clock rates, weighted branching edges, integer variables, data structures, and user-defined functions.A train-gate model uses state-dependent exponential arrival rates, uniform crossing times, and a queue maintained by the controller.
- Numerical extensions: Floating-point clock arithmetic supports small-step integration of functions such as sin(t) and cos(t), with high rates producing small random time steps.The resulting monitored trajectories approximate the intended functions and form an almost perfect circle in the plotted sin-cos representation.
3 Properties and Queries
UPPAAL-SMC specifies weighted temporal properties over priced timed automata and uses statistical model checking to approximate generally undecidable probability questions. Its queries support hypothesis testing, probability estimation and comparison, expected values, and monitoring-based handling of full WMTL≤ formulas.
- Property formalism: WMTL≤ expresses weighted temporal properties over runs using atomic propositions, Boolean operators, next-state, and bounded-until operators.A bounded-until formula requires one property to hold until another becomes true before a clock increases by more than a specified bound.
- Statistical model checking: Checking whether PM(ψ) ≥ p is generally undecidable, so cost-bounded reachability probabilities are approximated with simulation-based statistical model checking.The supported form is PM(♦x≤Cφ) ≥ p, where φ is a state predicate, x is a clock, and C is a bound.
- Query types: UPPAAL-SMC answers threshold, probability-evaluation, and probability-comparison questions through statistical algorithms over sampled runs.Runs are encoded as Bernoulli observations, followed by sequential hypothesis testing or estimation procedures.
- Hypothesis testing: Hypothesis testing uses an indifference region between p0 = θ + δ0 and p1 = θ − δ1, with α and β controlling error probabilities.The tested hypotheses are H0: p ≥ p0 and H1: p ≤ p1.
- Additional queries: The verifier also evaluates expected minima or maxima of clock or integer expressions over bounded runs, but currently provides no confidence for these values.The syntax explicitly supplies the number of runs N and the expression to evaluate.
- Full WMTL≤: Full WMTL≤ support constructs deterministic under- and over-approximation monitoring PTAs before applying the simulation engine.This extends the tool beyond the simpler statistical queries summarized above.
4 Graphical User Interface
UPPAAL-SMC’s graphical interface turns statistical verification and simulation into visual feedback, including distributions, monitored trajectories, and probability intervals. These views support comparison of system behavior and exploration of properties in train-gate and chemical-reaction examples.
- Statistical views: The verifier reports frequency histograms, average time or cost, probability densities, and cumulative distributions with confidence intervals.Confidence intervals for the latter distributions can use the Clopper-Pearson method.
- Plot composer: The plot composer superposes probability distributions, allowing users to compare trains 0, 3, and 5 from the train-gate example.Users can select data and adjust plot labels, shapes, and colors.
- Monitoring expressions: Expression monitoring visualizes train crossings and queue length along a random run, exposing behavior that can motivate additional queries.The example monitors Train(0).Cross, Train(5).Cross, and Gate.len.
- Querying monitored behavior: The probability that Gate.len remains below 3 after time 20 is estimated in the interval [0.102,0.123].The query uses a 300-time-unit bound and an added clock t.
- Case-study visualization: Chemical-reaction simulations visualize oscillating concentrations of reactants a and b and can display clouds of trajectories.Starting from a=99 and b=1, the model describes mutual consumption and production of the two reactants.
- Visualization performance: High exponential rates create many small time steps, so the engine filters curves on the fly to avoid impractical memory and redraw costs.Without filtering, plots can consume several GB of memory and incur substantial transfer and redraw times.
5 Engine
The UPPAAL-SMC engine implements optimizations for accurate and efficient statistical simulation, including distributed execution, state detection, early termination, and dependency-aware reuse of stochastic choices. These techniques support query evaluation without relying on symbolic zones for the described state-detection mechanism.
- Engine overview: The engine section exposes optimizations and new features underlying UPPAAL-SMC’s current performance.The paper presents techniques that were not exposed in earlier versions of the tool.
- Distributed SMC: Distributed sequential SMC must prevent bias caused by accepting runs finishing faster than rejecting runs on different computation cores.The stated solution is to force all cores to generate the same amount of work.
- State detection: State detection ensures delay selection does not skip future points where guards or query formulas become relevant.The engine tracks lower bounds for transitions and formulas using decorated states rather than symbolic zones.
- Early termination: Early termination stops a run when its query is satisfied, while until properties can stop it when their continuing condition no longer holds.Both mechanisms avoid simulating the run through its full specified bound.
- Reuse of choice: Dependency-aware reuse preserves previously sampled delays when transitions cannot affect another process, invalidating them only when dependencies arise.Dependencies include synchronization, clock rates, invariants, guards, and updates.
- Performance evaluation: The engine evaluates queries such as bounded train-crossing properties during simulation, with Table 1 comparing probability and time results with and without reuse.The cited comparison is organized as results without (-) and with (+) reuse.
6 Case-Studies
The case studies apply UPPAAL-SMC to robot control, communication protocols, wireless-network equilibria, resource-constrained task systems, and distributed SMC. They demonstrate probability estimation and comparison, energy analysis, protocol evaluation, and performance comparisons with Prism.
- Robot Control: UPPAAL-SMC computes the probability distribution for a robot reaching its goal while bounding time spent on consecutive fire and ice fields.The property is expressed in WMTL≤ using a clock that grows at rate 1 and is never reset.
- Firewire: UPPAAL-SMC compares estimated probabilities directly or through a more efficient indirect probability-comparison method.The Firewire case study visualizes estimated probabilities together with regions where the probabilities are indistinguishable.
- Bluetooth: Bluetooth analysis estimates response-time and energy-consumption distributions, with operation cost reaching at least 2440 energy units after 70 seconds and a mean of about 2853 energy units.These values describe the reported energy-consumption analysis for device operation.
- Wireless Ad Hoc Networks: An SMC-based two-phase algorithm heuristically finds and then statistically tests Nash-equilibrium strategies for Aloha CSMA/CD and IEEE 802.15.4 CSMA/CA.For two-node Aloha CSMA/CD, the Nash-equilibrium strategy is slightly less efficient than the symmetric optimum but still has high utility.
- Duration Probabilistic Automata: In Duration Probabilistic Automata experiments, UPPAAL models use continuous, matched, or discrete semantics, and UPPAAL is notably faster than Prism.The comparison varies the numbers of SDPAs, tasks per SDPA, and resource types; the time bound is calibrated from 369 simulations.
7 Conclusions
UPPAAL-SMC extends statistical model checking to real-time systems and supports applications beyond classical model checkers. The conclusion identifies future work in floating-point support, hybrid modeling, new application domains, and rare-event analysis.
- UPPAAL-SMC handles real-time features and has been applied to case studies beyond classical model checkers.
- Floating Point: Current floating-point support misuses and extends clock operations, motivating more general support.
- Hybrid Systems: Future hybrid-system support is planned through differential equations, restricted to simple equations with known analytical solutions to fit the stochastic semantics.
- New Applications: The extended hybrid modeling language broadens applications, particularly to biological systems, with visualization and statistical model-checking support.
- New Applications: UPPAAL-SMC can analyze controller stability and energy consumption, and can support refinement checking.
- Rare Events: Rare-event work aims to reduce simulation effort by developing efficient importance-sampling distributions for priced timed automata.The proposed direction exploits pure timed model checking to improve the search for efficient distributions.