VMDV: A 3D Visualization Tool for Modeling, Demonstration, and Verification

TL;DR

This paper introduces VMDV, a 3D visualization tool designed to make the structure of models and verification procedures more understandable, especially in theorem proving and model checking contexts.

Contribution

The paper presents a novel 3D visualization tool that enhances comprehension of models and verification processes in automated theorem proving and model checking.

Findings

VMDV effectively visualizes proof systems.

Improves understanding of complex verification procedures.

Facilitates model analysis through 3D visualization.

Abstract

The output of an automated theorem prover is usually presented by using a text format, they are often too heavy to be understood. In model checking setting, it would be helpful if one can observe the structure of models and the verification procedures. A 3D visualization tool (\textsf{VMDV}) is proposed in this paper to address these problems. The facility of \vmdv is illustrated by applying it to a proof systems.

Equations

$$\scriptsize\begin{array}[]{@{}lll@{}}\vdash P(s_{1},...,s_{n})&\hskip 14.22636pt\vdash\neg P(s_{1},...,s_{n})&\hskip 14.22636pt\vdash\top\vspace{2mm}\par\\ \vdash\phi_{1}\wedge\phi_{2}\lx@proof@logical@and\vdash\phi_{1}\vdash\phi_{2}&\hskip 14.22636pt\vdash\phi_{1}\vee\phi_{2}\vdash\phi_{1}&\hskip 14.22636pt\vdash\phi_{1}\vee\phi_{2}\vdash\phi_{2}\vspace{2mm}\\ \vdash EX_{x}(\phi)(s)\vdash(s^{\prime}/x)\phi&\lx@intercol\hskip 14.22636pt\vdash AX_{x}(\phi)(s)\lx@proof@logical@and\vdash(s_{1}/x)\phi\ldots\vdash(s_{n}/x)\phi\hfil\lx@intercol\vspace{2mm}\\ \Gamma\vdash AF_{x}(\phi)(s)\vdash(s/x)\phi&\lx@intercol\hskip 14.22636pt\Gamma\vdash AF_{x}(\phi)(s)\lx@proof@logical@and\Gamma\vdash AF_{x}(\phi)(s_{1})\ldots\Gamma\vdash AF_{x}(\phi)(s_{n})\hfil\lx@intercol\vspace{2mm}\\ \lx@intercol\Gamma\vdash EG_{x}(\phi)(s)\lx@proof@logical@and\vdash(s/x)\phi\Gamma,EG_{x}(\phi)(s)\vdash EG_{x}(\phi)(s^{\prime})\hfil\lx@intercol&\Gamma\vdash EG_{x}(\phi)(s)\vspace{2mm}\\ \lx@intercol\hfil\Gamma\vdash AR_{x,y}(\phi_{1},\phi_{2})(s)\lx@proof@logical@and\vdash(s/y)\phi_{2}\Gamma^{\prime}\vdash AR_{x,y}(\phi_{1},\phi_{2})(s_{1})~{}...~{}\Gamma^{\prime}\vdash AR_{x,y}(\phi_{1},\phi_{2})(s_{n})\hfil\lx@intercol\vspace{2mm}\\ \lx@intercol\Gamma\vdash AR_{x,y}(\phi_{1},\phi_{2})(s)\lx@proof@logical@and\vdash(s/x)\phi_{1}\vdash(s/y)\phi_{2}~{}~{}~{}~{}~{}~{}~{}~{}\Gamma\vdash AR_{x,y}(\phi_{1},\phi_{2})(s)\hfil\lx@intercol\vspace{2mm}\\ \lx@intercol\Gamma\vdash EU_{x,y}(\phi_{1},\phi_{2})(s)\vdash(s/y)\phi_{2}~{}~{}~{}~{}~{}~{}~{}\Gamma\vdash EU_{x,y}(\phi_{1},\phi_{2})(s)\lx@proof@logical@and\vdash(s/x)\phi_{1}\Gamma\vdash EU_{x,y}(\phi_{1},\phi_{2})(s^{\prime})\hfil\lx@intercol\end{array}$$

$$E{U}_{x,y}(safe(x),complete(y),S_0)$$

Full text

