Decidability of MSO Theories
東北大ロジックセミナ 金曜セミナ
Friday, 9 July 2010
We present basic results and techniques related to the
decidability of monadic second order (MSO) theories.
Outline
• Rabin’s Theorem .
• Decidability of MSO‐theory of countable linearly ordered sets
Review
Definition
A Rabin automaton over Σ is , , , such that 1. is a finite set of states,
2. is the set of initial states,
3. : Σ , called the transition table, and 4. whose elements are designated subsets of .
Rabin’s Theorem
Lemma (Rabin ’69)
Rabin automata are effectively closed under union, intersection, complementation, and projection.
From now on, we will concentrate on the MSO theory of two
successor’s structure,
The MSO Logic of two successor
We define the language for MSO of two successor.
The symbols which we use in this logic (language) are the following:
1. We use symbols , , , …, called individual variables. 2. We use the symbols , , , …, called set variables. 3. We use symbols , .
4.We use symbols represent the structure of binary tree and symbol and whose meaning is simply two unary operation s.t.,
, and .
5. We use logical connectives &, , , , and quantifiers , .
6.We also use nonlogical symbols and , left and right parentheses.
Satisfiability and Theories
We fix the structure , , , .
Suppose that to each individual variable and a set variable , we assigned an element and a set .
i.e., we have fixed an interpretation
: , :
We define satisfaction of Φ on under the interpretation Φ .
Definition (Basic Step)
• , … , if , … , .
• , … , , … ,
if , … , , … , .
• if .
• , … , , … , , … , if it is indeed the case
that the ‐tuple , … , , … , , … , .
Definition (Inductive Step)
• Φ Φ if Φ or Φ .
• Φ & Φ if Φ and Φ .
• Φ Φ if Φ or Φ Φ .
• Φ if Φ .
• Φ if s.t., Φ under the new
which is the same as except its value on is .
• Φ if s.t., Φ under the new
which is the same as except its value on is .
• Φ if Φ .
• Φ if Φ .
Definition
The formulas Φ , … , , , … , and , … , , , … , are equivalent in a structure if , … , and , … , ,
Φ , … , , , … , iff , … , , , … , .
Definition
The MSO theory of the structure , , , of two successor functions is denoted by .
Definability in and Decidability of
Definition
Let .
We say that is definable if Φ , … , , , … , s.t.,
, … , , , … , | Φ , … , , , … , .
Σ‐Valued Trees as Structures
Suppose that , is a Σ‐valued tree. Take a symbol Σ. Define subset on :
, iff
Example
Suppose Σ , , . Consider a Σ‐valued tree , defined by: if | |
if | | if | |
This valuation defines the following subsets:
| | , ,
| | , ,
| | , .
So, we have the structure , , , , , , .
In general, given Σ‐valued tree , with Σ , … , , define , , , , , … , .
There is another way to look structure .
Example
Let Σ , , . We identify the alphabet with the subset of the alphabet , in such a way that
, , .
Now the valuation considered in previous example can be expressed if | |
if | | if | |
The valuation defines the pair , as follows:
iff the component of . iff the component of . Similarly for .
Hence, we see that
| | | | ,
| | | | .
Consider the sets and just defined above. The pair , determines a valuation :
,
where iff .
From Rabin Automata to Formulas
Let , , , be a Rabin automaton over Σ.
Let , … , and , … , (denoted by ).
Define a symbol of Σ:
, … , ,
where for each , iff or
o. w
We denote this Σ‐valued tree by tree , .
The opposite is also true:
Any Σ‐valued tree , defines an ‐tuple of sets , … , , where
, , and ,
iff the component of , iff the component of .
Theorem
There exists a procedure which, given a Rabin automaton
, , , , constructs a formula Φ , such that the following property holds:
accepts tree iff Φ .
Proof.
Let , , , be a given Rabin automaton. Since is a finite set we can also suppose that
, , … , with being the initial state.
Let Σ be of the form
,
where each , .
We define the formula Φ , , where is , … , , as follows:
Φ , , … , & … & ,
where if
if
Let , , … , be set variables.
We write down the following formula , where is , … , :
& & &
i.e., automaton cannot be in two distinct states simultaneously.
We define another formula Φ , , , such that
& Φ , & .
, ,
Informally, the formula corresponds to the fact that:
if is in state , the next input signal is ,
then the automaton splits itself into two (left and right) copies such that the left copy is in state and the right copy is in state so that
, , .
Finally, the last formula we need is the formula which states that, , & such that the following properties hold:
1. .
2. & , if , , for which and .
The formula is intended to code the notion of successful computation.
Now, we write down the desired formula Φ , … , :
… & & & , Φ , , , & .
Now our goal is to show that the formula Φ satisfies the theorem.
We need to prove: ,
accepts tree iff Φ .
Suppose that accepts the tree .
Therefore, : s.t., ,
| for infinitely many .
We need to prove that
Φ ,
i.e., we need to show that there are subsets , … , on the tree
Φ under the new : , , … , .
Here is how we define each , , … , :
| .
Now suppose that Φ . To prove: accepts tree .
There are subsets , … , such that Φ .
, consider set such that , where .
Hence we have a mapping : .
One can check that the function
, ,
is a run of on the tree .
Moreover, the run is a successful run.
From Formulas to Rabin Automata
Definition
Let Φ , be a formula and let be a Rabin automaton over , . represents Φ , if , ,
accepts tree , iff Φ , .
Lemma
Suppose that Rabin automata and represent the formulas Φ , and Φ , , respectively. Then there exist Rabin automata representing
Φ , Φ , , Φ , , Φ , , and Φ , ,
where , &, , , , , … , , , … , .
Lemma
Let Φ be an atomic formula. There exists an automaton which represents Φ.
Theorem
There exists a procedure which for every MSO formula Φ , constructs a Rabin automaton representing the formula.
Proof. Note that Rabin tree automata are effectively closed under union, intersection, complementation, and projection.
The lemma above proves the theorem for atomic formulas that is for the basic step of our induction.
Another lemma above proves the inductive step and hence the
theorem.
Theorem
The MSO theory of two successors is decidable.
Proof. Let Ψ be a sentence. We want to check whether or not Ψ.
Consider the case when the sentence Ψ has the form Φ .
By previous theorem, there exists a Rabin automaton representing
Φ .
We conclude that,
, Φ iff accepts tree .
Thus, such that,
Φ iff tree accepted by . It follows that Φ holds in iff .
Thus we have reduced the satisfiability problem for Φ to the emptiness problem for a Rabin automaton representing Φ .
Since the emptiness problem for Rabin automata is decidable, we see that is also decidable. The theorem is proved.
Applications to Linear Ordered Sets
Definition
A linearly ordered set , is embedded into a linearly ordered set , if there exists a mapping : such that
1. for all , , if , then ; 2. for all distinct , , .
The function is called an embedding of , into , .
Fact 1
Any countable linearly ordered set , can be embedded into , , that is the linearly ordered set of rational numbers ordered naturally.
Proof.
Stage 0.
We set .
Stage 1.
We take . There are two cases to consider:
i) if , then we assign s.t., .
ii) If , then we set s.t., .
In either case we set and .
Clearly, extends .
Stage t + 1.
Assume that we have defined the function at the previous stage,
such that , … , .
For we have three cases.
Case 1. If , … , , then we assign such that
, … , .
Case 2. If , … , , then we assign such that
, … , .
Case 3. Assume that for some . Then
which is .
We set has constructed such that .
We can see that is indeed a desired isomorphic embedding from
, into , .
Proposition
The linearly order set of the rational number , has the following two properties:
1. (Density) , if , then such that .
2. The linearly ordered set , possesses neither a greatest nor a smallest element, i.e., , , s.t., and .
Definition
A linearly ordered set , is ‐like if it is dense and possesses no greatest or smallest element.
Fact 2
Two countable ‐like linearly ordered sets are isomorphic. In particular, every ‐like is isomorphic , .
Theorem
The MSO theory of all countable linearly ordered sets is decidable.
Proof. Let be
| and the string occurs in just once}.
Lemma
The set is definable.
Let be the restriction of to the set .
Lemma
The pair set , is isomorphic to the linearly ordered set , .
Proof. Clearly , is a linearly ordered set.
We need to show that , is ‐like. Then by the Fact 2, the lemma will be proved.
Let . Then, and .
Note that and .
We conclude that , has no maximal or minimal elements.
Now assume that . Then, such that:
and .
Then clearly .
We conclude that .
Hence the linearly ordered set , is ‐like.
By Fact 2, , is isomorphic to , . The lemma is proved.
Let be a formula of the MSO logic of linearly ordered sets.
We transform into the formula by induction as follows:
Basic Step.
Atomic formulas and are transformed into and , respectively.
Inductive Step.
If Φ Φ Φ , where , &, or Φ Φ , then we set
Φ Φ Φ or Φ Φ
where , &, .
If Φ is any formulas
Φ , Φ ,
then we transform Φ into
& Φ ,
& Φ ,
respectively.
If Φ is any of the formulas
Φ , Φ ,
then we transform it into
& Φ ,
& Φ ,
respectively.
Now we can see that Φ is true in all countable linearly ordered sets iff the transformed formula Φ belongs to .
Emptiness of automata
(W) MSO over finite words (W) MSO over finite trees
Presburger arithmetic
FO over ,
MSO over countable
We briefly review decidability results for MSO logics interpreted over tree structure.
We did not mention:
• fragments of MSO logics and other non‐classical logics
(transitive closure logics, ‐calculus, interval logics, branching time logic)
• game theoretic problems, which deal with winning strategies over infinite transition systems.
• equivalence testing problem, which consist in deciding isomorphism, bisimilarity, similarity, ..., etc.
• Definability and decidability questions related to first‐order fragments of arithmetic (Presburger arithmetic, Skolem arithmetic).
