---
title: "Prolog过渡系统的动画、验证与可视化：ProB工具最新扩展"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2607.21192v1"
permalink: "https://feed.astralor.com/items/itm_3facf37784b8b0e7c509c7eb"
published: "2026-07-23T11:16:49.000Z"
score: 72
channel: "tech"
tags: ["Event-B","ProB","Prolog","形式化验证","模型检测"]
---

# Prolog过渡系统的动画、验证与可视化：ProB工具最新扩展

## AI 点评

> 这篇论文虽然看似小众，但如果你是Prolog或形式化方法从业者，ProB的统计模拟和可视化扩展能大幅提升调试与验证效率。对于AI领域，形式化验证与强化学习中的策略评估有潜在交叉，值得关注。

## 速览

ProB是一个基于Prolog的模型检测器、动画器和约束求解器，用于高级形式化规范。最新工作扩展了其Prolog动画模式，支持统计模拟、可靠的回放、用户输入过渡和改善的状态可视化。通过游戏策略（如四子棋）案例研究展示了新功能，也适用于Event-B证明义务的序列证明器和交互式教学模型。

## 关键点

- ProB新增统计模拟功能，支持对Prolog过渡系统进行随机化验证与分析。
- 改进的状态可视化允许用户更直观地探索系统行为和游戏策略。
- 通过四子棋游戏案例，证明新特性可评估不同决策策略的有效性。

## 全文

ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB's Prolog animation mode and its recent extensions. The extended capabilities include simulation for statistical checks, more reliable trace replay, transitions with user input and improved state visualisation. We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four. The features are useful for many other applications, especially for ProB's new sequent prover for Event-B proof obligations, as well as for demonstration models for teaching in combination with interactive visualisation.

---

引用前请核对原文;本文由星际流动整理:https://feed.astralor.com/items/itm_3facf37784b8b0e7c509c7eb