Animation, Verification and Visualisation of Prolog Transition Systems with ProB

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.

In Proceedings ICLP 2026, arXiv:2607.17707

Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Computer Science and Game Theory (cs.GT)

arXiv:2607.21192 [cs.LO]

(or arXiv:2607.21192v1 [cs.LO] for this version)

https://doi.org/10.48550/arXiv.2607.21192 arXiv-issued DOI via DataCite (pending registration)

EPTCS 450, 2026, pp. 148-162

https://doi.org/10.4204/EPTCS.450.13 DOI(s) linking to related resources