Counter Formulas
Next: Pattern Formulas Up: Input Formulas Previous: Random Formulas

Counter Formulas

Pre-translation rewriting is highly effective for random formulas, but ineffective for structured formulas [2,5]. To measure performance on scalable, non-random formulas we tested the tools on formulas that describe $n$-bit binary counters with increasing values of $n$. These formulas are irreducible by pre-translation rewriting, uniquely satisfiable, and represent a predictably-sized state space. Correctness is easily determined by checking for precisely the unique counterexample for each counter formula. We tested four constructions of binary counter formulas, varying two factors: number of variables and nesting of $\mathcal{X}$'s.

We can represent a binary counter using two variables: a counter variable and a marker variable to designate the beginning of each new counter value. Alternatively, we can use 3 variables, adding a variable to encode carry bits, which eliminates the need for $\mathcal{U}$-connectives in the formula. We can nest $\mathcal{X}$'s to provide more succinct formulas or express the formulas using a conjunction of unnested $\mathcal{X}$-sub-formulas.

Let $b$ be an atomic proposition. Then a computation $\pi$ over $b$ is a word in $(2^{\{0,1\}})^\omega$. By dividing $\pi$ into blocks of length $n$, we can view $\pi$ as a sequence of $n$-bit values, denoting the sequence of values assumed by an $n$-bit counter starting at $0$, and incrementing successively by $1$. To simplify the formulas, we represent each block $b_0,b_1,\ldots,b_{n-1}$ as having the most significant bit on the right and the least significant bit on the left. For example, for $n=2$ the $b$ blocks cycle through the values $00$, $10$, $01$, and $11$. For technical convenience, we use an atomic proposition $m$ to mark the blocks. That is, we intend $m$ to hold at point $i$ precisely when $i=0 \bmod n$.

For $\pi$ to represent an $n$-bit counter, the following properties need to hold:

1) The marker consists of a repeated pattern of a 1 followed by n-1 0's.
2) The first n bits are 0's.
3) If the least significant bit is 0, then it is 1 n steps later
   and the other bits do not change.
4) All of the bits before and including the first 0 in an n-bit block flip
   their values in the next block; the other bits do not change.

For $n=4$, these properties are captured by the conjunction of the following formulas:

1. (m) && ( [](m -> ((X(!m)) && (X(X(!m))) && (X(X(X(!m))))
                                           && X(X(X(X(m)))))))
2. (!b) && (X(!b)) && (X(X(!b))) && (X(X(X(!b))))
3. []( (m && !b) ->
       ( X(X(X(X(b)))) &&
         X ( ( (!m) &&
           (b -> X(X(X(X(b))))) &&
           (!b -> X(X(X(X(!b))))) ) U m ) ) )
4. [] ( (m && b) ->
        (X(X(X(X(!b)))) &&
          (X ( (b && !m && X(X(X(X(!b))))) U
               (m || (!m && !b && X(X(X(X(b)))) &&
                      X( ( !m && (b -> X(X(X(X(b))))) &&
                          (!b -> X(X(X(X(!b))))) ) U m ) ) ) ) ) ) )

Scalable counter formulas of this form are automatically generated by LTLcounter.pl. Usage: LTLcounter.pl number_of_bits

Note that this encoding creates formulas of length $O(n^2)$. A more compact encoding results in formulas of length $O(n)$. For example, we can replace formula (2) above with:

2. ((!b) && X((!b) && X((!b) && X(!b))))

Scalable counter formulas of this form, with nested $\mathcal{X}$-operators, are automatically generated by LTLcounterLinear.pl. Usage: LTLcounterLinear.pl number_of_bits

We can eliminate the use of $\mathcal{U}$-connectives in the formula by adding an atomic proposition $c$ representing the carry bit. The required properties of an $n$-bit counter with carry are as follows:

A 4-bit Binary Counter
m 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001
b 0000 0001 0010 0011 0100 0101 0110 0111 1000 1001
c 0000 0001 0000 0011 0000 0001 0000 0111 0000 0001
 
m 0001 0001 0001 0001 0001 0001 0001 ...    
b 1010 1011 1100 1101 1110 1111 0000 ...    
c 0000 0011 0000 0001 0000 1111 0000 ...    


To describe the behavior of the counter, we describe six properties and AND them together. For example, here is the program output for a 4-bit counter:

1) The marker consists of a repeated pattern of a 1 followed by n-1 0's.
2) The first n bits are 0's.
3) If m is 1 and b is 0 then c is 0 and n steps later b is 1.
4) If m is 1 and b is 1 then c is 1 and n steps later b is 0.
5) If there is no carry, then the next bit stays the same n steps later.
6) If there is a carry, flip the next bit n steps later and adjust the carry.

For $n=4$, these properties are captured by the conjunction of the following formulas.

1. (m) && ( [](m -> ((X(!m)) && (X(X(!m))) && (X(X(X(!m))))
                                           && (X(X(X(X(m))))))))
2. (!b) && (X(!b)) && (X(X(!b))) && (X(X(X(!b))))
3. [] ( (m && !b) -> (!c && X(X(X(X(b))))) )
4. [] ( (m && b) -> (c && X(X(X(X(!b))))) )
5. [] (!c & X(!m)) ->
      ( X(!c) && (X(b) -> X(X(X(X(b))))) &&
                 (X(!b) -> X(X(X(X(!b))))) )
6. [] (c -> ( ( X(!b) -> ( X(!c) && X(X(X(X(X( b))))) ) ) &&
              ( X( b) -> ( X( c) && X(X(X(X(X(!b))))) ) ) ))

Scalable counter formulas of this form, using a carry bit and no $\mathcal{U}$-operators, are automatically generated by LTLcounterCarry.pl. Usage: LTLcounterCarry.pl number_of_bits

Scalable counter formulas using a carry bit and nested $\mathcal{X}$-operators are automatically generated by LTLcounterCarryLinear.pl. Usage: LTLcounterCarryLinear.pl number_of_bits


Next: Pattern Formulas Up: Input Formulas Previous: Random Formulas
Kristin Yvonne Rozier 2007-05-10