OUTPUT

The blog of Maxime Kjaer

CS-550 Formal Verification

Throughout these notes, vectors are denoted in bold and lowercase (e.g. ).

Transition systems

Definition

We’ll start by introducing transition systems, a generalization of DFAs. They may be not finite, and not deterministic.

Definition: Transition system

A transition system is a 4-tuple where:

  • is the set of states
  • is the set of starting states
  • is the transition relation
  • is the alphabet

For and , means that ther is a transition from to on input .

A few special cases of this general form exist:

  • If is finite, we have a finite state machine
  • If and , then the system is deterministic.

Traces and reachability

Definition: Trace

A trace is a finite or infinite sequence, describing steps taken by a transition system:

where we require, :

A trace may or may not be finite. If they are finite, we can assume that the trace ends with a state . We’ll introduce some notation for traces:

Definition: Trace of a transition system

is the set of all traces of a transition system , starting from .

Definition: Reachable states of a transition system

The reachable states are states for which there exists a trace that ends in :

To check for reachability, for a finite , we can simply run DFS.

Relations

Let’s study relations more closely. A relation is a directed edge in the transition graph. We follow this edge when we see a given input .

If we look at the graph, we may not be interested in the inputs associated to each edge. Therefore, we can construct the edge set :

Generally, we’ll use a bar for relations that disregard input. Note that even when is deterministic, can become non-deterministic.

Relations can be composed:

Definition: Composition of relations

Note that composition is not commutative, but is associative.

To understand what a composition means, intuitively, we’ll introduce a visual metaphor. Imagine the nodes of the graph as airports, and the edges as possible routes. Let be the routes operated by United Airlines, and be the routes operated by Delta. Then is the set of routes possible by taking a United flight followed by a Delta flight.

Definition: Iteration

An iteration describes paths of length in a relation . It is defined recursively by:

Here, describes the identity relation, i.e. a relation mapping every node to itself.

Definition: Transitive closure

The transitive closure of a relation is:

In our airport analogy, the transitive closure is the set of all airports reachable from our starting airports.

Finally, we’ll introduce one more definition:

Definition: Image of a set

The image of a state set under a relation is the set of states reachable in one step from :

We also introduce an alternative notation:

The alternative notation may make it simpler to read images; can be read as “ following then following ”.

The above definitions lead us to a first definition of reach:

Theorem: Definition 1 of reach

Post

We’ll introduce another definition in order to give an alternative definition of reach. We’re still considering a state system .

Definition: Post

If , define:

We also define:

This definition of post leads us to another formulation of reach:

Theorem: Definition 2 of reach

The proof is done by expanding the post:

Where:

Invariants

Definition: Invariant

An invariant of a system is any superset of the reachable states:

A way to think of invariants is that all the reachable states must “satisfy the invariant”, i.e. be included in .

Definition: Inductive Invariant

An inductive invariant is a set satisfying:

Intuitively, the second condition means that you can’t “escape” an inductive invariant by taking a step: there can be ingoing edges to an inductive invariant, but no edges exiting the set.

Note that every inductive invariant is also an invariant. Indeed, for an inductive invariant , if then we must also grow to include all states reachable from in order to satisfy the second property. Therefore, and is an invariant.

Definition: Inductive strengthening

For an invariant , is an inductive strengthening of if:

  • is an inductive invariant

In this case, we have:

Encoding and storage

Motivating example

Transition systems very quickly get out of hand. Suppose a snack dispenser has different items, and has 10 of each. It can take 500 coins. It then has:

They might not all be reachable, but reachability is a separate question. Here, we’re just defining the graph. In any case, this is too large to store explicitly. Therefore, we must find formulas and data structures to represent it more compactly.

Sequential circuit

We’ll consider a deterministic finite-state transition system . We will let be such that , and , or in other words, and .

To encode the transition system in bits, we can think of it as 4-tuple of boolean functions:

  • We can represent the states on bits:
  • We can represent the alphabet on bits:
  • We can represent the set of initial states by the boolean function , which maps each state to a boolean (“initial” or “not initial”).
  • We can represent the transition relation as a function , which is

We can think of these functions as a circuit receiving an input , which alters the state , which in turn alters the relation .

Example of a simple sequential circuit

Formula encoding of boolean functions

Both the initial states and the transition relation are boolean functions. We will often define them mathematically (e.g. or ), but how do we encode them in bits?

