arXiv cs.AI· Peter Dolog, Kim G. Larsen, Marius Miku\v{c}ionis, Frederik F. K. Rasmussen·· 14 小时前AI 评分31
UPPAAi：面向 LLM 辅助建模、验证、分析与综合的 UPPAAL 扩展
UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis
AI 导读
UPPAAi 是 UPPAAL 的扩展，让用户通过与 LLM 对话来构建、解释、调试和规约模型，遵循"用户请求、LLM 提议解释与编排、UPPAAL 验证"的原则。它通过 Tools API 开放 UPPAAL 编辑器、查询与验证器，并报告了 7 个案例研究，覆盖时间自动机、随机混合自动机和策略学习。研究显示 LLM 不仅能生成方案，还会主动建议用户未询问的相关 UPPAAL 功能。
正文 · 原文
Abstract: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.
| Comments: | Submitted to IFS/ETAPS 2027 |
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2610.40042 [cs.SE] |
| (or arXiv:2610.40042v1 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2610.40042 arXiv-issued DOI via DataCite |
Submission history
From: Marius Mikučionis [view email]
[v1]
Thu, 29 Oct 2026 13:40:33 UTC (746 KB)
来源：arXiv cs.AI · arxiv.org