arXiv cs.AI· Peter Dolog, Kim G. Larsen, Marius Miku\v{c}ionis, Frederik F. K. Rasmussen·· 4 小时前AI 评分36
UPPAAi：用 LLM 辅助 UPPAAL 的建模、验证、分析与综合
UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis
AI 导读
UPPAAi 是 UPPAAL 的扩展，让用户通过与 LLM 对话来构建、解释、调试和规约实时与信息物理系统模型，核心原则是用户提出请求、LLM 提议解释与编排、UPPAAL 负责验证。它通过 Tools API 暴露 UPPAAL 编辑器、查询和验证器，并报告了七个案例研究，覆盖时间自动机、随机混合自动机和策略学习。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