Transcript Fresco - ERNET

DECIDABILITY OF PRESBURGER
ARITHMETIC USING FINITE
AUTOMATA
Presented by :
Shubha Jain
Reference :
Paper by Alexandre Boudet
and Hubert Comon
TOPICS TO BE COVERED
Decidability
Presburger Arithmetic
Construction of Finite Automata
DECIDABILITY
 Some definitions :
 Formula : A formula is a well formed string over the alphabet :
{^ , ˇ , ¬ , ( , ) ,  ,  ,  ,  ,< , > ,x , y , z , …} that is, binary operators,
parenthesis, quantifiers, relational operators and variables. For ex,
x y (y=x+1).
 An atomic formula contains just addition and relational operators.
 Sentence : A sentence is a formula with no free variables (variable not
within the scope of any quantifier).The above example is a sentence. A
sentence can consist of some atomic formulae along with the Boolean
operators ^,ˇ and ¬ and the quantifiers  and  .
 Theory : It is a set of true sentences in a formal language.
 Decidability : The term “decidable” (in logic) refers to the existence of an
effective method using which we determine whether a sentence is true or
not.
PRESBURGER ARITHMETIC
 Presburger arithmetic is named in honor of Mojzesz Presburger,
who introduced it in 1929.
 It is the theory of the natural numbers with addition denoted as
(N,+,<).
 Presburger arithmetic is a decidable theory. This means it is
possible to effectively determine, for any sentence in the language of
Presburger arithmetic, whether that sentence is provable from the
axioms of Presburger arithmetic.
 Limitation : Presburger Arithmetic cannot formalize concepts such
as divisibility or prime number . Generally , any number concept
leading to multiplication cannot be defined in Presburger
Arithmetic .
PRESBURGER ARITHMETIC
The axioms of Presburger arithmetic are the universal closures of the following:
1) ¬(0 = x+ 1)
2) x + 1 = y+ 1 → x= y
3) x + 0 = x
4) (x + y) + 1 = x + (y + 1)
5) Let P(x) be a first-order formula in the language of Presburger arithmetic
with a free variable x (and possibly other free variables). Then the following
formula is an axiom:
(P(0) ∧ ∀x(P(x) → P(x + 1))) → P(y).
(5) is an axiom schema of induction.
Some examples :
 We can express the fact that every number is
either even or odd :
x y ((y+y=x)ˇ(y+y+1=x))
 We can express that there are infinitely many
natural numbers :
x y (x+1=y)
 (x+x+1+1+1 = y+1+1) is a formula which can
be written as (2x+3=y+2).
PRESBURGER ARITHMETIC
 Mojzesz Presburger proved Presburger arithmetic to be:
 Consistent : There is no statement in Presburger arithmetic which can be
deduced from the axioms such that its negation can also be deduced.
 Complete : For each statement in Presburger arithmetic, either it is possible to
deduce it from the axioms or it is possible to deduce its negation.
 Decidable : There exists an algorithm which decides whether any given
statement in Presburger arithmetic is true or false.
 Fischer and Rabin (1974) proved that every algorithm which decides the truth of
Presburger statements has a running time of at least 22^(cn) for some constant c,
where n is the length of the Presburger statement. Therefore, the problem is one
of the few currently known that provably requires more than polynomial run
time.
 The decidability of Presburger arithmetic can be shown using FINITE
AUTOMATA.
CONSTRUCTION OF FINITE AUTOMATA FOR
DECIDABILITY OF PRESBURGER ARITHMETIC
 Natural numbers can be encoded as finite words over the alphabet
{0,1} : it is sufficient to consider their binary representation, which
we write from right to left.
 The representation is not unique as we may add some zeroes on the
right. For example, we may represent the number thirteen as
1011,10110,…
 More generally, tuples of natural numbers can be represented in
binary notation as words over the alphabet {0,1}n, simply by
stacking them using an equal length representation for each
number. For example, the pair (thirteen, four) can be represented
as
1
0
1
1
0
0
1
0
or
1
0
1
1
0
0
0
1
0
0
 If we assume given, for all atomic formulae φ,π, automata Aφ ,Aπ
