Scholarlink

During a period of 30 years, the tool Uppaal has evolved from being a Timed Automata model checker to a tool allowing reinforcement learning of near-optimal control strategies for hybrid Markov Decision Processes. In this tutorial, we present the various capabilities of Uppaal, with a detailed explanation of the syntax and semantics of the various supported modeling formalisms. We demonstrate through examples the type of analysis supported, which includes model checking, performance analysis, controller synthesis, and reinforcement learning. In addition, we provide details of the various engines that allow for these analyses to be carried out efficiently.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Model Checking, Performance Analysis, Synthesis and Learning for Cyber Physical Systems

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Kim G. Larsen,
  • Marius Mikučionis

摘要

During a period of 30 years, the tool Uppaal has evolved from being a Timed Automata model checker to a tool allowing reinforcement learning of near-optimal control strategies for hybrid Markov Decision Processes. In this tutorial, we present the various capabilities of Uppaal, with a detailed explanation of the syntax and semantics of the various supported modeling formalisms. We demonstrate through examples the type of analysis supported, which includes model checking, performance analysis, controller synthesis, and reinforcement learning. In addition, we provide details of the various engines that allow for these analyses to be carried out efficiently.