Transcript MONADIC SECOND ORDER LOGIC

BϋCHI’S MONADIC SECOND
ORDER LOGIC
Verification Seminar
V.Sowjanya Lakshmi ( [email protected])
Subhasree M. ([email protected])
CONTENTS






Introduction
Syntax of S1S
Semantics of S1S
Satisfiability of S1S
Proof
Conclusion
INTRODUCTION



Logic interpreted over Natural
Numbers, N0={0,1,…..}
Quantification over individual
elements of N0 and subsets of N0
Natural ordering of N0 (unique and
one successor)
SYNTAX

Terms

Atomic Formulas

Formulas
TERM
A term is built up from constant 0 and
individual variables x,y,… by
application of
successor function succ.
Examples of terms:
0,succ(x),succ(succ(succ(67))),
succ(succ(y))
ATOMIC FORMULAS
An atomic formula is of the form
t t’ or
tX
where t and t’ are terms and
X is a set variable
FORMULAS


A formula is built up from atomic
formulas using the Boolean connectives
(not),(or) with the existential
quantifier ()
Existential quantifier () can be applied
to both individual variables and set
variables.
Examples of formulas:
, , (x), (X)

Remaining Boolean connectives are
defined using (not) and (or).
Examples:
 is defined as  ()
  is defined as ()
 is defined as ()  ()
UNIVERSAL QUANTIFIER
Universal quantifier  is defined using 
(x)  is defined as  ((x)   )
(X)  is defined as  ((X)   )
EXAMPLES of Formulas
xX is defined as  x  X
 X  Y is defined as
x [(x  X  x  Y)  (x  Y  x  X )]
 Sub(X,Y) is defined as
(x) (x  X  x  Y)
 Zero(x) is defined as
(x) [(x  X )   (y)(y x)]

Examples


Sing(X ) is defined as
( Y )[Sub(Y,X) (Y X)  (Z )
(Sub (Z,Y )  (Z Y ) )]
Lt(x,y) is defined as
Z [succ(x)  Z (Z )(z  Z 
succ(z)  Z )] (y  Z )
SEMANTICS




Formulas are interpreted over N0
Individual variables x,y,..are interpreted
as natural numbers ie. elements of N0
Function Successor corresponding to
adding one
t t’ is true provided t and t’ denote
the same natural number
Semantics ..


Set variables like X,Y,.. are interpreted
as subsets of N0
t  X is true iff the number denoted by
t belongs to the set denoted by X
Free and bound variables


A variable is said to occur free in a
formula if it is not within the scope of a
quantifier
Variables which do not occur free are
said to be bound
Example:
(x) [(x  X )   (y)(y x)]
x and y are bound variables
X is free variable




(x1,x2,..,xk,..,X1,X2,..,Xl) indicates all the variables
which occur free come from {x1,x2,..,xk,..,X1,X2,..,Xl}
To assign a truth value to the
formula(x1,x2,..,xk,..,X1,X2,..,Xl) ,map each individual
variable xi to a natural number miN0
and each set variable Xj to a subset MjN0
M╞  (X) denote that  is true under the
interpretation {xi→mi} i {1,2,..,k} and
{Xi→Mi } i {1,2,.., l}
Examples




(M,N) ╞ Sub(X,Y) iff
MN
M ╞ Zero(X) iff
0M
(m,n) ╞ Lt(x,y) iff
m<n
M ╞ Sing(X) iff
M is a singleton {m}
Sentence
A sentence is a formula in which no
variables occur free
 A sentence is either true or false
 Assigning values is not needed
X [0  X (x)(x  X  succ (x)  X )]
(x) (x X)

SATISFIABILITY

An S1S formula is (x1,x2,..,xk,X1,X2,..,Xl ) is
said to be satisfiable if we can choose
M1= (m1,m2,..,mk,M1,M2,..,Ml ) such that
M1╞ (X1), where X1= (x1,x2,..,xk,X1,X2,..,Xl )


Büchi showed that every word in L has an
interpretation for the free variables in 
under which  evaluates to true
Every interpretation which makes  true is
represented by some word in L
Satisfiability...


 is satisfiable iff there is some
