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 -bit binary counters with increasing values of . 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 '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 -connectives in the formula. We can nest 's to provide more succinct formulas or express the formulas using a conjunction of unnested -sub-formulas.

Let be an atomic proposition. Then a computation over is a word in . By dividing into blocks of length , we can view as a sequence of -bit values, denoting the sequence of values assumed by an -bit counter starting at , and incrementing successively by . To simplify the formulas, we represent each block as having the most significant bit on the right and the least significant bit on the left. For example, for the blocks cycle through the values , , , and . For technical convenience, we use an atomic proposition to mark the blocks. That is, we intend to hold at point precisely when .

For to represent an -bit counter, the following properties need to hold:

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 , these properties are captured by the conjunction of the following formulas:

&& 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 . A more compact encoding results in formulas of length . For example, we can replace formula (2) above with:

Scalable counter formulas of this form, with nested -operators, are automatically generated by LTLcounterLinear.pl. Usage: `LTLcounterLinear.pl number_of_bits`

We can eliminate the use of -connectives in the formula by adding an atomic proposition representing the carry bit. The required properties of an -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:

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 , these properties are captured by the conjunction of the following formulas.

&& (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 -operators, are automatically generated by LTLcounterCarry.pl. Usage: `LTLcounterCarry.pl number_of_bits`

Scalable counter formulas using a carry bit and nested -operators are automatically generated by LTLcounterCarryLinear.pl. Usage: `LTLcounterCarryLinear.pl number_of_bits`