which accept the solutions of φ and π respectively, then for every
formula ψ, the automaton accepting ψ can be defined inductively as
follows :
 If ψ = φ ^ π , then A ψ = A φ ∩ Aπ i.e. the automaton accepting the intersection
language.
 If ψ = φ ˇ π , then A ψ = A φ U Aπ i.e. the automaton accepting the union
language.
 If ψ = ¬φ , then A ψ = A ¬φ is the automaton accepting the complement of the
language accepted by A φ.
 If ψ = x φ , then A ψ =A x φ is computed by projection.
 If ψ = x φ , then A ψ= A x φ = A ¬  x ¬φ
 If we want to decide the validity of the sentence ψ, it is sufficient to
compute Aψ and check whether it contains an accessible final state.
CONSTRUCTION OF FINITE AUTOMATA FOR THE
ATOMIC FORMULAE INVOLVING EQUATIONS
Given an atomic formula
(e)
a1x1 + . . . + anxn = k
We construct an automaton A = (Q ,  , T , [e] , F) .
We have  = {0,1}n.
We start from a set of states containing [e] where e is the equation to
be solved and the junk state [-]. [e] is the start state. The transition
rules T only contain initially the transition from [-] to itself by any
letter of the alphabet .Then we saturate Q and T according to the
following rules:
b1
If [a1x1 + . . . + anxn = k]  Q and  =.
.
.
bn

Then if k - (a1b1 + . . . + anbn) is even then
add
[a1x1 + . . . + anxn = k]
[a1x1 + . . . + anxn = (k – (a1b1 + . . . + anbn))/2]
to T and
[a1x1 + . . . + anxn = (k – (a1b1 + . . . + anbn))/2]
to Q.
If k - (a1b1 + . . . + anbn) is odd then add
[a1x1 + . . . + anxn = k]
[ - ] to T.
The final state is [a1x1 + . . . + anxn = 0] :
Every word in the set of solution might be followed eventually by a
sequence of
.
0
0
0
The automaton constructed is deterministic and complete.
Example :
Consider an atomic formula x + 2y = 3z + 2.
We can rewrite it as :
(e)
x + 2y - 3z = 2.
Here k=2 and our input alphabet is  = {0,1}3 , thus it contains :
0
0
0
0
1
1
1
1
0
0
1
1
0
0
1
1
0
1
0
1
0
1
0
1
Initially, set of states Q = { [x + 2y - 3z = 2] , [-] }.
0
For  = 0
,
0
k - (a1b1 + . . . + anbn) = 2 – ( 0 + 0 - 0) = 2 is even so, we add
[x + 2y - 3z = 2] → [x + 2y - 3z = (2-(0+0-0))/2]
0
0
0
 [x + 2y - 3z = 2]
[x + 2y - 3z = 1]
to T and [x + 2y – 3z = 1] to Q.
Similarly for  =
0
1
,
0
k - (a1b1 + . . . + anbn) = 2 – ( 0 + 2*1 - 0) = 0 is even so,
we add
[x + 2y - 3z = 2] → [x + 2y - 3z = (2-(0+2-0))/2]
0
1
0
 [x + 2y - 3z = 2]
[x + 2y - 3z = 0]
to T and [x + 2y – 3z = 0] to Q.
1
Similarly for  =
,
0
1
k - (a1b1 + . . . + anbn) = 2 – ( 1 + 2*0 – 3*1) = 4 is even so,
we add
[x + 2y - 3z = 2] → [x + 2y - 3z = (2-(1+0-3))/2]
1
0
1
 [x + 2y - 3z = 2]
to T .
[x + 2y - 3z = 2]
1
Similarly for  = 1
,
1
k - (a1b1 + . . . + anbn) = 2 – ( 1 + 2*1 – 3*1) = 2 is even so,
we add
[x + 2y - 3z = 2] → [x + 2y - 3z = (2-(1+2-3))/2]
1
1
1
 [x + 2y - 3z = 2]
to T .
[x + 2y - 3z = 1]
0
Now for  =
0
,
1
k - (a1b1 + . . . + anbn) = 2 – ( 0 + 0 – 3*1) = 5 is odd so,
we add
0
1
0
 [x + 2y - 3z = 2]