1 Introduction

In the field of mathematical logic, a formal proof is usually defined as a sequence of formulas, which are either axioms or logical consequences of the preceding formulas. In the most natural way, a proof is generally presented as a proof tree, where each node is labelled by a formula, and its sub-nodes are the hypothesises. Nowadays, one can obtain proofs from computers automatically, thanks to the development of automated theorem provers. However, the outcome of a theorem prover is usually displayed in text format. This usually makes the proof tree difficult to understand (e.g., to observe the relative locations of some nodes in the same proof tree), especially when the proof tree contains a large set of nodes. The same problem also arises in the field of model checking [1], where the counterexample generated by model checkers are usually hard to read. A more readable form will be helpful to engineers who are not familiar with model checking [5]. Text format is difficult to show the structures when proof trees are dynamically updated. This is very common in a proving procedure, where the nodes may be dynamically created or deleted. Then the following questions arises that motivate our work:

How to enable the output of a theorem prover to carry huge amount of information, and at the same time be easy to understand and reason about? 2. 2.

How to observe the verification procedure when checking a proof tree in an intuitive manner?

To answer the previous questions, a 3D visualization tool, called VMDV (Visualization for Modeling, Demonstration, and Verification), is proposed in this paper. VMDV employs a 3D renderer to plot proof trees in 3D space. In this way, the original text format is easily organized and displayed. Local detail text information adheres then to the node on demand. VMDV is based on the 3D information visualization techniques. As is well known, 3D information visualization techniques take advantage of the human eyes’ broad bandwidth pathway into the mind to allow users to capture large amounts of information at once. In our case, VMDV represents the proofs by 3D trees (Fig. 1). In the following figure, the 2D format is much more convenient to reflect the structure of the proof tree than the text format. However, when the number of nodes becomes large, there would not be enough space to show the labels of each node in 2D format. 3D format, on the other hand, can use space much more efficiently than 2D format when the nodes becomes large enough, by showing clearly both the structure of the graph, and the labels of each node. In this situation, 3D format can be seen as the combination of multiple 2D spaces in a consistent manner.

VMDV allows the observation either from a global perspective or a local one. The global view shows the shape, or the topological structure while the local view shows the detailed information of interesting nodes or sub-structures (Fig. 4).

VMDV also enables us a variety of manners to observe or interact with the proof tree. The zooming and rotation operations effectively change the viewport, making the presentation of the overall structure of the proof tree clear via different angles of view (Fig. 5); when the proof tree is very large and only a subtree is interesting, this subtree can be selected and get focused with other parts of the tree hidden; nodes with specific pattern can be searched and highlighted on the proof tree (Fig. 6), etc. This allows us to find, among others, all the formulas from which one specific formula can be inferred or deduced.

In some proof systems, there may be some auxiliary structures emerging along with the construction of proof trees, such as Kripke models or inductively defined terms. VMDV enables the visualization of both proof trees and auxiliary structures, and the interaction between proof trees and the auxiliary structures may help better understand the proving procedure.

As a visualization tool, VMDV is designed and implemented as a stand-alone program, not as a part of specific proof systems. Proof systems and VMDV communicate via TCP sockets. This facilitate the extensibility of VMDV to different proof systems. Design such a visualization interface for existing proof systems such as Coq is our future work.

Related Work.

As far as we know, many efforts have been made to the visualization of the output of theorem provers. For instance, in [10, 4, 17, 18], proofs are presented in graph format instead of lines of text, and colors are used to highlight crucial parts of a proof tree; [13] proposed several criteria for the visualization of proof trees, such as distinguishing different kinds of rules, following the progress of subproofs, focusing on different aspects of the proof, etc; and [2] has explored the visualization of both proof trees, and other data structures such as expressions. Our work is different from the existing visualization tools: Firstly, we render the graphs in 3D format, instead of 2D format in most of the existing visualization tools. Rendering in 3D space enables the visualization of graphs with complicated structures that are usually difficult to view in 2D space. For instance, in 2D space, the graph will be confusing with hundreds of nodes, whereas in 3D space, we can demonstrate the structure of the graph with thousands of nodes clearly. Secondly, even though some of the existing visualization tools [10, 2] use 3D libraries, their layout algorithms are rather limited to graphs with simple structures. Instead, we use an automatic layout algorithm which simulates a physical system where nodes repulse each other, much like magnets while edges attract the nodes that they connect, much like springs. This algorithm is capable of handling the layout of the proof tree smoothly, where nodes may be hidden, created, or deleted during a proving procedure.

