For more than three decades, UPPAAL has supported the modelling and analysis of real-time and cyber-physical systems. Yet building a suitable model, formalising the intended properties, choosing analysis techniques and interpreting counterexamples remain iterative tasks that demand substantial expertise. Large language models (LLMs) can offer plausible explanations and even solutions, but they are not necessarily correct. We present UPPAAI, an extension of UPPAAL in which users construct, explain, debug and specify models in dialogue with an LLM. The guiding principle is that the user requests, the LLM proposes, explains and orchestrates, and UPPAAL verifies. UPPAAI exposes the UPPAAL editor, queries and verifier through a Tools API. We report on seven case studies, from explaining to a newcomer to learning a controller, covering timed automata, stochastic hybrid automata and strategy learning. LLMs proved to be extremely helpful in not just generating solutions but also pro-actively suggesting relevant UPPAAL features it was not asked about.
Figures & tables
Figure 1: The U PPAAI loop: the LLM generates, the model checker acts as the critic, and the user remains in control of the requirements and the model.
Figure 2: UML component diagram showing U PPAAL connecting to LLM Service through the langchain4j library via the LCMessages API, while a vendor-supplied Agentic Client connects via the LLMMessages API and reaches the U PPAAL tools through MCP.
Function
Description
Model and templates
getContext
The state of U PPAAL GUI (changes and selection)
get / replaceModel
Read or replace the whole model
checkSyntax
Check the model for syntax errors
getTemplateList
List the templates in the model
get / replaceTemplate
Read or replace a template
Table 1: Tools API: functions exposed by U PPAAL to the LLM.
Table 6: Results per model variant over 24 h, random scenario (1000 runs, 95 % CI; Qmax : fully open outlet flow in m 3 /min; severity in m ⋅ min; –: not checked).
Table 8: Results per model variant ( ✓ : holds; × : violated; WCRT: exact worst-case latency; Pr: S MC probability of a deadline miss within 10 cycles; cex: steps of the shortest counterexample; –: not checked).
bug suspected at once and confirmed by UPPAAL; explained from the trace; fixed with one timer per black box; final model verifies in seconds
bound of at most 8 boxes on the belt; state-space explosion diagnosed; scalar sets for symmetry reduction
model never taken this far by us; session of 17 min
Lanes
12
56
two bugs found with UPPAAL, explained and fixed; SMC guarantees for the full model with more lanes and cars, in a full sweep
lanes shortened (700 → 120) to fit the state space
buggy left-over; unresolved after repeated half-hour attempts
Known domain
COVID
6
51
agent-based model (one automaton per individual), fully parameterised; SMC queries in correct syntax; CTMC and ODE variants
clean-up of previous session; extensions (age structure, threshold-triggered lockdown or vaccination, hospital capacity); consistency of the three models shown
agent-based model was the end goal of our earlier work [ 9 ]
Pond
12
39
Stratego model with randomised rain scenarios and ODE pond dynamics; learned periodic outlet controller balancing overflow against average level
previous model saved and cleared; step-size study with Stratego to shorten learning
complete model and controller in one session
Table 12: The sessions side by side, emphasising acceleration (Pr.: prompts; Calls: MCP tool calls; Beyond the request: contributions the user did not ask for; Reference: what had been achieved, or what the user knew, without the LLM).
Appendix figures & tables7 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 4: Claude prompt, result and explanations
Figure 5: Claude created traffic lights model with queries through U PPAAL MCP
Figure 6: U PPAAL with direct connection to Anthropic API with Claude Sonnet 5.5
Figure 7: Configuring U PPAAL MCP connection (Fig. 8(b) ) within Claude Desktop
Figure 8: LLM configuration dialogs in U PPAAL
Ingredient
Example syntax
Role
Locations
Idle , Busy
Control states. Initial, urgent (no delay) and committed (atomic, no interleaving) variants
Clocks
clock x , y ;
Real-valued, advancing at rate 1 . Stopwatches via rate constraints x ’==0
Hybrid / ODE dynamics
T ’ == - k *( T - Tenv )
Continuous variables with arbitrary rates or ODEs written as derivative constraints in invariants, using double variables and maths functions. These give stochastic hybrid automata, analysed by simulation and S MC ; the symbolic engines support only stopwatches
Invariants
x < = 5
Location constraint bounding how long time may pass there
Edges
g / sync / upd
Guard, optional synchronisation and update (clock resets, assignments, function calls), with select for families of edges
Clock constraints
x - y < 3
Bounds on clocks and clock differences, in guards and invariants
Appendix
Table 13: Ingredients of a U PPAAL modeling language.
Formalism
Non-determinism
Typical queries
Results produced
Timed automata (symbolic MC)
Non-deterministic: all behaviours are explored exhaustively
E < > p , A [] p , E [] p , A < > p , p −− > q , A [] not deadlock , sup / inf / bounds { p }: e
Boolean verdict (“maybe” for stopwatch over-approximation). Symbolic diagnostic trace (witness or counterexample). Upper and lower bounds
Stochastic (hybrid) TA (SMC)
Probabilistic: uniform or exponential delays, weighted branches, race between components
Pr [ < = T ]( < > p ) , Pr [ < = T ]( < > p ) > = 0.9 , Pr .. > = Pr .. , E [ < = T ; n ]( max : e ) , simulate [ < = T ; n ]{ e1 , e2 }
Probability estimates with confidence intervals. Hypothesis-test and comparison verdicts. Expected values with confidence intervals. Sampled trajectories, histograms and concrete witness traces
Timed games (TIGA)
Antagonistic environment controls the uncontrollable edges
control : A [] p , control : A < > p
Verdict, plus a synthesised most permissive winning strategy that is correct by construction
Timed MDPs (Stratego)
Stochastic environment, controller chooses
strategy S = minE ( e )[ < = T ]: < > p under Safe , Pr [..]( < > p ) under S , E [..]( max : e ) under S , simulate [..]{..} under S
Near-optimal strategies learned by reinforcement learning, optionally shielded by a synthesised safe strategy. Strategies can be evaluated, compared and model checked
Appendix
Table 14: Formalisms, queries and results supported by U PPAAL 5.0.
Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.
Jun Yang, Yuechun Sun, Yi Wu +5
The University of Chicago · Purdue University · The University of Toronto +1
We study whether Large Language Models (LLMs) can perform feature model analysis operations (AOs) directly on semi-formal textual blueprints, i.e., concise constrained-language descriptions of feature hierarchies and constraints, enabling early validation in Software Product Line scoping. Using 12 state-of-the-art LLMs and 16 standard AOs, we compare their outputs against the solver-based oracle FLAMA. Results show that reasoning-optimized models (e.g., Grok 4 Fast Reasoning, Gemini 2.5 Pro) achieve 88-89% average accuracy across all evaluated blueprints and operations, approaching solver correctness. We identify systematic errors in structural parsing and constraint reasoning, and highlight accuracy-cost trade-offs that inform model selection. These findings position LLMs as lightweight assistants for early variability validation.
Viet-Man Le, Thi Ngoc Trang Tran, Sebastian Lubos +2
Verification is becoming central to both reinforcement-learning-based training and inference-time control of large language models (LLMs). Yet current verifiers face a fundamental trade-off: LLM-based verifiers are expressive but hard to control and prone to error, while deterministic executable verifiers are reliable and interpretable but often limited in capability. We study the following question: given a development set of LLM outputs and labels for a target objective, such as correctness, can we automatically induce a minimal set of Python verifiers whose joint satisfaction closely matches that objective? We propose AutoPyVerifier, a framework that uses an LLM to synthesize candidate verifier functions and then refines them through search over a directed acyclic graph (DAG). By navigating the DAG, AutoPyVerifier systematically explores the space of deterministic executable verifiers and selects a compact verifier set whose joint satisfaction best approximates the target objective. Across mathematical reasoning, coding, function calling, and instruction-following benchmarks for several state-of-the-art LLMs, AutoPyVerifier improves target-objective prediction by up to 55.0 F1 points over the initial LLM-generated verifier sets. Additional analyses show that the most useful verification targets vary by benchmark and model, and that the DAG-based search shifts the learned verifier sets toward more structural and semantically grounded checks. We further show that exposing the discovered verifier set to an LLM as an external tool improves downstream accuracy by up to 17.0 points. We release our code