We can use a truth table. For instance, the truth table encoding of is a table mapping inputs and to outputs . This is the most efficient encoding if we need to be able to encode any relation: there is no better general encoding. However, most functions can be stored more efficiently.

Let us consider the relation function . We can consider an input-output pair as the following condition:

We can write this as a propositional formula with variables . This formula should be true exactly when the tuple belongs to .

Let , and let be a propositional variable. We can then define:

With this notation in hand, we can state the following:

Theorem: Formula encoding of boolean functions

We can always represent a transition relation as a propositional formula in disjunctive normal form, where:

For many boolean functions (, , etc) this formulation will be quite small.

Auxiliary variables

This formula is a tree, where variables are leaves, and operations are internal nodes (much like an AST). Clearly, the variables are shared by many operations, so the more efficient representations exploit this sharing, and represent the tree as a directed acyclic graph (DAG) instead.

Note that not only leaves of the tree are shared, but that bigger nodes can also be shared. This leads us to introduce the notion of auxiliary variable definitions. An auxiliary variable represents one such shared node.

We can define auxiliary variables directly in the propositional logic by using the operator (which is alternative notation for ).

For instance, for a -bit ripple-carry adder can be encoded with:

  • Initial state
  • Input numbers
  • Output

The formula for the adder with auxiliary variables (serving as the carry) is:

The initial carry is . Every individual adder gets 3 bits of input to add: two bits, and the previous carry. It outputs a carry of 1 iff two or more input bits are 1. It outputs a single bit as the result of the addition, which is the XOR of all inputs.

Propositional logic

Definition

Propositional logic is a language for representing Boolean functions as formulas. The grammar of this language is:

Where denotes variable identifiers.

QBF

Having looked at boolean formulas let’s now look at a small generalization, QBFs:

Definition: Quantified Boolean Formulas

Quantified Boolean Formulas (QBFs) is built from:

  • Propositional variables
  • Constants and
  • Operators

We will use as alternative notation for . A boolean formula is QBF without quantifiers ( and ).

Free variables

Definition: Free variables

The free variables of a formula is the set of variables that are not bound by a quantifier:

Environment

Definition: Environment

An environment is a partial map from propositional variables to (“false” or “true”).

Consider two vectors and of propositional variables. We denote the environment as a mapping given by ,

We denote the result of evaluating a boolean expression with the environment as . This can evaluate to (“false”) or (“true”).