The rest of the paper is organized as follows: Section 2 presents the preliminaries of this paper, including some basic notions of information visualization, and the brief introduction of a proof system. Section 3 introduces our visualization tool VMDV. Section 4 involves the applications of VMDV to the proof system. Section 5 concerns conclusion and future works.

2 Preliminaries

We present the concept of information visualization, and a proof systems in sequent calculus style. The interested reader is referred to [7] for further details.

2.1 Information Visualization

Information visualization is the study of visual representation of abstract data that focus on the creation of approaches for humans to capture abstract information intuitively. With the visual representations of data, it is easier for humans to get a deeper understanding, and gain the essentials over the massive data-sets.

Benefit from the study of computer graphics, information presentation using visualization has been enjoying popular support. The Open Graphics Library (OpenGL) provides a language independent and cross-platform application programming interface (API) for the rendering of three dimensional graphics. As for the hardware, the enhancing of the computational power of Graphics Processing Units (GPU) has made the efficient rendering of complex graphics a reality. As opposed to digital numbers which are more readable for computers, Visualization systems are more friendly to human beings for providing both concrete and abstract inspirations. For instance, plotted charts are better understandable than bare data-sets. It assists in uncovering the trends, reveal insights, or even tell stories. Information visualization provides a easier way for users to capture the abstract patterns of the massive data by applying a graphical presentation.

We applied the ideas of information visualization to the development of VMDV, as it provides:

• •

The presentation of data in 3D space, where the data points are encoded as 3D solid spheres, and the structure of data are encodes as lines between spheres;

• •

Visual interaction with data, such as highlighting the search results for specific data, or controlling the progress of producing new data.

2.2 The System SCTL

Model checking [6, 8, 9] and automated theorem proving [11, 14] are two major pillars of formal verification methods. The proof system SCTL, introduced in [7], is a sequent calculus for Computation Tree Logic (CTL) [8, 9], taking a Kripke model as parameter. SCTL performs verification directly on a given Kripke model from the perspective of automated theorem proving, and produces formal proofs when the verification procedure terminates.

The syntax of SCTL is stipulated as follows. The properties of a Kripke model are expressed in a language tailored for this model. The language contains, for each state $s$ of the model, a constant also written $s$; for each relation $P$ over the model, a predicate symbol, also written $P$. Formulas are built in the usual way with the connectors $\top$, $\bot$, $\wedge$, $\vee$ and $\neg$, to which we add modalities $AX$, $EX$, $AF$, $EG$, $AR$, and $EU$. If $\phi$ is a formula, and $t$ is either a constant or a variable, then $AX_{x}(\phi)(t)$, $EX_{x}(\phi)(t)$, $AF_{x}(\phi)(t)$, and $EG_{x}(\phi)(t)$ are formulas. Like quantifiers, modalities bind the variable $x$ in $\phi$. If $\phi_{1}$ and $\phi_{2}$ are formulas and $t$ is either a constant or a variable, then $AR_{x,y}(\phi_{1},\phi_{2})(t)$ and $EU_{x,y}(\phi_{1},\phi_{2})(t)$ are formulas. These modalities bind the variable $x$ in $\phi_{1}$ and $y$ in $\phi_{2}$.

The semantics of a SCTL formula is defined as follows, and the proof rules for the system SCTL is depicted in Fig. 2.

Definition 1 (Valid formula)

Let $\mathcal{M}$ be a model and $\phi$ be a closed formula, the set of valid formulas $\models\phi$ in the model $\mathcal{M}$ is defined by induction on $\phi$:

• •

$\models P(s_{1},...,s_{n})$, if $\langle s_{1},...,s_{n}\rangle\in P$;       $\models\neg P(s_{1},...,s_{n})$, if $\langle s_{1},...,s_{n}\rangle\notin P$,

