UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis

📄 arXiv: 2610.40042v1 📥 PDF

作者: Peter Dolog, Kim G. Larsen, Marius Mikučionis, Frederik F. K. Rasmussen

分类: cs.SE, cs.AI, cs.LO

发布日期: 2026-10-29

备注: Submitted to IFS/ETAPS 2027

💡 一句话要点

提出UPPAAI以解决实时与网络物理系统建模难题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 实时系统 网络物理系统 大型语言模型 模型验证 UPPAAL 自动机 策略学习

📋 核心要点

  1. 现有的UPPAAL工具在建模和分析实时系统时，用户需要具备较高的专业知识，过程复杂且迭代性强。
  2. UPPAAI通过引入大型语言模型，允许用户与模型进行对话，从而简化模型构建、调试和验证的过程。
  3. 在七个案例研究中，UPPAAI展示了其在模型解释和控制器学习方面的有效性，LLMs的引入显著提升了用户体验和效率。

📝 摘要（中文）

UPPAAL在过去三十年中一直支持实时和网络物理系统的建模与分析。然而，构建合适的模型、形式化预期属性、选择分析技术以及解释反例仍然是需要大量专业知识的迭代任务。大型语言模型（LLMs）能够提供合理的解释甚至解决方案，但并不一定正确。本文提出UPPAAI，这是UPPAAL的一个扩展，用户可以与LLM对话来构建、解释、调试和指定模型。UPPAAI通过工具API暴露UPPAAL编辑器、查询和验证器。我们报告了七个案例研究，从向新手解释到学习控制器，涵盖了定时自动机、随机混合自动机和策略学习。LLMs在生成解决方案和主动建议相关UPPAAL特性方面表现出极大的帮助。

🔬 方法详解

问题定义：本文旨在解决UPPAAL在建模和分析实时与网络物理系统时，用户需要大量专业知识和迭代过程复杂的问题。现有方法在模型构建、属性形式化和反例解释等方面存在显著挑战。

核心思路：UPPAAI的核心思路是利用大型语言模型（LLMs）与用户进行对话，帮助用户构建、解释和调试模型。通过这种方式，用户可以更轻松地与模型交互，减少对专业知识的依赖。

技术框架：UPPAAI的整体架构包括用户界面、LLM交互模块和UPPAAL验证器。用户通过工具API与UPPAAL编辑器进行交互，LLM负责生成建议和解释，最后由UPPAAL进行验证。

关键创新：UPPAAI的最大创新在于将LLMs与UPPAAL的功能结合，使得用户能够在建模过程中获得实时的反馈和建议。这种交互式的建模方式与传统的静态建模方法有本质区别。

关键设计：在设计中，UPPAAI实现了对UPPAAL编辑器的全面暴露，允许用户通过API进行查询和验证。同时，LLMs的引入使得系统能够主动建议与用户需求相关的UPPAAL特性，提升了用户的建模效率。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在七个案例研究中，UPPAAI展示了其在模型构建和控制器学习方面的有效性。LLMs不仅能够生成解决方案，还能主动建议相关的UPPAAL特性，显著提升了用户的建模效率和体验。

🎯 应用场景

UPPAAI的研究成果在实时系统、网络物理系统和控制器设计等领域具有广泛的应用潜力。通过简化建模和分析过程，UPPAAI可以帮助工程师和研究人员更高效地开发和验证复杂系统，降低对专业知识的依赖，推动相关领域的技术进步。

📄 摘要（原文）

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.