
Recent Posts
 Predicate Logic Without Negation March 24, 2020
 Conjunctive Satisfiability with Functions and Inequalities March 13, 2020
 Modal Logic Provability February 14, 2020
 Modal Logic S5Satisfiability January 31, 2020
 First Order Theory of Equality January 17, 2020
Recent Comments
Archives
 March 2020
 February 2020
 January 2020
 December 2019
 November 2019
 October 2019
 September 2019
 August 2019
 July 2019
 June 2019
 May 2019
 April 2019
 March 2019
 February 2019
 January 2019
 December 2018
 November 2018
 October 2018
 September 2018
 August 2018
 July 2018
 June 2018
 May 2018
 April 2018
 March 2018
 February 2018
 January 2018
 December 2017
 November 2017
 October 2017
 September 2017
 August 2017
 July 2017
 June 2017
 May 2017
 April 2017
 March 2017
 February 2017
 January 2017
 December 2016
 November 2016
 October 2016
 September 2016
 August 2016
 July 2016
 June 2016
 May 2016
 April 2016
 March 2016
 February 2016
 January 2016
 December 2015
 November 2015
 October 2015
 September 2015
 August 2015
 July 2015
 June 2015
 May 2015
 April 2015
 March 2015
 February 2015
 January 2015
 December 2014
 November 2014
 October 2014
 September 2014
 August 2014
 July 2014
 June 2014
Categories
 Algebra and Number Theory
 Appendix Algebra and Number Theory
 Appendix Automata and Language Theory
 Appendix Games and Puzzles
 Appendix Mathematical Programming
 Appendix Network Design
 Appendix Program Optimization
 Appendix Sets and Partitions
 AppendixGraph Theory
 AppendixLogic
 Appendix: Sequencing and Scheduling
 Appendix: Storage and Retrieval
 Chapter 3 Exercises
 Core Problems
 Overview
 Problems not in appendix
 Uncategorized
Meta
Category Archives: Appendix Automata and Language Theory
Protected: Linear Bounded Automaton Acceptance
Enter your password to view comments.
Posted in Appendix Automata and Language Theory
Tagged 3SAT, AL3, Difficulty 5, Generic Reduction, Linear Bounded Automaton Acceptance
Minimum Inferred Finite State Automaton
Here’s the actual problem my student Dan Thornton spent most of his semester trying to understand and prove. It’s pretty crazy.
The problem: Automaton Identification from Given Data. We abbreviate it “AutID”. G&J call this problem “Minimum Inferred Finite State Automaton” and it is problem AL8 in the appendix.
The description: Given a finite set of data, is it possible to build a deterministic finite automata of or fewer states that agrees with the data?
Prior to giving a description of this problem we must introduce a few concepts and definitions. We want to construct a finite automation, this means a Mealy model deterministic finite automata. Formally a 6tuple of the form
 is the input alphabet, where is an individual character, and is a string.
 the set of states in the model. refers to an individual state. may equivalently be referred to as the set of all equivalence classes , with representative element . Each equivalence class is a set of all input strings such that .
 the output alphabet, where is a individual character, .
 is the transition function.
 is the output function.
 Both of the above functions may be extended in a natural way so that
and respectively. Usage should be clear from context.
 Both of the above functions may be extended in a natural way so that
 is the start state.
We use the standard convention that refers to the empty string of no characters.
A black box is similar to an ‘unknown’ Mealy model with the restriction that for any input string we only get to see the last output character returns. Consider the following black box. With input alphabet and output alphabet .
So if the above known black box was passed the string the complete Mealy model’s output function would give us back the string where as the black box would only give us back .
Now our above finite automata is constructed using data we are given, here we assume that data is a set of finite pairs of the form .
such that is not empty and for .
An automata agrees with data if for every datum , the final output character of .
Formal Problem Statement:
Given input alphabet , output alphabet and data, a set of finite pairs determine if an automation of or fewer states exists that agrees with D.
The Reduction:
The reduction by Gold uses Monotone EQ SAT. So we are given a conjunction of clauses where each clause in contains all negated or nonnegated variables and the number of clauses and variables is equal, is there an assignment of the variables so that is satisfied? Our instance will have clauses and variables. Clauses will be numbered and variables will be numbered .
In the above instance of Monotone EQ SAT we do not have a variable . Indices in our reduction will sometimes force us to reference . We may think of this variable as simply a place holder for .
The idea behind this reduction is that we may encode our instance of Monotone EQ SAT into data in such a way that if we can create a finite automata from our encoding, then we can use it to obtain a solution to the instance of Monotone EQ SAT if one exists.
Aut ID construction:
Here we transform our instance of Monotone EQ SAT into data , to do so we need the following functions:
The bounds on the above functions are a result of our numbering of clauses and . Note that is really a placeholder for .
Given a propositional formula which is an instance of MonotoneEQ SAT we encode it by the following:
 The variables of are encoded by the set
. Here each corresponds to the element where is an element of the output alphabet, .  We encode the clauses of by for , . Here each clause has a \textit{identifying tag}, , then the term is used specify a particular variable, . Importantly, datum in this set for which returns are thrown out.
 Each clause encoding will be only if clause does not contain variable , otherwise will be and is thrown out.
 We then encode whether each clause is a set of all negated, or nonnegated variables. for .