• •

$\models\top$,       $\models\bot$ is never the case;

• •

$\models\phi_{1}\wedge\phi_{2}$, if $\models\phi_{1}$ and $\models\phi_{2}$,

• •

$\models\phi_{1}\vee\phi_{2}$, if $\models\phi_{1}$ or $\models\phi_{2}$,

• •

$\models AX_{x}(\phi_{1})(s)$, if for each state $s^{\prime}$ in $Next(s)$, $\models(s^{\prime}/x)\phi_{1}$,

• •

$\models EX_{x}(\phi_{1})(s)$, if there exists a state $s^{\prime}$ in $Next(s)$ such that $\models(s^{\prime}/x)\phi_{1}$,

• •

$\models AF_{x}(\phi_{1})(s)$, if for all infinite paths $s_{0},s_{1},...$ starting from $s$, there exists a natural number $i$, such that $\models(s_{i}/x)\phi_{1}$,

• •

$\models EG_{x}(\phi_{1})(s)$, if there exists an infinite path $s_{0},s_{1},...$ starting from $s$, such that for all natural numbers $i$, $\models(s_{i}/x)\phi_{1}$,

• •

$\models AR_{x,y}(\phi_{1},\phi_{2})(s)$, if for all infinite paths $s_{0},s_{1},...$ starting from $s$, and for all $j$, either $\models(s_{j}/y)\phi_{2}$ or there exists an $i<j$ such that $\models(s_{i}/x)\phi_{1}$,

• •

$\models EU_{x,y}(\phi_{1},\phi_{2})(s)$ if there exists an infinite path $s_{0},s_{1},...$ starting from $s$ and a natural number $j$ such that $\models(s_{j}/y)\phi_{2}$ and for all $i<j$, $\models(s_{i}/x)\phi_{1}$.

3 VMDV

3.1 Architecture

In the design of VMDV , the proof system does not know exactly how VMDV renders graphs, and VMDV does not know the working procedure of the proof system. The proof system simply sends output information to the VMDV, and gets the manipulation feedbacks from it. As is shown in Fig. 3, there are two kinds of messages interchanged by a proof system and VMDV : the Visualization Messages sent by VMDV , and the Graph Update Messages sent by the proof system. Visualization Messages are control messages consist of requiring the related information of the current formula, such as the hypothesis, sub-formulae, or other specific information (e.g., the related state in an SCTL formula). Graph Update Messages are data messages consist of the responds to the control messages. VMDV serves as the interface to dynamically visualize the output of the proof system. The relationship of a VMDV with a proof system is very similar to that of a web browser and a web server. In order to extend the applications of VMDV to other proof systems, VMDV is designed and implemented as a stand-alone program, not as a part of specific proof systems. Proof systems and VMDV communicate via TCP sockets. Both control and data messages are wrapped as TCP packets. This way, VMDV can easily communicate with proof systems implemented in different programming languages, or run in different computers in networks.

Note that VMDV allows multiple outputs to visualize multiple structures, proof trees, or, e.g., Kripke models in SCTL system.

VMDV is implemented in Java111https://www.oracle.com/java/index.html and rendered using JOGL,222http://jogamp.org/jogl/www/ the Java binding of the OpenGL API.

3.2 Interfaces

Fig. 4 shows a typical screenshot of VMDV. It consists of two panels: the main panel on the top shows the overall structure of the proof tree, and the panel at the bottom shows the details of the selected nodes.

Similar to other 3D visualization tools, VMDV adopts some commonly used operations (for instance, zooming, rotation, and selection) for users to interact with 3D graphs. Furthermore, VMDV provides mechanisms to extend its functionalities to fulfill the special requirements of different kinds of proof systems.

Zooming and rotation. The most obvious advantage of 3D visualization over 2D one is the capacity of observing a graph from different angles. Although there exist different ways to plot a 2D graph, it is still hard to match the 3D solution when the structure of the graph is too complicated to present in 2D space. 3D visualization techniques handle this easily by two operations, zooming and rotation: zooming in to see the details, rotating the tree to locate the sub-tree of interest, and zooming out to capture the overall shape, as are shown in Fig. 5.

