Paper deep dive
Animation, Verification and Visualisation of Prolog Transition Systems with ProB
Jan Gruteser, Michael Leuschel, Katharina Engels, Fabian Vu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 7/24/2026, 2:47:17 AM
Summary
The paper presents extensions to ProB, a Prolog-based model checker and animator, specifically enhancing its XTL mode for animating Prolog-defined transition systems. Key contributions include integration with SIMB for statistical simulation, improved state visualization via VISB and HTML exports, symbolic transitions for handling user input and side effects, and enhanced trace replay capabilities. These features are demonstrated through case studies such as game strategy analysis (Connect Four) and proof obligation verification.
Entities (10)
Relation Signals (9)
ProB → implementedin → SICStus Prolog
confidence 96% · ProB [25] 1 is a model checker, animator, and constraint solver for high-level formal specifications implemented in SICStus Prolog.
ProB → implements → XTL Mode
confidence 95% · For historical reasons, the animation of prolog systems is referred to as the XTL mode of PROB.
ProB → usedfor → Connect Four
confidence 93% · We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four.
ProB → integrates → SIMB
confidence 92% · We apply the new integration with SIMB [43], a timed-probabilistic simulator in PROB
ProB → supports → Event-B
confidence 91% · especially for PROB's new sequent prover for Event-B proof obligations
ProB → supports → VISB
confidence 90% · improved state visualisation features with VISB [44]
ProB → supports → PCTL
confidence 89% · Recent work has integrated a model checker for Probabilistic Computation Tree Logic (PCTL) into PROB
SIMB → uses → Monte Carlo Simulation
confidence 88% · allowing for statistical validation using Monte Carlo simulation, hypothesis tests, and estimators
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2607.21192v1
- Canonical: https://arxiv.org/abs/2607.21192v1
Trouble viewing inline? Open PDF directly →
Full Text
48,194 characters extracted from source content.
Expand or collapse full text
W. Faber, L. Giordano, R. Rocha, V. Santos Costa (Eds.): 42nd International Conference on Logic Programming (ICLP 2026) EPTCS 450, 2026, p. 148–162, doi:10.4204/EPTCS.450.13 © J. Gruteser, M. Leuschel, K. Engels & F. Vu This work is licensed under the Creative Commons Attribution License. Animation, Verification and Visualisation of Prolog Transition Systems with PROB Jan Gruteser Michael LeuschelKatharina EngelsFabian Vu Faculty of Mathematics and Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universitätsstr. 1, D-40225 Düsseldorf jan.gruteser,michael.leuschel,katharina.engels,fabian.vu@hhu.de PROB is a Prolog-based model checker, animator and constraint solver for high-level formal specifi- cations. 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 sim- ulation 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. 1 Introduction PROB [25] 1 is a model checker, animator, and constraint solver for high-level formal specifications implemented in SICStus Prolog. While it primarily targets formal methods such as the B method [1] and Event-B [2], PROB can also load and animate transition systems specified in Prolog. As a result, PROB supports most of its validation and verification features for Prolog, mainly animation, model checking and visualisation. Moreover, one can use the interface to implement interpreters for other formalisms. For historical reasons, the animation of Prolog systems is referred to as the XTL mode of PROB. 2 This is how we refer to it in this article as well. Motivated by several use cases, specifically PROB’s new sequent prover [12], the XTL mode has been subsequently enhanced by new features. In the following, we first present the existing animation and model checking features, along with an introductory example. Then, we discuss the new extensions, each accompanied by a motivating example. We apply the new integration with SIMB [43], a timed- probabilistic simulator in PROB, to analyse a case study concerning game moves encoded as a Prolog transition system for Connect Four. Altogether, we present the following contributions: • new integration of SIMB for simulation of Prolog models, allowing for statistical validation using Monte Carlo simulation, hypothesis tests, and estimators, • improved state visualisation features with VISB [44] and standalone HTML trace exports, • new concept of symbolic transitions, enabling delayed computation to incorporate custom user input and to prevent premature execution of external side effects (e.g. a call to another tool), 1 Our tooling IDE PROB2-UI is available athttps://prob.hhu.de/w/index.php?title=Download#ProB2-UI. 2 The name XTL originates fromXSB Prolog andTemporalLogic. When first mentioned, XTL referred to a finite-state model checker for CTL properties of systems represented in XSB [15, 27]. However, there is no longer a connection to XSB. J. Gruteser, M. Leuschel, K. Engels & F. Vu149 • new static and dynamic transition annotations, useful for adding transition probabilities, textual descriptions and parameter names, • support for more reliable and interactive trace replay, • demonstration and evaluation of a case study in the context of game theory (Connect Four). The source code for all discussed examples is available on GitHub: https://github.com/hhu-stups/xtl-examples. In the following section, we introduce the basic functionality of XTL. 2 Prolog-Based Transition Systems in PROB ProB Animator Model Checking LTL/CTL PCTL Simulation Statistical Checks Trace Replay Visualisation State Space VisB Transition Specification start/1 trans/3 .P/.pl Other Spec. load interprete interactive Figure 1: PROB’s XTL Prolog Mode With PROB, it has long been possible to load Prolog files that define a labelled transition system by using special Prolog predicates. Early versions of these transition predicates were introduced in [26, 23]. The core of the definition is based on the predicates start(State)and trans(Name,StateBefore,StateAfter), which specify theinitial statesand all possibletran- sitionsto new states based on the current state. A state can be represented by any (ground) Prolog term. For better comprehensibility of states and ver- ification, additionalstate propertiescan be provided by the predicateprop(State,Prop). 3 By loading the transition system into the PROB animator, we obtain access to most of its validation and verification features, particularly animation and model checking. An overview is shown in Figure 1. The green nodes highlight features that have been added or improved in this work and will be described in the following sections. Listing 1: Simple XTL Prolog Specification of a Traffic Light System 1start(lights(red,red)).% State: lights(Pedestrian,Cars) 2 3trans(tl_peds_green,lights(red,red), lights(green,red)). 4trans(tl_peds_red, lights(green,red),lights(red,red)). 5trans(switch_tl_cars(NL),lights(red,L),lights(red,NL)) :- tl_cars_seq(L,NL). 6 7prop(lights(P,_),'='(tl_peds,P)). 8prop(lights(_,C),'='(tl_cars,C)). 9prop(lights(P,C),unsafe) :- P \= red, C \= red. 10 11tl_cars_seq(red,red_yellow). tl_cars_seq(red_yellow,green). 12tl_cars_seq(green,yellow). tl_cars_seq(yellow,red). 3 More documentation can be found online athttps://prob.hhu.de/w/index.php?title=Other_languages. 150Animation, Verification and Visualisation of Prolog Transition Systems withPROB Figure 2: Prolog Animation in PROB2-UI Animation.Listing 1 il- lustrates a simple example of a traffic light system, con- trolling one light for pedes- trians and one for cars (avail- able on GitHub [14]). The states are modelled as terms of the formlights(P,C), wherePis the state of the pedestrian light andCthe state of the light for cars, given by Prolog atoms, e.g. greenorred_yellow. Ini- tially, both lights arered (line 1). The transitions are specified in lines 3 to 4, which allow changing a traf- fic light if and only if the other one isred. The first argument is the transition term, which can have additional parameters, such asNLforswitch_tl_cars. Prolog predicates can be used freely in the computation of a transition; for example,tl_cars_seq(lines 11, 12) is used to define the sequence of colours. If a transition predicate fails, no corresponding transition is available in the current state. A user can open the specification file using one of the PROB interfaces: a command-line interface and graphical user interfaces based on Tcl/Tk and Java. The latter is called PROB2-UI [5] and is shown in Figure 2 with the example of Listing 1 loaded into the animator. By selecting one of the enabled transitions in the top-left corner, a user can animate a transition to the next state. Here, only one transition is available for switching the car light toyellow. The trace leading to the current state, i.e. a sequence of animated transitions starting at an initial state, is shown in the history at the bottom right. Here, the current state islights(red,green), meaning the light for pedestrians isred, and the one for cars is green. One can inspect the current state, with the specified state properties at the top and custom state visualisations at the bottom. We integrate the latter as part of this work and discuss it in Section 3. Model Checking.One can apply the PROB model checker to find deadlocks (states in which no transi- tion is enabled) andunsafestates. We define a state as unsafe if an invariant, that is, a safety property that must be satisfied in every state, is violated. To declare safety conditions for the PROB model checker, one can define the special state propertyunsafe. For example, line 9 of Listing 1 states that one of the two traffic lights must always be red. For the traffic light system, the model checker explores six states and seven transitions without any unsafe state or deadlock (Fig. 5 shows a visualisation of the state space). Additionally, PROB supports model checking of formulas in Linear Temporal Logic (LTL) and Com- putation Tree Logic (CTL) to verify temporal properties. However, atomic propositions are restricted to state properties in the form of Prolog terms provided byprop/2. For example, the following LTL for- mula (left) verifies thattl_carswill always (G– globally) eventually (F– finally) becomegreen (which is prevented by the loop switching only the pedestrian light). The CTL formula (right) checks whether at least one such trace exists, which is indeed the case. GFtl_cars=green(false)EFtl_cars=green(true) J. Gruteser, M. Leuschel, K. Engels & F. Vu151 To restrict the state space, we added support forscopepredicates in this work. PROB will ignore all states where the predicate is not satisfied. However, the predicate has to be provided in B syntax, so XTL properties are addressed by PROB’s built-in functions, for example, to obtain the current value of a state property (check that the car light does not showred_yellow): prob_pragma_string('SCOPE','STATE_PROPERTY("tl_cars") /= "red_yellow"'). prob_pragma_string/2allows to keep preferences for PROB directly in the specification, where the preference name is the first and the value the second argument. The predicate above eliminates all states after the car light has becomered_yellow, i.e. the model checker finds four states and four transitions. There exist more advanced features, such as directed model checking controlled by a heuristic func- tion [24], provided byheuristic_function_result/2. Interpreters for other Formalisms.One can also use the interface to implement a custominter- preterfor other specification languages and to declare the transitions for PROB. The interface was used, for instance, for Promela (the verification language of the SPIN model checker [19]), SMV [28], CSP(-M) [23], and Lustre [37]. Those interpreters are implemented to support the loading of files mod- elled in the new formalism. From the engineering perspective, one must implement the formalism by defining predicates that describe the initial state (start/1), the state transitions involving predecessor and successor states (trans/3), and state-based properties such as invariants and other state-based er- rors (prop/2). Implementing those predicates enables the use of PROB’s animator and model checker for the new formalism, allowing one to check, e.g., for invariants and deadlocks. Another advantage of implementing interpreters in Prolog is that operational semantics expressed as inference rules of the form [ B A Cond] align with Prolog’s clause notation and can be translated toA :- B, Cond. A concrete example is the following semantic rule, which one can encode as shown in Listing 2. Listing 2: Interpreter Code for Semantic Rule interpret(assign(x,E), State, NewState) :- eval(E,V), update(State, x, V, NewState). eval(E)⇒V,σ ′ =σ◁−x7→V σ−→ x:=E σ ′ Concerning the performance aspect, we expect implementing an interpreter in Prolog to perform faster than translating to a B machine and then interpreting with PROB. Still, for some verification and validation tasks, e.g. symbolic model checking, one could translate to B. That approach would also enable code generation to other programming languages [40, 38, 41] to achieve better performance. Both aspects were analysed with Lustre [37] and may also apply to other formalisms. 3 State Visualisation Visualisation plays a crucial role in validating formal models, as it helps modellers and domain experts understand and check whether the behaviour is as expected. Hence, PROB offers multiple ways to visualise state properties and interact with visualisations. This work improves the state visualisation of XTL models by an animation function and enables the use of the more advanced component VISB [44]. Animation Function.In XTL mode, it has already been possible to create a lightweight domain- specific state visualisation using special predicates targeting PROB’s “animation function”. This func- tion defines a grid-based visualisation and transforms the current state into a matrix of coordinates, each mapped to an image or text. The animation function is specified in Prolog using the predicate 152Animation, Verification and Visualisation of Prolog Transition Systems withPROB Figure 3: Interactive Chess Visualisation Defined by an Animation Function in PROB2-UI Chess Piece Icons by Cburnett via Wikimedia Commons, licensed under C BY-SA 3.0 (https://creativecommons.org/licenses/by-sa/3.0). animation_function_result(State,Matrix), whereMatrixis a term of the form((I,J),Img). As part of this work, we integrate an HTML trace export into PROB2-UI, which contains individual state visualisations for each trace step independently of PROB for inspection in a browser. Our examples include an implementation of the chess game. Allowed moves are encoded as transi- tions; several scenarios can be used as the initial state. The current state of the chessboard is visualised using an animation function, as shown in Figure 3. Images of the chess pieces are used as cell content (registered viaanimation_image(Nr,ImgPath)). Moreover, the visualisation is interactive by imple- menting right-click actions; the user can select from a list of available moves for the specific position (these actions are defined viaanimation_image_right_click_transition(I,J,Act,State)). A complete HTML trace export can be found online [14]. VisB.Grid visualisations are especially useful for board games like chess, but they are limited when it comes to complex systems. In this case, VISB [44] provides a more flexible and customisable approach based on SVG graphics. The user can provide a custom SVG, and the attributes of the SVG elements are updated according to the current state. For example, this could be the colour of a circle represent- ing a traffic light, as shown in Figure 2. As part of this work, we enabled the use of VISB for XTL specifications, allowing for more advanced visualisations. We use the existing mechanism for loading B definition files containing VISB definitions, together with the specification file. Using VISB definitions, one can specify SVG objects and corresponding attribute value updates. 4 For the traffic light in Figure 2, the following definition registers an update of thefillattribute for the light with the SVG IDcars_red depending on the state propertytl_cars: VISB_SVG_UPDATES == rec(`id`: "cars_red", fill: IF STATE_PROPERTY("tl_cars") ∈"red", "red_yellow" THEN "red" ELSE "black" END). 4 A detailed summary of VISB’s syntax can be found athttps://prob.hhu.de/w/index.php?title=VisB. J. Gruteser, M. Leuschel, K. Engels & F. Vu153 Figure 4: VISB HTML Export for Connect Four Figure 5: State Space Visualisation for Listing 1 generated by PROB That is, if the traffic light indicatesredorred_yellowin the current state, the element is filled with red, otherwise with black colour. As VISB definitions are written in the B language, it is required to use the built-in functionSTATE_PROPERTY(Name)to access the value of a state property. In this context, Namecorresponds to a property of the special style’=’(Name,Value)(a way to mimic identifiers, cf. Listing 1). As with the animation function, it is possible to register click events for SVG objects. The following definition adds a click listener for the same element that triggers the eventswitch_tl_cars if the predicate is satisfied (the predicate can constrain the parameter values, hereNL, and the post state): VISB_SVG_EVENTS == rec(`id`: "cars_red", event: "switch_tl_cars", predicate: "NL = STRING_TO_TERM(\"red\")"). Our work introduces support for such event predicates, which are evaluated as B predicates. However, a solution was required to use parameter values provided as Prolog terms in the B predicate, since they do not correspond to valid B data types. We address this with a new built-in functionSTRING_TO_TERM, which wraps a B string and translates it to a data value of the typetermfor internal representation using basic Prolog functionality for reading terms from atoms. Hence, for the above definition, a click triggers the transitionswitch_tl_cars(red)(if enabled). Alternatively, one can provide the raw transition term directly, i.e.event: "switch_tl_cars(red)". Finally, the definition file must be linked in the XTL file usingprob_pragma_string("VISB_- DEFINITIONS_FILE",Path)or interactively in PROB2-UI. VISB offers an HTML trace export showing the visualisation for a state selected from the transitions. The transitions can be controlled manually or played automatically with a certain delay. The export has been made compatible with XTL models and extended by a table with the values of XTL state properties. Figure 4 shows a screenshot of a trace export for the Connect Four game (more details in Section 6). 154Animation, Verification and Visualisation of Prolog Transition Systems withPROB Graph Visualisation.PROB offers additional graph visualisations with its interface to Graphviz [16]. A feature of interest when dealing with Prolog transition system is visualising theexplored partof the state space by plotting all the states and transitions between them. Figure 5 shows the state space of the traffic light system. Other options include a graph showing the current trace and variations of the state space visualisation (e.g. highlighting the current state). 4 New Animation Features This section presents the new features added to the animator, primarily to address requirements arising from the new PROB sequent prover based on the XTL mode [12]. A state of the sequent prover consists of a set of hypotheses and a goal, where all of them are predicates in first-order logic. By applying proof rules that are encoded as XTL transitions, we aim to prove the goal based on the given hypotheses. Additionally to the sequent prover, this section introduces a further example application, PCTL model checking, to highlight the applicability of the features in a different context. 4.1 Transition Properties PROB allows one to store properties for transitions in the state space for B models. We adapted this mechanism for XTL models so that one can add arbitrary Prolog terms asdynamictransition properties (i.e. properties that can depend on parameter values and the state context in which the transition is available). For this purpose, we supplement the transition predicatetrans/3bytrans/4, which accepts a list of transition properties as its last parameter. The initial application includes user-friendly transition descriptions (for proof rule transitions), which is possible by adding a propertydescription/1. The descriptions are displayed in PROB’s GUIs, for example, at the top left of Figure 3, where chess move transitions are described by human-readable text. The (PCTL) example below includes a second dynamic transition property in addition todescription/1. Another type of transition properties isstaticproperties, which do not depend on the state context of a transition, but provide general information about a transition. For this purpose, we add the new special predicatetrans_prop/2, which accepts a transition name and a property of this transition (one can provide any number of predicates with properties). This predicate can be used, for example, to specify parameter names of a transition, e.g.trans_prop(t1,param_names([p1,p2])). Note that this restricts the arity of transitiont1to the length of the list of parameter names (2) and makes the transition known to the PROB animator as disabled, even if no outgoing transitions are available. This feature is useful forsymbolictransitions and trace replay, which we will describe in the following subsections. Application: PCTL Model Checking.Recent work has integrated a model checker for Probabilistic Computation Tree Logic (PCTL) into PROB for probabilistic model checking. With the new dynamic transition properties, probabilities can be easily assigned to transitions, for example: trans(tl_peds_green,lights(red,red),lights(green,red), [probability/0.6,description('switch pedestrian light to green')]). The probability could also be computed based on the state or parameter values. 4.2 Symbolic Transitions When exploring a state, PROB computes all possible outgoing transitions. However, some transitions require user input or have side effects that should not be triggered when searching for available transi- J. Gruteser, M. Leuschel, K. Engels & F. Vu155 tions. For example, this could involve the user-guided instantiation of a free identifier in a proof rule or the invocation of an external proof system. Motivated by this, we introduced the concept ofsym- bolictransitions. One can specify these transitions using the new predicatesymb_trans/3in the same way astrans/3, except that symbolic transitions are not automatically evaluated during animation and can be executed only using the “execute by predicate”-mechanism of PROB. The new predicatesymb_- trans_enabled(TransitionName,State)can be used to indicate whether a symbolic transition could potentiallybe enabled. Figure 6: Execute by Predicate in PROB2-UI Execute Transitions by Predicate.This technique was previously available for B machines only and al- lows the user to find and compute possible transi- tions for the specified parameter values and further state properties. We implemented a variation for XTL, where the inputs are the current state term, the desired transition name, optional parameter values and an ad- ditional B predicate. User input can be passed via the parameters or the additional predicate, as illustrated in Figure 6. This information is translated into a tran- sition term with the provided name as a functor and variables for the parameters. The implementation uni- fies the parameters with the provided values during evaluation of the transition candidates. If PROB finds a suitable candidate and the additional predicate is satisfied in the current state, it executes the corresponding transition. Application: Proof Rules.The newly introduced feature is indispensable for the sequent prover, since advanced proofs often depend on user input. It could be necessary to prove a goal that con- tains an existential quantifier. In particular, the user cannot make progress by applying the rule alone, as a suitable choice for the instantiation is required to proceed with the goal. The input (Inst) for the proof ruleexists_instmight look like in Figure 6. The evaluation yields the transition term exists_inst(' x | x∈S∧x/∈T '). In this case, however, the predicate stating that the proofGOALis true (⊤) is not satisfied. Therefore, PROB rejects the execution. 4.3 Trace Replay After manual animation or automated simulation, the animator holds a certain sequence, i.e. atrace, of transitions that have been performed to reach the current state. We aim to save the trace as a separate file to use it as a regression test. So far, a simplistic trace replay existed for the XTL mode, simply keeping the sequence of transition terms as a text file. However, this can be ambiguous. For instance, for each initial state, there is astart_xtl_systemtransition without parameters, which differs only in terms of the target state. Since PROB does not store these states in the standard trace format, it selects the first available transition with a matching name during replay, which results in an imprecise replay. Listing 3: Entry of a JSON Trace for an XTL Model "name": "switch_tl_cars", "params": "NL": "green" , "destState": "xtl_state": "lights(red,green)." To ensure correct trace replay, the JSON trace replay for B models has been reused and adapted for XTL. As a result, we can use interactive trace replay [17], i.e. a user can reproduce 156Animation, Verification and Visualisation of Prolog Transition Systems withPROB traces step by step and replace transitions. Each trace step corresponds to a JSON entry containing in- formation such as the transition name, the parameter values by their name and the destination state (cf. Listing 3). For B models, PROB stores the destination state in the fielddestState, which contains a map of machine identifiers to their values in the corresponding state. Since the concept of identifiers is not applicable in XTL mode, PROB now stores the raw destination state term with the special identifier xtl_state. For symbolic transitions, trace steps are replayed with the “execute by predicate” feature to unify user-provided values with the parameter variables. Application: Replay of Proofs.The improved trace replay enhances the reproducibility of proofs with the sequent prover. In some cases, a proof resembles an existing one, differing only in specific transitions which can be replaced during interactive trace replay. On the other hand, if the user provides parameter values, the extended replay mechanism allows one to reload the corresponding trace without further interaction and manual adjustments by the user. 5 Simulation PROB2-UI offers a simulation feature for B models called SIMB [43]. Its support has been extended for XTL, allowingsimulationof XTL transition systems. This extension enables one to apply validation techniques such as Monte Carlo simulations with hypothesis testing and other statistical measures. Listing 4: SimB Activation in JSON 1"id": "place", 2"execute": "place", 3"after": 10, 4"fixedVariables": 5"player": "STRING_TO_TERM(\"yellow\")" 6, 7"transitionSelection":"uniform", 8"activating": ["auto_play_minimax"] Timed Probabilistic Simulation.SIMB intro- duces a concept to simulate formal models with timing and probabilistic behaviour, referred to astimed probabilistic simulation. The concept builds onactivationsthat execute an action after a specific time and subsequently trigger other ac- tivations. In particular, one can specify how mul- tiple activations trigger one another, or how to choose between multiple activations probabilisti- cally. Listing 4 shows an example of an activation for Connect Four, which represents a random player. The player places a yellow disc through theplace event (after 10ms) at a random position, which is chosen uniformly (indicated by line 7). Afterwards, theauto_play_minimaxactivation is triggered, which performs a move found by theMinimax strategy (cf. Section 6). Through theactivatingattribute, SIMB simulates the entire game automatically, with the random and Minimax player triggering one another. Listing 5: SimB Listener in JSON 1"id": "player", 2"event": "place", 3"activating" : ["auto_play_minimax"] Interactive Simulation.Interactive simulation[42] is an extended feature in SIMB which allows one to trigger simulations interactively. Technically, SIMB’s activation concept is extended bylisteners, which are reactive elements that (1) monitor whether an event is performed through animation, and (2) trigger an activation afterwards. With this feature, one can sep- arate interactive and automatic components of a system and specify automatic processes triggered by a user event. For example, users can play games such as Chess, Connect Four and Tic-Tac-Toe against au- tomated strategies encoded in the XTL model: the user’s move (seeplacein line 2 of Listing 5) triggers the autoplay transition (see line 3 of Listing 5), after which the listener waits for the next manual move. J. Gruteser, M. Leuschel, K. Engels & F. Vu157 Figure 7: Monte Carlo Simulation PROB2-UI Monte Carlo Simulation.Based on SIMB’s auto- matic simulation features, one can perform Monte Carlo simulations with a specific number of execution runs. One can specify an ending condition, specifying when each execution run stops. Afterwards, one can formu- late certain properties or expressions and use them for hypothesis testing and value estimation. Due to the high number of runs in the Monte Carlo simulation, the user gains statistical confidence about the fulfilment of a property with a specific probability, or that an estimated value is within a desired range. Figure 7 shows a configuration for 10,000 runs, which evaluates a heuristic function in the final state and performs a two-tailed hypothesis test expecting that the predicate is satisfied with 50%. Traces from a Monte Carlo simulation can be saved using the new JSON trace ex- port feature and then inspected individually. In Section 6, we apply Monte Carlo simulations to evaluate strategies with the game Connect Four. 6 Case Study: Game Play In the following, we demonstrate the new simulation feature of SIMB for XTL models. Therefore, we discuss another use case where the logic ofturn-based, deterministic, zero-sum games with perfect infor- mation, such as chess, Connect Four and Tic-Tac-Toe, is encoded in XTL. In addition to the game logic, the specification also contains the AI, implemented as Minimax search [30] with alpha-beta pruning [20] and Monte Carlo Tree Search (MCTS) [11, 9]. More precisely, for each game, there are predicates for (1) playing one move manually, (2) playing one Minimax move (auto_play_minimax), and (3) playing one MCTS move (auto_play). We use SIMB to evaluate game strategies, in which a random player, a Minimax player, and an MCTS player play against each other. When comparing different strategies, the focus is on determining the optimal move and teaching a computer to make that move. For this, agame treeis constructed, with each node representing a player’s decision, and each path from the root to a leaf signifying a potential game outcome. With theMinimaxsearch strategy, we assume that our opponent will play the best possible move and then choose the best move for ourselves. That is, we alternate between minimising and maximising levels of the game tree, computing the values for each node bottom-up. For perfect play, one would have to expand the game tree until reaching a final state. As this is not feasible due to the exponential growth, the search stops after reaching a certain depth. Minimax uses a value (or heuristic) function to estimate the outcome. Additionally, our Minimax implementation uses a random ordering to improve the performance of alpha-beta pruning. Theoretical Minimax, when fully searched, ensures perfect play, allowing the first player to win always [30, 9]. Monte Carlo Tree Search(MCTS) is an alternative approach that searches the game tree by executing simulations from the current state until a player wins. Initially, MCTS chooses actions randomly, but as the process continues, data on node visitation frequencies and win rates refine the choice of actions, leading to progressively less randomness. With an increasing number of simulations, MCTS approaches optimal play and achieves perfect results with an infinite number of simulations [7]. The PROB examples [13] contain generic implementations of Minimax and MCTS that can be in- cluded into any XTL game specification, provided that the necessary predicates for the value function and game moves are available. As a particular example and a classic game for AI benchmarks [3], we examine Connect Four. In Connect Four, two players take turns placing discs in the columns. The aim is 158Animation, Verification and Visualisation of Prolog Transition Systems withPROB Table 1: Simulation Results for Connect Four (10,000 or †1,000 runs) Percentage of Wins by the First Player (1), Average Trace Length and Total Duration of the Simulations First MoveFree ChoiceFixed(Middle Column) [% length min. ] 2 1 RandomMinimaxMCTSRandomMinimaxMCTS Random55.7 22.3 13.1 96.0 18.0 21.9 100.0 9.7 266.3 64.4 21.8 11.2 97.3 16.3 13.4 100.0 9.7 214.9 Minimax 7.3 20.3 18.3 46.8 30.7 20.6 98.9 19.5 511.0 9.9 21.4 19.7 52.0 29.8 19.7 98.8 19.8 443.5 MCTS 0.0 12.5 373.9 0.5 24.5 730.0 † 44.2 32.8 147.3 0.0 14.6 403.6 1.1 25.6 718.8 † 47.1 32.9 153.8 to be the first player to get four discs in a horizontal, vertical, or diagonal row. The game is solved [4], meaning the outcome is predictable from any state with perfect play. The first player can force a win by starting in the middle column; other statements can be made if they choose one of the adjacent columns. For evaluation, we consider random play, Minimax with a search depth of two moves and MCTS (without any time limit per move). We conducted 10,000 Monte Carlo simulations (i.e. matches) for each combination of the three strategies, once with the first move chosen freely and once with it fixed to the middle column. We then evaluated the probability of the first player winning. One could either perform a hypothesis test to validate the expected probability, or use an estimator to estimate the average final value of the heuristic function (ranging from -1 for loss to 1 for win). Figure 7 shows an example configuration. We encode the SIMB activations as described in Section 5. In addition, we evaluate the average trace length (i.e. the number of moves, top right) and the performance in terms of execution time (bottom right). The results are presented in Table 1. Obviously, a random player has almost no chance against Minimax and no chance at all against MCTS. The weakness of Minimax is likely due to the shallow search depth we chose. Taylor and Stella [35] come to a similar conclusion for Minimax with depth three. This result also becomes evident when comparing Minimax against MCTS, where MCTS won around 99% of the games. However, this result was expected as outlined by Sheoran et al. [32], who compared an optimised Minimax algorithm with MCTS. The results of the comparison between random and MCTS are also the same (100%). They claim that with increasing search depth (four and five), Minimax can beat MCTS in more than 60%. Using a sample of 100 games, we could indeed show that the probability for Minimax wins increases from a depth of five onwards, although performance decreases. Interestingly, the results show that the first player does indeed have an advantage in a random vs. random match. However, further research is needed to determine why this is not the case with Minimax and MCTS. As expected, the probability of winning increases for all strategies if we restrict the first move to the middle column. The performance is satisfactory for random and Minimax (partly due to the small search depth). It was possible to simulate 10,000 matches in less than 20 minutes without any issues. MCTS, on the other hand, slows down significantly, resulting in run times of several hours. Depending on the number of remaining moves, the computation times per move can reach up to 500 ms. An interesting finding is that MCTS only requires an average of 9.7 moves to beat the random player, whereas Minimax requires 18.0 and a random opponent 22.3 moves. One can perform similar evaluations on the other implemented games. For games with a manageable state space, model checking is another exploration method. For instance, PROB model checks the Tic- Tac-Toe model in approximately 200 ms, analysing 5478 states and 16168 transitions. Our model is available online together with the other games [14]. J. Gruteser, M. Leuschel, K. Engels & F. Vu159 7 Practical Applications and Related Work The XTL mode has been used for teaching in several iterations of our university courses covering both introductory and advanced topics on logic programming. The modelling of small systems is taught to first-year Prolog students. With the XTL mode, it is easy to switch from pure code to an experimental mode where students can repeatedly test their own implementations. Complementary visualisations can help students better understand the system’s state. Unlike approaches using interactive documents, such as Jupyter notebooks [8, 31] or active learning documents [29], the XTL mode enables exploration of a Prolog model within a formal verification tool. Similar to our case study, Krings and Körner [21] propose to formalise the rules of games in the context of teaching formal methods. Our advanced course on logic programming involves a project in which the students develop an interpreter in Prolog. The XTL mode is particularly well suited to this task because semantic rules can be easily implemented and immediately tested (cf. Section 2). In recent years, interpreters have been implemented for subsets of Java bytecode, Petri nets and WebAssembly. There exist further applications, such as for model checking of security protocols [36]. More exam- ples are available in the PROB examples collection [13]. Sterling et al. [34] implemented a compiler from Z to readable Prolog code for animating formal specifications. In another related work, a Prolog-based animator for the Verilog Hardware Description Language has been developed [7]. Körner et al. [22] discussed the performance of bytecode interpreters implemented in Prolog. CLINGRAPH[18] is a visualisation tool foranswer set programming(ASP) using Graphviz [16]. In particular, CLINGRAPHsupports SVG visualisation of the computed solutions, dynamic problems (whose solutions are similar to a trace in formal methods), and the program structure. Another visualisa- tion tool is ASPVIZ [10] which allows one to present ASP solutions from a domain-specific perspective. Using ASPVIZ, one can also visualise the solutions as an animation (in the context of computer graph- ics, i.e., a sequence of frames). Bertagnon and Gavanelli present ASPECT [6], which is a sub-language of ASP that can be used to present the solver’s output graphically. Using ASPECT, the results can be converted to L A T E X to produce vector graphics. Another tool to visualise and debug Prolog programs is PrettyCLP [33]. Its visualisation features include SLD trees and and CLPFD constructs. PROB also supports domain-specific visualisations of the underlying system based on SVG graphics. The main difference is that PROB treats XTL programs as a state-based formalism, the other tools focus on the presentation of the ASP solutions. 8 Conclusion In this work, we presented the capabilities of PROB’s XTL mode for animating transition systems speci- fied in Prolog. We demonstrated new features, in particular, improved state visualisation and simulation applied to a detailed study of strategies with the Connect Four game. We argue that XTL provides a simple and flexible interface for validating and verifying Prolog transition systems, especially suited for writing simple interpreters to quickly connect other (formal) languages to the PROB tooling. One key application involves the sequent prover, which we intend to enhance in the future using an iterative deepening approach, similar to the games involving automatic proof strategies. With our new simulation for XTL models and Monte Carlo simulations in particular, we can validate Prolog specifications and obtain indications of potential weaknesses in our implementation, e.g., Mini- max losing against a random player in a few scenarios. In the future, we plan to evaluate game strategies using AI-driven simulations via SIMB’s interface to external simulations [39], such as a reinforcement learning agent that controls the simulation. 160Animation, Verification and Visualisation of Prolog Transition Systems withPROB References [1] Jean-Raymond Abrial (2005):The B-Book: Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162. [2] Jean-Raymond Abrial (2010):Modeling in Event-B: System and Software Engineering. Cambridge Univer- sity Press, doi:10.1017/CBO9781139195881. [3] Mohammed Alaa Ala’anzy, Akerke Madiyarova, Aidos Aigeldiyev, Raiymbek Zhanuzak & Omar Alnaseri (2026):Connect-4 AI: A Comprehensive Taxonomy and Critical Review of Methods and Metrics.Symmetry 18(2), doi:10.3390/sym18020293. Available athttps://w.mdpi.com/2073-8994/18/2/293. [4] Victor Allis (1988):A Knowledge-based Approach of Connect-Four, The Game is Solved: White Wins. Avail- able athttps://tromp.github.io/c4/connect4_thesis.pdf. [5] Jens Bendisposto, David Geleßus, Yumiko Jansing, Michael Leuschel, Antonia Pütz, Fabian Vu & Michelle Werth (2021):ProB2-UI: A Java-based User Interface for ProB. In:Proceedings FMICS, LNCS 12863, p. 193–201, doi:10.1007/978-3-030-85248-1_12. [6] Alessandro Bertagnon & Marco Gavanelli (2024):ASPECT: Answer Set rePresentation as vEctor graphiCs in laTex.Journal of Logic and Computation34(8), p. 1580–1607, doi:10.1093/logcom/exae042. [7] Jonathan Bowen (1999):Animating the Semantics of VERILOG using Prolog.UNU/IIST Report No. 176. [8] Anne Brecklinghaus & Philipp Körner (2022):A Jupyter Kernel for Prolog. In:Proceedings 36th Work- shop on (Constraint) Logic Programming (WLP 2022). Lecture Notes in Informatics (LNI), Gesellschaft für Informatik, Bonn. [9] Cameron B. Browne, Edward Powley, Daniel Whitehouse, Simon M. Lucas, Peter I. Cowling, Philipp Rohlf- shagen, Stephen Tavener, Diego Perez, Spyridon Samothrakis & Simon Colton (2012):A Survey of Monte Carlo Tree Search Methods.IEEE Transactions on Computational Intelligence and AI in games4(1), p. 1–43, doi:10.1109/TCIAIG.2012.2186810. [10] Owen Cliffe, Marina De Vos, Martin Brain & Julian Padget (2008):ASPVIZ: Declarative Visualisa- tion and Animation Using Answer Set Programming. In:Logic Programming, Springer, p. 724–728, doi:10.1007/978-3-540-89982-2_65. [11] Rémi Coulom (2006):Efficient Selectivity and Backup Operators in Monte-Carlo Tree Search. In:Proceed- ings CG,LNCS4630, Springer, p. 72–83, doi:10.1007/978-3-540-75538-8_7. [12] Katharina Engels, Jan Gruteser & Michael Leuschel (2026):Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB. In:Proceedings ICLP, EPTCS. To appear. [13] Software Engineering & Programming Languages Group – Heinrich Heine University Düsseldorf:ProB Examples. Available athttps://stups.hhu-hosting.de/downloads/prob/source/ProB_public_ examples.tgz. [14] Software Engineering & Programming Languages Group – Heinrich Heine University Düsseldorf (2026): XTL Examples. Available athttps://github.com/hhu-stups/xtl_examples. [15] Berndt Farwer & Michael Leuschel (2004):Model Checking Object Petri Nets in Prolog. In:Proceedings PPDP, p. 20–31, doi:10.1145/1013963.1013970. [16] Emden R. Gansner (2011):Drawing graphs with Graphviz. Technical Report. [17] Jan Gruteser & Michael Leuschel (2025):Interactive Trace Replay for Event-B Models. In:12th Rodin User and Developer Workshop. Available athttps://eprints.soton.ac.uk/id/eprint/503334. [18] Susana Hahn, Orkunt Sabuncu, Torsten Schaub & Tobias Stolzmann (2024):Clingraph:A Sys- tem for ASP-based Visualization.Theory and Practice of Logic Programming24(3), p. 533–559, doi:10.1017/S147106842400005X. [19] Gerard J. Holzmann (1997):The Model Checker SPIN.IEEE Transactions on Software Engineering23(5), p. 279–295, doi:10.1109/32.588521. J. Gruteser, M. Leuschel, K. Engels & F. Vu161 [20] Donald E. Knuth & Ronald W. Moore (1975):An Analysis of Alpha-Beta Pruning.Artificial Intelligence 6(4), p. 293–326, doi:10.1016/0004-3702(75)90019-3. [21] Sebastian Krings & Philipp Körner (2019):Prototyping Games Using Formal Methods. In:Proceedings FMFun,CCIS1301, Springer, p. 124–142, doi:10.1007/978-3-030-71374-4_6. [22] Philipp Körner, David Schneider & Michael Leuschel (2020):On the Performance of Bytecode Interpreters in Prolog. arXiv:2008.12543. [23] Michael Leuschel (2001):Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog. In:Proceedings PADL,LNCS1990, Springer, p. 14–28, doi:10.1007/3-540-45241-9_2. [24] Michael Leuschel & Jens Bendisposto (2010):Directed Model Checking for B: An Evaluation and New Techniques. In:Proceedings SBMF,LNCS6527, Springer, p. 1–16, doi:10.1007/978-3-642-19829-8_1. [25] Michael Leuschel & Michael J. Butler (2008):ProB: an automated analysis toolset for the B method.STTT 10(2), p. 185–203. Available athttp://dx.doi.org/10.1007/s10009-007-0063-9. [26] Michael Leuschel & Thierry Massart (1999):Infinite State Model Checking by Abstract Interpre- tation and Program Specialisation.In:Proceedings LOPSTR,LNCS1817, Springer, p. 62–81, doi:10.1007/10720327_5. [27] Michael Leuschel & Thierry Massart (2002):Logic Programming and Partial Deduction for the Verifica- tion of Reactive Systems: An Experimental Evaluation. Available athttps://eprints.soton.ac.uk/ 257666/1/Avocs2002.pdf. [28] Kenneth L. McMillan (1993):The SMV System. In:Symbolic Model Checking, Springer, p. 61–85, doi:10.1007/978-1-4615-3190-6_4. [29] Jose F. Morales, Salvador Abreu, Daniela Ferreiro & Manuel V. Hermenegildo (2023):Teaching Prolog with Active Logic Documents. In:Prolog: The Next 50 Years,LNCS6527, p. 171–183, doi:10.1007/978-3-031- 35254-6_14. [30] John von Neumann (1928):Zur Theorie der Gesellschaftsspiele.Mathematische Annalen100(1), p. 295– 320, doi:10.1007/BF01448847. [31] Galileo Sartor & Adam Wyner (2025):Teaching Prolog and Logic Programming with Jupyter Notebooks. In:Proceedings of the 41st ICLP Workshops. [32] Kavita Sheoran, Geetika Dhand, Mayank Dabaszs, Nishthavan Dahiya & Pratish Pushparaj (2022):Solving Connect 4 Using Optimized Minimax and Monte Carlo Tree Search.Advances and Applications in Mathe- matical Sciences21(6), p. 3303–3313, doi:10.4236/am.2023.146025. [33] Alessio Stalla, Davide Zanucco, Agostino Dovier, Viviana Mascardi et al. (2011):PrettyCLP: a Light Java Implementation for Teaching CLP.In:Proceedings CILC, p. 281–295. Available athttps://ceur-ws. org/Vol-810/paper-l17.pdf. [34] Leon Sterling, Paolo Ciancarini & Todd Turnidge (1996):On the animation of “not executable” specifica- tions by Prolog.International Journal of Software Engineering and Knowledge Engineering6(1), p. 63–87, doi:10.1142/S0218194096000041. [35] Henry Taylor & Leonardo Stella (2024):An Evolutionary Framework for Connect-4 as Test-Bed for Com- parison of Advanced Minimax, Q-Learning and MCTS. arXiv:2405.16595. [36] Miles Vella:Model Checking Security Protocols with ProB. Available athttps://stups.hhu-hosting. de/theses/master/Vella_security_protocols_thesis_2025.pdf. [37] Fabian Vu:Simulation and Verification of Reactive Systems in Lustre with ProB. Available athttps:// stups.hhu-hosting.de/theses/master/Masterarbeit_Fabian_Vu.pdf. [38] Fabian Vu, Dominik Brandt & Michael Leuschel (2022):Model Checking B Models via High-level Code Generation. In:Proceedings ICFEM, LNCS 13478, p. 334–351, doi:10.1007/978-3-031-17244-1_20. [39] Fabian Vu, Jannik Dunkelau & Michael Leuschel (2024):Validation of Reinforcement Learning Agents and Safety Shields with ProB. In:Proceedings NFM,LNCS14627, Springer, p. 279–297, doi:10.1007/978-3- 031-60698-4_16. 162Animation, Verification and Visualisation of Prolog Transition Systems withPROB [40] Fabian Vu, Dominik Hansen, Philipp Körner & Michael Leuschel (2019):A Multi-target Code Generator for High-Level B. In:Proceedings iFM, LNCS 11918, p. 456–473, doi:10.1007/978-3-030-34968-4_25. [41] Fabian Vu, Christopher Happe & Michael Leuschel (2024):Generating interactive documents for domain- specific validation of formal models.International Journal on Software Tools for Technology Transfer26(2), p. 147–168, doi:10.1007/s10009-024-00739-0. [42] Fabian Vu & Michael Leuschel (2023):Validation of Formal Models by Interactive Simulation. In:Proceed- ings ABZ,LNCS14010, Springer, p. 59–69, doi:10.1007/978-3-031-33163-3_5. [43] Fabian Vu, Michael Leuschel & Atif Mashkoor (2021):Validation of Formal Models by Timed Probabilistic Simulation. In:Proceedings ABZ,LNCS12709, p. 81–96, doi:10.1007/978-3-030-77543-8_6. [44] Michelle Werth & Michael Leuschel (2020):VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics. In:Proceedings ABZ,LNCS12071, Springer, p. 260–265, doi:10.1007/978-3-030-48077-6_21.