While the formula might seem weird at first (we defined in terms of another , it makes more sense if we think about the first as an AST node and the second as a logical and in the host language:

1
2
3
4
5
6
7
def eval(expr: Expr)(implicit env: Var => Boolean): Boolean = expr match {
    case x: Var => env(x)
    case Literal(0) => false
    case Literal(1) => true
    case And(a, b) => eval(a) && eval(b)
    case Or(a, b) => eval(a) || eval(b)
}

With this notation in hand, we can introduce the following shorthand:

Definition: Models

We write to denote that is true in environment , i.e. that .

Substitution

Definition: Substitution

Let and be propositional formulas, and let be a variable. Let denote the result of replacing each occurrence of in by :

We’ll also introduce a general notation to simultaneously replace many variables: denotes the substitution of a vector of variables with a vector of expressions .

Validity, Satisfiability and Equivalence

Definition: Satisfiability

A formula is satisfiable

Note that if is not satisfiable, it is unsatisfiable, which means .

Definition: Validity

A formula is valid

Theorem: Validity and unsatisfiability

is valid is unsatisfiable.

The proof should follow quite trivially from the definitions.

Definition: Equivalence

Formulas and are equivalent environment defined for all free variables in , we have:

This means that two formulas are equivalent if and only if they always return the same values for the same environment (assuming it’s defined for all their free variables).

Theorem: Equivalence and validity

and are equivalent the formula is valid.

Bounded model checking

Formula representation of sequential circuits

Definition: Sequential circuit

We represent a sequential circuit as a 5-tuple where:

  • is the vector of state variables
  • is a boolean formula describing the initial state
  • is a boolean formula called the transition formula
  • is the vector of auxiliary variables
  • is the vector of input variables

The boolean formula tells us which states we can start in, so it can only contain state variables:

The transition formula can only contain state (), next-state (), auxiliary () or input () variables:

The sequential circuit is a representation of a transition system , where:

  • , meaning that the initial states of a transition system is given by an assignment of state variables that verifies the formula
  • , meaning that the transition relation is given by a mapping of states and inputs to next-states , such that the mapping satisfies the transition formula. Here, the auxiliary variables are existentially quantified so that we can express the criterion without them.

Inductive invariant checking

Given a sequential circuit representation of a transition system , and a formula , how can we check that is an inductive invariant? According to the definition, we require:

We’ll ask the SAT solver to check if it’s possible to break either of the two conditions by asking it if it can satisfy either of the following two formulas:

  • to check if there is an initial state not included in the invariant.
  • to check if, starting from the invariant and take a step, we can end up outside of the invariant.

    To understand this condition, it’s useful to think of as determining the assignment of . Then, seeing that contains variables and , it will fix the assignment for the next states . We can then see if the invariant is still true at the next state.

If the SAT solver returns UNSAT to both, we have proven that is an inductive invariant. Note that this resembles a proof by induction (because it is!).

Bounded model checking for reachability

How do we check whether a given state is reachable? Often, we’re interested in knowing if we can reach an error state or not; being able to do so would be bad. To simplify the question a little, we can ask whether we can reach this error state in steps.

Let be the error formula corresponding to the error state, so . When we talked about circuits, we said that the state and inputs change at each step, so let us denote the state at step as , and the inputs at step as .

We’ll construct an error formula that is satisfiable if and only if there exists a trace of length starting from the initial state that satisfies :

This formula starts at the initial state, then computes all states , and plugs in the final state in the error formula to see if it can be satisfied.

If the SAT solver returns UNSAT, the error state is not reachable. If it returns SAT, the

Satisfiability checking

SAT problem

The SAT problem is to determine whether a given formula is satisfiable. The problem is NP-complete, but useful heuristics exist.

A SAT solver is a program that given a boolean formula either:

  • Returns SAT and optionally an environment such that
  • Returns UNSAT and optionally a proof that no satisfying assignment exists

Formal proof system

Let’s consider a set of logical formulas (e.g. propositional logic).

Definition: Proof system

A proof system is a pair where is a decidable set of inference steps, where:

  • A set is decidable there is a program to check if an element belongs to it
  • Given a set , denotes all finite sequences with elements from
Definition: Inference step

An inference step is a 2-tuple , which we can denote as:

We say that from the premises , we derive the conclusion .

Definition: Axiom

We say that an inference step is called an axiom when , i.e. that it has no premises:

Definition: Proof

Given a proof system , a proof is a finite sequence of inference steps such that, for every inference step , each premise is a conclusion of a previous step.

A minimal propositional logic proof system

We’ll look into a simple logic called the Hilbert system. We’ll define the grammar of our logic as follows. This grammar defines a set of formulas .

This may seem very minimal, but we can actually express many things by combining these. For instance, we can introduce negation (“for free”) as a shorthand:

The inference rules are , where:

The first two rules are axioms, telling us that an implication is true if the right-hand side is true (), and that implication is distributive (). We might recognize modus ponens in the last rule.

We can use these rules to construct a proof of . We’ll draw this proof as a DAG: we can always view a proof as a DAG because of the requirement that the premises of an inference step be a conclusion of a previous step.

G A (a→((a→a)→a) → ((a → (a→a))→(a→a) C (a→(a→a))→(a→a) Modus Ponens A->C B (a((a→a)→a) B->C E a→a Modus Ponens C->E D (a→(a→a)) D->E

Provability

A formula is provable if we can derive it from a set of initial assumptions. We’ll start by formally defining what an assumption even is:

Definition: Assumptions

Given where , and given a set of assumptions , a derivation from in is a proof in where:

In other words, assumptions from are just treated as axioms (i.e. they are rules that have no prerequisites, hence ). A derivation is a proof that starts from assumptions.

Definition: Provable

We say that “a formula is provable from a set of assumptions ”, denoted , there exists a derivation from in that contains an inference step whose conclusion is .

We write (or simply ) to denote that there exists a proof in containing as a conclusion.

Consequence and soundness in propositional logic

Definition: Semantic consequence

Given a set of assumptions , where is in propositional logic, and given , we say that is a semantic consequence of , denoted , for every environment that defines all variables in , we have:

In other words, iff an environment makes all assumptions true, and is true in an environment when the set of assumptions are all true in that environment, then we call a semantic consequence.

Definition: Soundness

A step is sound

A proof system is sound if every inference step is sound.

In other words, a conclusion of step is sound if it is a semantic consequence of the previous steps. A proof is sound if all steps are sound.

If is an axiom (which has no precondition, meaning that in the above), this definition of soundness means that is always a valid formula. We call this a tautology.

Theorem: Semantic consequence and provability in sound proof systems

Let where are propositional logic formulas. If every inference rule in is sound, then implies .

This theorem tells us that that if all the inference rules are sound, then is a semantic consequence of if is provable from . This may sound somewhat straightforward (if everything is sound, then it seems natural that the semantic consequence follows from provability), but is a nice way to restate the previous definitions.

The proof is immediate by induction on the length of the formal proof. As a consequence implies that is a tautology.

Proving unsatisfiability

Let’s take a look at two propositional formulas and . These are semantically equivalent if and .

We can prove equivalence by repeatedly applying the following “case analysis” rule, which replaces a given variable by 0 in and by 1 in :

Definition: Case analysis rule

This is sound, because if we consider an environment defining , and assume and , then:

  • if then
  • if then

In either case remains true when and are sound.

Strictly speaking, the above rule may not be quite enough, so we’ll also introduce a few simplification rules that preserve the equivalence:

Those rules together form the sound system , where:

Remember that a set of formulas is satisfiable if there exists an environment such that for every formula , . We can use to conclude unsatisfiability:

Theorem: Refutation soundness

If then is unsatisfiable

Here, means false. This follows from the soundness of . More interestingly, the converse is also true.

Theorem: Refutation completeness

If a finite set is unsatisfiable, then

This means that unsatisfiable .

For the proof, we can take the conjunction of formulas in and existentially quantify it to get (i.e. )

Conjunctive Normal Form (CNF)

To define conjunctive normal form, we need to define the three levels of the formula:

  • CNF is the conjunction of clauses
  • A clause is a disjunction of literals
  • A literal is either a variable or its negation

This is a nice form to work with, because we have the following property: if is a clause then there exists a literal such that .

We can represent formulas in CNF as a set of sets. For instance:

The false value can be represented as the empty clause . Note that seeing an empty clause in CNF means that the whole formula is unsatisfiable.

Clausal resolution

Definition: Clausal resolution rule

Let and be two clauses.

This rule resolves two clauses with respect to . It says that if clause contains , and clause contains , then we can remove the variable from the clauses and merge them.

Theorem: Soundness of the clausal resolution rule

Clausal resolution is sound for all clauses and propositional variables .

This tells us that clausal resolution is a valid rule. A stronger result is that we can use clausal resolution to determine satisfiability for any CNF formula:

Theorem: Refutational completeness of the clausal resolution rule

A finite set of clauses is satisfiable there exists a derivation to the empty clause from using clausal resolution.

Unit resolution

A unit clause is a clause that has precisely one literal: it’s of the form where is a literal. Note that the literal in a unit clause must be true.

Given a literal we define the dual as and .

Unit resolution is a special case of resolution where at least one of the clauses is a unit clause.

Definition: Unit resolution

Let be a clause, and let be a literal.

This is sound (if is true then is false and can thus be removed from another clause ). When applying this rule we get a clause : this gives us progress towards , which is good.

Equivalence and equisatisfiability

Let’s recall that two formulas and are satisfiable iff and .

Definition: Equisatisfiability

Two formulas and are equisatisfiable is satisfiable whenever is satisfiable.

Equivalent formulas are always equisatisfiable, but equisatisfiable formulas are not necessarily equivalent.

Tseytin’s Transformation

Tseytin’s transformation is based on the following insight: if and are two formulas, and we let be a fresh variable, then is equisatisfiable with:

Tseytin’s transformation applies this recursively in order to transform an expression to CNF. To show this, let’s consider a formula using :

The transformation works by introducing a fresh variable for each operation (we can think of it as being for each AST node):

Note that these formulas refer to subterms by their newly introduced equivalent variable. This prevents us from having an explosion of terms in this transformation.

Each of these equivalences can be converted to CNF by using De Morgan’s law, and switching between and . The resulting conversions are:

Operation CNF

Note that the Tseytin transformations can be read as implications. For instance, the transformation can be read as:

  • If and are true, then is true
  • If is false, then is false
  • If is false, then is false

It then takes the conjunction of all these equivalences:

SAT Algorithms for CNF

Now that we know how to transform to CNF, let’s look into algorithms that solve SAT for CNF formulas.

DPLL

The basic algorithm that we’ll use is DPLL, which applies clausal resolution recursively until an empty clause appears, or all clauses are unit clauses. This works thanks to the theorem on refutational completeness of the clausal resolution rule.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
def DPLL(S: Set[Clause]): Bool = {
    val S' = subsumption(UnitProp(S))
    if (∅  S') false // an empty clause means the whole thing is unsat
    else if (S' has only unit clauses) true // the unit clauses give e
    else {
        val L = a literal from a clause of S' where {L} not in S'
        DPLL(S' + Set(L)) || DPLL(S' + Set(complement(L)))
    }
}

// Unit Propagation
def UnitProp(S: Set[Clause]): Set[Clause] =
    if (C  S && unit U  S && resolve(U, C) not in S)
        UnitProp((S - C) + resolve(U, C))
    else S

def subsumption(S: Set[Clause]): Set[Clause] =
    if (C1, C2  S such that C1  C2)
        subsumption(S - C2)
    else S

Backtracking

Perhaps the most intuitive algorithm is to construct a binary decision tree. At each node, we take a random decision. If that leads to a conflict, we go back one step, and take the opposite decision.

This is quite simple, but the complexity is exponential. We’ll therefore see some smarter algorithms.

Non-chronological backtracking

We still construct a binary decision tree. Each decision may also force some other variables into a certain value: we will track these implications in a directed graph.

In this graph, each node represents a value assignment to a variable; let’s say we color a node blue if it has been set directly by a decision, and in green if the value is a consequence of a decision. Edges go from nodes (which may be blue or green) to their consequences.

As we construct the graph, we may create conflicts, meaning that we have two (green) nodes assigning different values to the same variable. In this case, we look at the set of nodes pointing to the conflicting pair of nodes:

G cluster_conflict x1 x1 = 0 x4 x4 = 1 x1->x4 x8 x8 = 0 x1->x8 x12 x12 = 1 x1->x12 x2 x2 = 0 x11 x11 = 1 x2->x11 x3 x3 = 1 x3->x8 x9b x9 = 1 x3->x9b x7 x7 = 1 x9a x9 = 0 x7->x9a x7->x9b x8->x12 x8->x9a

In the above example, the variables , and point to the conflicting pair of ’s. This means that one of the assignments to these variables was incorrect, because it lead us to the conflict. We can learn from this conflict, and add the following conflict clause to the formula:

We can then backtrack to the first decision where we set , or (which may be much earlier than the parent decision in the tree). Every once in a while, it may be useful to completely abandon the search tree (but keep the conflict clauses): this is called a restart.

This approach significantly prunes the search tree; by introducing this conflict clause, we’ve learned something that will be useful forever.

2-literal watching

This algorithm does the standard trick of unit propagation, but avoids expensive book-keeping by only picking 2 literals in each clause to “watch”. We ignore assignments to other variables in the clause.

For each variable, we keep two sets of pointers:

  • Pointers to clauses in which the variable is watched in its negated form
  • Pointers to clauses in which the variable is watched in its non-negated form

Then, when a variable is assigned true, we only need to visit clauses where its watched literal is negated. This means we don’t have to backtrack!

Interpolation

Definition: Interpolant

Let and be propositional formulas. An interpolant for and is a formula such that:

Note that if these conditions hold, we have . The goal of is to serve as an explanation of why implies .

Theorem: Existence and Lattice of Interpolants

Let and be propositional formulas such that and let be the set of interpolants of . Then:

  • If then and

Linear Temporal Logic

Definition

With bounded model checking, we’ve seen how to check for a property over a finite trace. However, there are certain properties that we cannot prove by just seeing a finite trace. For instance, program termination or eventual delivery cannot be proven with the semantics of propositional logic. This will prompt us to introduce linear temporal logic, with which we can study events on a trace.

Let be a boolean formula over state and input variables.

We write to say that a trace satisfies formula at time . The rules for the above constructs are:

We can interpret until to mean that is true until becomes true. For instance, we can guarantee something until an overflow bit is on, at which point all bets are off. Note that this does not impose any constraints on once is true.

Note that next and prev, and since and until are duals of each other2.

We can add some derived operations from these:

The operation globally can be thought of as meaning “forever, from now on” (where “now” is step ). For instance, means that from now on, every point in the trace satisfying is followed by a point in the trace satisfying at some point.

Binary Decision Diagrams

Definition

Binary Decision Diagrams (BDDs) are a representation of Boolean functions: we can represent a Boolean function as a directed acyclic graph (DAG). We distinguish terminal from non-terminal nodes. Each edge is labeled with a decision: a solid edge (“high edge”) means the variable is 1, and a dashed edge (“low edge”) means that it is 0. The leaf nodes are labeled with the outcome.

For instance, the BDD for is:

G cluster_output f1a 1 f1b 1 f0 0 x x x->f1a y y x->y y->f1b y->f0

We can also think of this DAG as a finite automaton, or as a (loop-free)branching program.

Canonicity

The key idea of BDDs is that specific forms of BDDs are canonical, and that BDDs can be transformed into their canonical form. For instance, the previous example can be rewritten as:

G f1 1 f0 0 x x x->f1 y y x->y y->f1 y->f0

Let’s define this transformation more formally.

We first assign an arbitrary total ordering to variables: variables must appear in that order along all paths. Here, we picked as our ordering. Note that in general, selecting a good ordering is an intractable problem, but decent application-specific heuristics exist.

Then, the reduced ordered BDD (RO-BDD) is obtained by:

  • Merging equivalent leaf nodes (which is what we did above)
  • Merging isomorphic nodes (same variables and same children)
  • Eliminating redundant tests (where both outgoing edges go to the same child)

Doing this brings us to the following property:

Theorem: Unicity of RO-BDD

With a fixed variable order, the RO-BDD for a Boolean function is unique

In the following, we’ll always refer to RO-BDDs, and just call them BDDs.

Data structures for BDDs

To encode a BDD, we’ll map number all nodes as 0, 1, 2, …, where 0 and 1 are terminals. The variables are also numbered as . We also number the levels in the diagram, according to the total ordering that we selected: level 1 is the root node, and level contains terminal nodes.

G cluster_level1 Level 1 cluster_level2 Level 2 cluster_level3 Level 3 x x y y x->y f1 1 x->f1 y->f1 f0 0 y->f0

A data structure for BDDs is the node table , mapping a node to its low child and high child . The node table also contains an entry describing the level in the ordering as well as the name of the variable.

For instance, for the example we used above, the table would be:

Node number Level and name Low edge High edge
0 3    
1 3    
2 2 0 1
3 1 2 1

We’ll assume we have some methods for querying this table:

  • init(T): initialize with 0 and 1 terminal nodes
  • u = add(T, i, l, h): add node with to
  • var(u): get of node
  • low(u): get of node
  • high(u): get of node

We can also define the inverse of a node table, allowing us to find a node if we have all the information about it. We’ll assume that we have some methods to query and update this structure:

  • init(H): initialize with 0 and 1 terminal nodes
  • u = lookup(H, i, l, h): get node from
  • insert(H, i, l, h, u): add an entry from to

Basic operations on BDDs

Somewhat surprisingly, given a BDD for a formula , we can check whether it is a tautology, satisfiable or inconsistent in constant time:

  • is a tautology the BDD is
  • is satisfiable the BDD is not
  • their BDDs are equal3

To insert a node into , we ensure that we’re keeping a RO-BDD by eliminating redundant tests, and preventing isomorphic nodes. If that is not the case, we can update the tabée and the reverse mapping .

1
2
3
4
5
6
7
8
9
10
11
12
13
14
type NodeId = Int
type Level = Int

def mk(i: Level, l: NodeId, h: NodeId): NodeId = {
  // eliminate redundant tests:
  if (l == h) l
  // prevent isomorphic nodes:
  else if (lookup(H, i, l, h) != null) lookup(H, i, l, h) 
  else {
    u = add(T, i, l, h) // insert node
    insert(H, i, l, h, u) // update reverse mapping
    u
  }
}

With this method in hand, we can see how to build a BDD from a formula . The key idea is to use Shannon’s expansion:

Here, means that we replace all nodes by their high-edge subtree. In the formula, we can think of it as a substitution of by 1. We call this basic operation Restrict.

This breaks the problem into two subproblems, which we can solve recursively:

1
2
3
4
5
6
7
8
9
10
def build(f: Formula): NodeId = build2(f, 1)
private def build2(f: Formula, level: Level): NodeId =
  if (level > n)
    if (f == False) 0 else 1
  else {
    xi = f.variables.head
    f0 = build2(f.subst(xi, 0), level + 1)
    f1 = build2(f.subst(xi, 1), level + 1)
    mk(level, f0, f1)
  }
  1. The proof of this identity is in exercise session 1, exercise 2.1.1. It is done by decomposing into existential quantifiers. 

  2. Or rather, they’re almost duals, because the future is infinite but the past is finite. 

  3. This is a consequence of the the theorem of unicity of the RO-BDD 

« Back