Highlighting. Sometimes some local information (for instance, specific nodes, edges, or proof patterns) is more interesting rather than the overall structure. Highlighting becomes a useful operation to show the local focused parts of the given proof tree. VMDV enables highlighting parts of the proof tree either by manual selection using mouse clicking, or by automatic selection via formulae searching. (Fig. 6)333In VMDV , we say that the proofs of two formulas have similar pattern if the first rules applied in the two bottom-up proofs are the same. For instance, if the proofs of two formulas in SCTL have similar pattern, then according to the rules in Fig. 2, both formulas must have the same modality or connector, or both are atomic formulas with the same predicate.

Focusing a specific subtree. In many cases, interesting information may be carried out by specific subtrees. To concentrate on these subtrees, the nodes that are not related are hidden. Additional operations can then be applied only on these subtrees. The focusing of a subtree is easily done by changing the root node. A reset operation will recover the entire tree (Fig. 5).

Extended Operations. In addition to the commonly used operations, some other operations that are specific to proof systems are also needed, so that VMDV can be adapted to different proof systems. The controlling of the construction of both the proof tree and the Kripke model in the SCTL system is a good example. Define a new operation includes the handling of messages from VMDV and the responds from the proof system. New operations are implemented as plug-ins that are dynamically loaded by VMDV . One selection from a pop up menu triggers one such operation when right click the mouse (Fig. 7).

3.3 Automatic Layout

The layout of 3D graphs is non-trivial. Our solution is modified from ForceAtlas2 [16]. ForceAtlas2 is a force-directed algorithm that simulates a physical system, where nodes repulse each other like magnets while edges attract the nodes they connect like springs. The forces of repulsion and attraction make the movement of nodes until the 3D graph reaches a balanced state. Since the clustering of nodes are not the main concern of VMDV, we set the degree of each node to be constant $1$ in our algorithm, not the number of edges that are attached to the node as ForceAtlas2 does. Same as ForceAtlas2, our algorithm is continuous and homogeneous, as opposed to the OpenOrd [15] algorithm which is not, and the algorithm of Yifan Hu [12] which is semi-continuous. The continuity and homogeneity of the algorithm make the movement of nodes to respect the feeling of a physical system, and users comprehend the 3D graph by “playing” with it.

4 Applications

In this section, we first show the applications of VMDV in the implementation of SCTL (in programming language OCaml), and then illustrate how VMDV visualize proof trees produced by existing proof system Coq [3].

4.1 The System SCTL

With the application of VMDV, we can show both proof trees and Kripke models in 3D format. We can also visualize, in 3D format, the verification procedure, revealing gradually the relation between a proof tree and the corresponding states of the Kripke model under consideration. Although the Kripke model in realistic cases may be very large, thanks to the on-the-fly style of proof search in SCTL, we can only show the states that need to be explored, which may be a small part of the whole model. The application of VMDV to the proof system SCTL is illustrated in the following small example.

Example 1 (The River Crossing Puzzle.)

A farmer is trying to transport a wolf, a sheep, and a cabbage from one side of a river to another, however, he can only carry at most one item each time. During the transportation, the sheep cannot be left alone with the wolf, nor the cabbage can be left alone with the sheep. The question is how can the farmer get across the river by bringing the wolf, the goat, and the cabbage.

We formalize this problem by defining a Kripke model, where each state is represented by an assignment of four boolean state variables farmer, wolf, goat and cabbage, and each transition between states is represented by the transformation of an assignment of these variables to another. The property to be verified is that whether there is a path that starts with the state

$\mathsf{S_{0}}$: {farmer:false, wolf:false, goat:false, cabbage:false}

and end with the state

$\mathsf{S}$: {farmer:true, wolf:true, goat:true, cabbage:true}.

This equals to verify if the sequent $\vdash EU_{x,y}(safe(x),complete(y),S_{0})$ is provable in SCTL, taking the Kripke model above as parameter, where $safe(x)$ denotes the atomic formula which specifies that, in state $x$, the sheep is not alone with the wolf, and the cabbage is not alone with the sheep; and $complete(y)$ the atomic formula which specifies that, in state $y$, the farmer has carried all the three items across the river. Using VMDV, we can show in 3D format the proof tree and the Kripke model, provided both by the proof system SCTL (Fig. 9). In addition, along with the proof search of the sequent in progress, in the Kripke model, a path of states emerges from scratch, certifying this proof. This is because the formula

