---
title: "Animation, Verification and Visualisation of Prolog Transition Systems with ProB: Recent Extensions"
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","Formal Verification","Model Checking"]
---

# Animation, Verification and Visualisation of Prolog Transition Systems with ProB: Recent Extensions

## AI commentary

> This paper may seem niche, but if you work with Prolog or formal methods, ProB's statistical simulation and visualisation extensions can significantly boost debugging and verification efficiency. For the AI community, there is potential crossover with formal verification and strategy evaluation in reinforcement learning – worth a look.

## At a glance

ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. This work presents extended capabilities for Prolog animation mode, including statistical simulation, reliable trace replay, transitions with user input, and improved state visualisation. Case studies on game strategies (e.g., Connect Four) demonstrate the features, which also benefit ProB's new sequent prover for Event-B proof obligations and interactive teaching models.

## Key points

- ProB adds statistical simulation capabilities for randomized validation and analysis of Prolog transition systems.
- Improved state visualisation enables users to intuitively explore system behavior and game strategies.
- Connect Four case study validates the effectiveness of different decision strategies using the new features.

## Full text

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.

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_3facf37784b8b0e7c509c7eb