interpretation which makes it true iff L
is nonempty
The language L is defined over the
alphabet {0,1}m where m is the number
of free variables in 
Language L  ({0,1}m)) is S1S
definable if L= L for some formula 
 Any Language L   can be converted
into an equivalent language L {0,1}
over{0,1}m
 L ={ αM | M1╞ (X1)}
 L {0,1}={α {0,1} | α L}

THEOREM


Let  be an S1S formula . Then L is an
-regular language
Let L be an -regular language. Then L{0,1}
is S1S definable
Theorem: Let  be an S1S formula.
Then L is an -regular language
Proof:



Proof is by induction on the structure of 
An equivalent language S1S0 is introduced
S1S0 does not have individual variables, xi




All variables in S1S0 are set variables, Xj
Atomic formulas are of the form X ⊆Y and
succ (X,Y )
X ⊆Y is true if X is a subset of Y
Succ ( X,Y ) is true if X and Y are singletons
{x } and {y } respectively and y = x +1
Converting S1S formula  to S1S0
formula 0 such that L = L0

Removing nested application of successor
function
succ (succ (x ))X ) can be written as
(∃y)(∃z) y =succ(x) ∧z = succ (y)∧z X

Eliminating formulas of the form 0 X using
the formula Zero ( X )
Eliminating singleton variables, using the
formula Sing
( x) (∃y) succ(x) = y ∧y Z can be written as
( X) (Sing ( X ) [(∃y ) Sing ( Y ) ∧
succ ( X,Y ) ∧Y ⊆ Z ] )

Construct a Büchi Automaton
(A ,G ) for S1S0 formula 

 = X ⊆Y
<0,0>, <0,1>, <1,1>
S1
<1,0>
S2
Construct a Büchi Automaton
(A ,G ) for S1S0 formula 
 = succ (X,Y )
<0,0>
<0,0>
<1,0>
S1
S2
<0,1>
S3
Induction Step
Considering the connectives ⌐,∨ and ∃X


 = ⌐Ψ, construct the complement of Ψ
 = 1∨ 2 ,construct 1  2

 =(∃X1 ) Ψ(X1,X2,..,Xl ) , the language
corresponds to the projection of LΨ via
the function
Π:{0,1}m →{0,1} m-1, erases the first
component of each m-tuple in {0,1}m
Let L be an -regular language.
Then L{0,1} is S1S definable.
Proof:
(A,G) –Büchi Automaton recognizing L⊆ 
= {a1,a2,..,am} , A=(S,→, Sin ) with S = {s1,s2,..,sk}
A1,A2,..,Am are the free variables
A1 describes the positions in which the input where letter ai occurs
S1,S2,..,Sk describes the runs
Sj describes the positions in the run where the automaton is
in Sj
(∃S1) (∃ S2)…(∃ Sk)
( x)  i {1,2,..,m} (x  Ai)  i {1,2,..,m}
(x  Ai  (j i x Aj ) 
( x)  i {1,2,..,k} (x  Si)  i {1,2,..,k} (x  Si 
(j i x Sj ) 
( x)  Si Sin (0  Si)

( x)  (Si,, ai, sk)→ (x  Si)  (x  Aj)  (succ (x)  Sk)
 Si G ( x) (∃y) (x<y)  (y  Si)
Example
a
f
a,b
b
e
(∃Sf) (∃ Se)
( x) [(x  Aa)  (x  Ab)  (x  Aa  x Ab)
 (x  Ab  x Aa) ]

( x) [(x  Sf)  (x  Se)  (x  Sf  x Se)
 (x  Se x Sf)]
(0  Sf)


( x) [((x  Sf)  (x  Aa)  succ (x)  Sf) 
((x  Sf)  (x  Ab)  succ (x)  S2)  ((x  Se)  succ (x)  Se)]
( x) (∃y) (x<y)  (y  Sf)

Conclusion

Büchi has proved that Notions of S1S
definability and -regularity are
equivalent.
Reference
Madhavan Mukund. Linear Time Temporal
Logic and Büchi Automata
Thank You