[TABLE]

starts with $EU$ modality (called $EU$-formula), and each application of the rule $\mathbf{EU}$-$\mathsf{R_{2}}$ of SCTL (Fig. 2) corresponds to one unfolding step in the Kripke model. This process stops until the $\mathbf{EU}$-$\mathsf{R_{1}}$ applied. During this procedure, VMDV sends messages to the proof system SCTL, and automatically shows the newly constructed nodes both in the proof tree and in the Kripke model (Fig. 9). This way, when we highlight all the nodes with $EU$-formulas in the proof search tree, a state path in the Kripke model is also highlighted, certifying this proof (Fig. 9).

In SCTL, the proof tree for formulas starting with different modalities are clearly distinguishable from each other, the same scenario holds for the related part in the Kripke model under consideration. For instance, the main part of a proof tree of an $EU$-formula corresponds to a finite path in the model, testifying this proof. While for verifying an $AG$-formula, both the proof tree and the related part in the Kripke model may appear very complicated (Fig. 10). In this situation, one may focus on a part of the proof tree each time, and track the corresponding part of state transitions (Fig. 11).

4.2 A Small Example of Coq

We illustrate, by a small example, how VMDV can visualize proof trees produced by Coq. In Coq, the steps of interactive proof of a formula is controlled by a proof script. Each step of the proof script introduces new proof goals based on the current proof goal. Thus, we formulate the proof tree in such a manner that each proof goal is formulated as a node, and all sub-goals of the current goal are formulated as the sub-nodes of the current node. If the current goal has no sub-goal, then the current node is a leaf node. For instance, the proof script of the formula

$\forall A\;B\;C\;:Prop,\;(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))$

is

Proof. intros A B C. intros H1 H2 H3. apply H1. assumption. apply H2. assumption. Qed.

There are 7 steps (the first “assumption” comprise two steps: finish the current goal, and jump to the next goal) in this proof script. Thus, the proof tree should have 7 edges, as shown in Fig. 12.

In order to visualize proof trees produced by Coq in VMDV , one usually has two options. The first option is to build an integrated development environment (IDE) for the coq toplevel system (coqtop444https://www.mankier.com/1/coqtop) from scratch, and let the IDE communicate with VMDV . In this situation, the developer may have to handle many basic and cumbersome I/O problems of the IDE and coqtop. The second option is to build a wrapper upon existing interfaces for coqtop, such as coqide555https://www.mankier.com/1/coqide, or Proof General666https://proofgeneral.github.io/. These existing interfaces are usually much more flexible and easy to extend. The developer has to adapt the XML protocol specified by coqide or Proof General and translate the message into the TCP packets that are understandable by VMDV , which is very straightforward. We prefer the second option, and our interface is now under development. We believe that designing such a interface would guide the interactive proof in Coq in a much more friendly way with visualization, and may be helpful in the education classes.

5 Conclusion and Future Works

In this paper, we have proposed a visualization tool VMDV for visualising the output of various proof systems in 3D space. VMDV enables us a variety of manners to observe or interact with the 3D graph. In addition, we use an automatic layout algorithm to manage the shape of the 3D graph. Up to now, we have made our first step to the application of visualization analysis of proof trees produced by two automatic proof systems. For the future work, we intend to integrate our tool with more sophisticated theorem provers. For instance, in Coq [3], the construction of proof trees are controlled by proof scripts, but users can only focus on the current branch of a proof tree, and they have to memorize (or imagine) the overall structure of the current proof tree. In this situation, VMDV can show the overall structure of proof trees along with the dynamically updating of local branches. In this way, users can easily find whether the current formula has been already proved in another branch of the proof tree. If so, there is no need to do extra proof on this formula, and directly abort the proof of the current formula. Designing such a interface for Coq (or other existing proof systems) requires a middleware (broker) that can dispatch control and data messages interchanged by prove engines and VMDV . This is also the future work.