[-]
0
to T. Similarly for  =
1
1
transitions to dead state.
1
,
0
0
1
and
1
0
we have
This can be shown as :
1
0
1
0
1
1
0
1
0
x +2y-3z=1
x+2y-3z=2
0
1
0
x+2y-3z=0
Transitions to the dead state are not shown.
Now we need to saturate the sets Q and T. We need to find the
transitions for the state [x+2y-3z=1].Here k=1.
0
For  = 0
,
1
k - (a1b1 + . . . + anbn) = 1 – ( 0 + 0 – 3*1) = 4 is even so, we add
[x + 2y - 3z = 1] → [x + 2y - 3z = (1-(0+0-3))/2]
0
0
1
 [x + 2y - 3z = 1]
to T .
[x + 2y - 3z = 2]
Continuing in this manner, the set of states Q now contains 5 states :
[x+2y-3z=2]
[x+2y-3z=1]
[x+2y-3z=0]
[x+2y-3z=-1]
[x+2y-3z=-2]
The start state is [x+2y-3z=2] and the final state is [x+2y-3z=0]
And the transition diagram can be shown as :
0
0
1
1
1
1
0
1
0
0
0
0
0
1
1
1
0
1
x+2y-3z= -2
x+2y-3z=2
x+2y-3z=0
1
1
0
0
0
1
1
0
1
1 0
0
1
1
0
0
1
0
1
0
1
x+2y-3z=-1
x+2y-3z=1
1
1
0
0
1
0
0
1
1
1 0
0
0
1
1
1
0
0
1
1
0
CONSTRUCTION OF FINITE AUTOMATA FOR
THE ATOMIC FORMULAE INVOLVING
DISEQUATIONS
Turning the automaton A recognizing the solutions of an equation e
into one recognizing the solutions of the disequation ¬e is
straightforward : A being complete and deterministic, we just have
to say that the accepting state is no longer accepting and that all the
other states are accepting.
CONSTRUCTION OF FINITE AUTOMATA FOR THE
ATOMIC FORMULAE INVOLVING INEQUATIONS
Given an atomic formula
(e)
a1x1 + . . . + anxn  k
The only case where this equation has no solution is when k is
negative and a1. . . an are all positive. In this case, the automaton is a
trivial one, with only one non-accepting state. Otherwise we start
from a set of states containing [e] where e is the equation to be
solved and the junk state [-]. [e] is the start state. Then the
transitions are generated as follows :
b1
.
.
If [a1x1 + . . . + anxn  k]  Q and  =

.
bn
Then if k0 or ai <0 for some i, then add
[a1x1 + . . . + anxn  k]

[a1x1 + . . . + anxn   (k – (a1b1 + . . . + anbn))/2 ]
to T and
[a1x1 + . . . + anxn   (k – (a1b1 + . . . + anbn))/2 ]
to Q
if k<0 and a1 >0, . . . ,an >0, then add
[a1x1 + . . . + anxn  k]
[-]
to T.
The accepting states are all those labeled by an
0
inequation for which
0
.
is a solution, that is , the
.
0
states [a1x1 + . . . + anxn  k] for which k0. The automata computed
is
deterministic and complete.
PROJECTION CONSTRUCTION FOR THE PRESENCE
OF EXISTENTIAL QUANTIFIER
This can be done simply by removing the corresponding component
in the transition rules.
Consider the equation
z x+2y-3z=2
The construction of an automaton for this formula can be done simply
by constructing the automaton for the equation
x+2y-3z=2
on the alphabet {0,1}3 and then removing the row corresponding to z
from the inputs on the transitions . Here we remove the last row
from the tuple. The resulting automaton will then be nondeterministic and can be shown as :
0
1
1
0
1
0
1
1
0
0
1
0
x+2y-3z= -2
x+2y-3z=2
x+2y-3z=0
1
0
1
1
1
0
1
1
0
0
0
1
1
1
0
0
0
x+2y-3z=-1
x+2y-3z=1
1
1
0
1
0
1
0
0
0
0
1
CONCLUSION
We saw an introduction to Presburger Arithmetic ,
and also how to construct a finite automata for its
decidability by checking its emptiness..
THANK YOU..