Liveness Analysis for Parameterised Boolean Equation Systems

Today I have talked about our paper Liveness Analysis for Parameterised Boolean Equation Systems at ATVA’14 (which is currently being held in Sydney). Let’s take a look at what this work is about.

To start with, a parameterised Boolean equation system (PBES) is a system of fixed point equations that can, e.g., be used in model checking modal mu-calculus properties, check behavioural equivalence between systems, or solve Datalog queries.

Let’s take a look at what such a system looks like: \(\begin{array}{ll} \nu X(i,j,k,l\colon N) & = (i = 1 \land j = 1 \land k = 1 \Rightarrow X(2,j,k,l+1)) \\ & \land (j = 1 \Rightarrow Y(i,1,1,k)) \\ & \land \forall m \colon N . (j = 2 \Rightarrow Y(i,j,m+k,k)); \\ \nu Y(i,j,k,l \colon N) & = (j \neq 2 \Rightarrow k < 10) \\ & \land (j = 2 \Rightarrow X(1,1,l+1,1)) \land X(2,2,1,l);\\ \mathbf{init}~X(1,1,1,1); \end{array}\)

So, in short, we have a system of mutually recursive fixed point equations, where the variables are parameterised with variables ranging over abstract data types; the right hand sides range over formulas over these data types and first order variables. In general we are interested in the solution to a specific instance of a variable, like $X(1,1,1,1)$ in the example above.

Typically, we solve PBESs using instantiation into Boolean equation systems (BESs) or parity games (both are equivalent). The main motivation for instantiating is that it is easy to automate. However, this can easily lead to an infinite BES. For instance, in the example above, $X(2,2,1,1)$ depends on $Y(2,2,v+1,1)$ for infinitely many values of $v$.

In our paper, we present a static analysis technique for PBESs that can be used to overcome such problems. In the example, we can observe that parameter $k$ to the equation for $Y$ is only relevant when $j \neq 2$, but in the infinity in the example, we only reach $Y$ with $j = 2$, hence if we look closely, we can see that it is sound to replace $Y(i,j,m+k,k)$ by $Y(i,j,1,k)$! This is exactly what the approach in the paper establishes in three steps:

1. We analyse the structure of the PBES to determine a set of control flow parameters. Using these control flow parameters we build a control flow graph.
2. In the next step, we label the nodes in the control flow graph with those data parameters that are possibly relevant at that control flow location, and use backwards reachability to propagate relevance. All parameters that occur not in the labelling of a particular control flow location are not relevant (dead) at that location.
3. Once we have established this labelling, we can use the information to reset dead variables in every recursion in the PBES.

The first analysis that we present treats all control flow parameters simultaneously. However, this approach suffers from an exponential blow-up. We therefore also present an approximate analysis that considers separate control flow graphs that does not suffer from this blow-up, yet closely approximates the global analysis.

The analysis has been implemented in the mCRL2 toolset, in the tool pbesstategraph. Our running example is reduced to: \(\begin{array}{ll} \nu X(i,j,k,l\colon N) & = (i = 1 \land j = 1 \land k = 1 \Rightarrow X(2,1,1,1)) \\ & \land (j = 1 \Rightarrow Y(i,1,1,1)) \\ & \land (j = 2 \Rightarrow Y(i,2,1,k)); \\ \nu Y(i,j,k,l \colon N) & = (j \neq 2 \Rightarrow k < 10) \\ & \land (j = 2 \Rightarrow X(1,1,l+1,1)) \land X(2,2,1,1);\\ \textbf{init}~X(1,1,1,1); \end{array}\)

This PBES has a finite instantiation, hence we can get an arbitrarily large reduction using this approach. Also in practice we have seen large reductions in size, and dramatic speedups for model checking, while the added overhead is limited.

Check out the slides and the paper (missing reference). If you are interested in the details of the proofs, they are available in the arXiv version (missing reference).

References