Animation, Verification and Visualisation of Prolog Transition Systems with ProB

[Submitted on 23 Jul 2026]

Authors:Jan Gruteser (Heinrich Heine University Düsseldorf), Michael Leuschel (Heinrich Heine University Düsseldorf), Katharina Engels (Heinrich Heine University Düsseldorf), Fabian Vu (Heinrich Heine University Düsseldorf)

View PDF

Abstract: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.

Submission history

From: EPTCS [view email] [via EPTCS proxy]
[v1] Thu, 23 Jul 2026 11:16:49 UTC (1,567 KB)