As a simple example we convert to data the following formula
So after our conversion we get:
Aut ID instance
Now we create an instance of by letting be the number of variables and .
True{Aut ID} True{Monotone EQ SAT}
Now we may assume that we have a finite automata that agrees with the data in . Now we may use the transition function and the output function to deduce properties of .
Let be , this is the state that is in after receiving the input string .
A splitting string of and is a string so that differs from . If such a string exists then obviously . If two states do not have splitting string then they are equivalent
We define variable states as follows, a variable has the encoding , so is ‘s variable state, we will sometimes refer to this as .
Clause states are defined in a manner similar to variable states. A clause corresponds to the identifying tag in the encoding of or , so is ‘s clause state, we will sometimes refer to this as .
In the following theorems we shall talk of assignment of clause state to variable state , this means that these two states are equivalent or alternatively that there does not exist a splitting string of and .
Theorem 1:All variable states are different.
Proof. We assume two variable states are equal and where . Then in the encoding of we get and respectively. But now we may define the splitting string . The final element of is defined in our data as . By a similar argument we get where , in our data this corresponds to one of the entries . Our automata must agree with the data, so as a result these states and cannot be equal. Thus we have reached a contradiction.
Theorem 2: Each state in our finite automata corresponds to exactly one variable.
Proof. The above follows by the pigeonhole principle, as has exactly states, there are variable states, and by Theorem 1, no two variable states are equal.
By the above we may talk about the states of in term of the variable each state corresponds to.
Theorem 3: If clause state and variable state are equal, Then clause contains variable .
Proof. Assume = and is not contained in . Once again we have the following encodings and that were defined in our construction of . Now we may define a splitting string . When we append the splitting string to each of the above encodings we get and . Both of these strings are defined in our data as and respectively, and by our assumption that is not contained in , So by the a conclusion identical to that of Theorem 1, and our theorem follows.
Theorem 4:No two clause states and may be equal if they are of opposite composition, meaning one has all negated variables, and the other all unnegated variables.
Proof. Once again we proceed by contradiction, assume and that , are of opposite composition. Once again we get each clauses encoding and respectively. Now we may define the splitting string . Looking at the final character output by we see and . It follows that as and are of opposite composition. Thus we arrive at a contradiction.
Theorem 5: gives us a solution to our instance of .
Proof. By Theorem 2 every clause state must be assigned to a single variable state, notice this does not mean only a single assignment is possible but just the given automata will give a single assignment. By Theorem 1 no clause may be assigned more than one variable state. By Theorem 3 a clause may be assigned to a variable state only if the clause contains the variable. So we see that our automata assigns clauses to the variables that could potentially satisfy them. Furthermore by Theorem 4, each variable state is given clauses of only one composition, so there is an obvious variable assignment to satisfy all of the clause states equal to a given variable state.
True{Monotone EQ SAT} True{Aut ID}
Now we assume there exists a mapping that satisfies our instance of Monotone EQ SAT, with clauses and variables. From this mapping we build a finite automata that agrees with all data .
We let ‘s 0transitions refer to transitions on input 0. Similarly 1transitions refer to the transitions on input 1.
So first we define all 1transitions as given in the following example automata, obviously such transitions will satisfy all data in .
Now for to satisfy all of the data in we notice by Theorems 3 and 4 above mapping each clause to the variable state that satisfies it seems like a natural thing to do. We may determine this mapping of clauses to the variables that satisfy them from our truth assignment that satisfies , .
Such mappings may be added to by noticing the following, as soon as we encounter a 0 in input we must transition to a clause state. So we may define a 0transition for every state in that maps the clause state (which recall corresponds to the string ) to the variable state that satisfies it. When adding 0transitions we must be careful as if clause is satisfied by variable then in order to agree with the data in we really should map to variable due to the definition of .
Now we must assign an output to each of these 0transitions. To do so we iterate through every clause state by sequentially considering . At each clause state we assign the output of the 0transition starting at this state to be . Notice that if two clause states and are identical, then they must both be satisfied by the same variable and so therefore .
Below is an example of adding such a 0transition and assigning it’s output:
The Blue edge is the zero transition added that maps the clause state ,which corresponds to the string , to the variable state . Semantically this means that the variable satisfies this clause.
The Red edge shows us adding the output value of a 0transition, as from the above blue edge we know corresponds to the clause ‘s clause state, so to the zero transition from this clause state will have output .
Theorem 6: Our constructed automata agrees with all
Proof. This is quite obvious from our example of in Figure 1. We have defined all the transitions, and notice that the final output of all if and this exactly matches our data .
Theorem 7: Our constructed automata agrees with all
Proof:Here we consider the final character output of for all encodings of fixed clause , these encodings are precisely the for . Now with the addition of the transitions, we transition into , and from this state we only worry about transitions. Recall that in our definition of , all datum are of the form . In there is a single transition that outputs the nonzero value . To agree with it is sufficient to make sure that this nonzero output occurs for an input string not in .
From our assignment of transitions defined above this singular transition that outputs will occur for the variable that satisfies , so then must be in . So will give the datum (,1). Now notice the corresponding entry in as defined by would be (,), but all of these datum were removed from . So the sufficiency condition above is satisfied.
Theorem 8 :Our constructed automata agrees with all
Proof: The manner in which we defined our 0 transitions explicitly involved a term, so for any clause state , now a 0 transition as defined above will output which will obviously agree with
By Theorem 6, Theorem 7, and Theorem 8. We conclude that will agree with data
(Back to me)
Difficulty: 9. This is basically the reduction in the Gold paper, though Dan reorganized it a bunch to make it fit our format, and be more understandable. But the formatting of the various variables, the fact that you need to define the I_{F} function on variable k to talk about z_{lk} instead of z_{k}, and the three different kinds of test data all make this super hard to understand. In some ways, I wonder if this should be a 10, given the work we did on it. But I’m saving the 10’s for things that are truly impenetrable, and we did manage to figure this one out.