3 min read

Introduction: Automata are the main modeling tools in Computer Science. Whenever we want to design a program, a protocol or an information system, or even just describe what it is intended to do, its characteristics, and its behavior, we use these special kinds of diagrams. Automata are systems consisting of states, some of them designated as initial or final, and (usually) labeled transitions. Formal definition Automaton

2 min read

Definition: Two finite accepters M1 and M2 are equivalent iff L(M1 ) = L(M2 ) i.e., if both accept the same language. Both DFA and NFA recognize the same class of languages. It is important to note that every NFA has an equivalent DFA. Let us illustrate the conversion of NDA to DFA through an example.

4 min read

Introduction: Given languages L,L1, and L2, new languages may be defined using various operations. First, consider the set operations of union, intersection, set difference, and symmetric difference. These familiar set operations help define new languages as defined below: Union:L1 ∪ L2 = {x | x ∈ L1 ∨ x ∈ L2} Intersection: L1 ∩ L2 = {x | x ∈ L1 ∧ x ∈ L2}

4 min read

Introduction: In this section, we: define several operations on languages; say what regular expressions are, what they mean, and what regular languages are; and begin to show how regular expressions can be processed by Forlan. The union, intersection and set-difference operations on sets are also operations on languages, i.e., if L1;L2 2 Lan, then L1 [ L2, L1 \ L2 and L1 ¡ L2 are all languages. (Since L1;L2 2 Lan, we have that L1 µ §¤1 and L2 µ §¤2 , for alphabets §1 and §2. Let § = §1 [ §2, so that § is an alphabet, L1 µ §¤ and L2 µ §¤. Thus L1 [ L2, L1 \ L2 and L1 ¡L2 are all subsets of §¤, and so are all languages.) The first new operation on languages is language concatenation. The concatenation of languages L1 and L2 (L1 @ L2) is the language

4 min read

THEOREM 1: If L1 and L2 are regular over S, then L1 L2 È is regular i.e., union of two regular sets is also regular. [Regular sets are closed w.r.t. union]. Proof: As L1 and L2 are given to be regular; there exists finite automata M1 Q 1 q1 F1 = ( , S,d , , ) and M2 Q2 2 q2 F2 = ( , S,d , , ) such that L1 = T(M1) and

4 min read

Introduction: A regular set (language) is a set accepted by a finite automaton. Closure: A set is closed under an operation if, whenever the operation is applied to members of the set, the result is also a member of the set. For example, the set of integers is closed under addition, because x y is an integer whenever x and y are integers. However, integers are not closed under division: if x and y are integers, x/y may or may not be an integer. There are several operations defined on languages:

2 min read

Example of a NFA, Nondeterministic Finite Automata givenby a) Machine DefinitionM = (Q, sigma, delta, q0, F) Q = { q0, q1, q2, q3, q4 } the set of states

2 min read

Introduction: Two-way finite automata are machines that can read input string in either direction. This type of machines have a “read head”, which can move left or right over the input string. Like the finite automata, the two-way finite automata also have a finite set Q of states and they can be either deterministic (2DFA) or nondeterministic (2NFA). They accept only regular sets like the ordinary finite automata. Let us assume that the symbols of the input string are occupying cells of a finite tape, one symbol per cell as shown in fig. The left and right end markers |— and —| enclose the input string. The end markers are not included in the input alphabet S.

4 min read

Introduction: If we do not allow writing or two-way operation of the tape head, we have what has been traditionally called a finite automaton. This machine is only allowed to read its input tape and then, on the basis of what it has read and processed, accept or reject the input This restricted machine operates by: a) Reading a symbol,

1 min read

Introduction: The DFA machine can exist in only one state at any given time. It accepts a string if starting from the start state and moving from state to state, each time following the arrow that corresponds the current input character, it reaches a final state when the entire input string is consumed. Otherwise, it rejects the string. A DFA is defined by the 5-tuple: {Q ∑ q F δ } Q ==> a finite set of states

3 min read

Introduction: Basic data structure or input to grammars or automaton is strings. Strings are defined over an alphabet which is finite. Alphabet may vary depending upon the application. Elements of an alphabet are called symbols. Usually we denote the basic alphabet set either as Σ or T. For example, the following are a few examples of an alphabet set. Σ1 = {a,b} Σ2 = {0,1,2}

4 min read

Introduction: In 1959, Noam Chomsky tried to give a mathematical definition for grammar. The motivation was to give a formal definition for grammar for English sentences. He defined four types of grammar viz., type 0, type 1, type 2, and type 3. At the same time, the programming language ALGOL was being considered. It was considered as a block-structured language and a grammar was required which could describe all syntactically correct programs. The definition given was called Backus Normal Form or Backus-Naur Form (BNF). This definition was found to be the same as the definition given by Chomsky for type 2 grammar. We now formally define the four types of grammars:A context-free grammar G is defined by the 4-tuple: Where

4 min read

Introduction: A binary relation on two sets A and B is a subset of A × B. For example, if A = {1, 3, 9}, B = {x, y}, then {(1, x), (3, y), (9, x)} is a binary relation on 2-sets. Binary relations on k–sets A1, A2,...,Ak can similarly be defined. Another basic concept on sets is function. A function is an object that sets up an input-output relationship. That is, a function takes an input and produces the required output. For a function f, with input x, the output y, we write f(x) = y. We also say that f maps x to y. For example, addition is a function which produces the sum of the numbers that are input. The set of possible inputs to a function is called its “domain.” The output of a function comes from a set called its “range.” Let D be the domain and R be the range of a function f. We denote this description of a function as “f: D → R”. For example, f is a function with domain Z and range Z, we write it as f: Z → Z. A function that uses all the elements of the range is said to be onto (surjective). A function “f: D → R” is said to be one-to-one or 1–1 (injective) if for any two distinct elements a, b ∊ D, f (a)≠f (b). A function which is both one-to-one and onto is called a bijective function. A binary relation K ⊆ A × B has an inverse, say K−1 ⊆ B × A defined as (b, a) ∊ K−1 if and only if (a, b) ∊ K. For example,

5 min read

Introduction: A set is a collection of well-defined objects. Usually the elements of a set have common properties. For example, all the students who enroll for a course ‘Computability’ make up a set. Formally,a set is an unordered collection of objects. The definition of a set is intuitive in nature and was stated by the German mathematician Cantor in 1895. The objects in a set are called the elements or members of the set. Example 1: The set E of even positive integers less than 20 can be expressed by: E = {2, 4, 6, 8, 10, 12, 14, 16, 18}, or

4 min read

Introduction: All the machines discuss in the Power diagram, including DFAs, are primarily string processors. They are started in their initial state and are fed an input string. The inputs of interest are finitely long (“finite”) strings. The main question of interest is whether, at the end of the input, the machine is in an accepting state or not. The Turing machine has, in addition to a set of accepting states, a set of rejecting states. There are several axes along which machines can be distinguished. Some of these distinctions are now pointed out. We will remind the reader of these details when specific machine types are discussed. The purpose of the current discussion is to portray the overall nature of the variations that exist among machines.

3 min read

Introduction: An undirected graph or simply a graph is a set of points with lines connecting some points. The points are called nodes or vertices. The lines are called edges. Types of graphs: 1. The number of edges at a particular vertex is the degree of the vertex. In Figure 1, degree of 1 is 3. No more than one edge is allowed between any two vertices. We label the vertices for convenience, and call the graph as labeled graph.

3 min read

Introduction: The time taken to execute any algorithm depends upon the machine on which it is implemented and also on the algorithm. Hence, efficiency of any algorithm is measured by the amount of time it takes and also the space it needs for execution on the machine. Comparison of algorithms has become an important topic. We give here a mathematical basis for comparing algorithms. A complexity function f is a function of n, the size of the problem or parameter on which the problem is dependent. That is, f (n) is either a measure of the time required to execute an algorithm on a problem of size n or the measure of memory space. If f (n) is describing the measure of time, then f(n) is called the time-complexity function; if f(n) is describing the measure of space, then it is called space-complexity function. We have the following important definitions of complexity functions.

4 min read

Introduction: The idea of using regular expressions to denote whole classes of strings is quite widespread. In many card games, the Joker card is called the “wild-card,” in that it can be used in lieu of any other card. In most operating systems, the wild-card is ∗that matches all file names—as in rm *.* or del *.*. Such expressions are practical examples of regular expressions in day-to-day use. Formally, we define regular expressions as follows. We use the inductive definition style in which a basis case and a list of inductive rules are provided, and define regular expressions to be the least set satisfying these rules: RE r1r2 denotes L(r1) ◦ L(r2) encoded in grail as r1 r2 RE r1 r2 denotes L(r1) ∪L(r2) encoded in grail as r1 r2

2 min read

Kleene Star, ‘∗’ Star performs the union of repeated exponentiations: L∗ = {x | ∃k ∈ N : x ∈ Lk}.

2 min read

Introduction: Conversion of The NFA simplifies computational design, but the use of nondeterministic selections and ǫ-transitions makes it look very different from FA.An NFA for a language can be smaller and easier to construct than a DFA. A Greedy Conversion Algorithm Step 1: For each state p ∈ Q and for each symbol a ∈Σ, compute the set R(p, a) of all states that can be reached from state p by:

2 min read

Introduction: An input string is accepted by a nondeterministic finite automaton if and only if at least one of the possible transition sequences, defined by the input, leads to a final state. As language recognizer devices, nondeterministic automata are not more powerful than their deterministic counterpart, indeed they accept the same class of languages, that is to say they are equivalent. However, they are very often more convenient to use. In many cases, the most direct formalization of a problem is in terms of a nondeterministic automaton. A NFA is represented formally by a 5-tuple, (Q, Σ, Δ, q0, F), consisting of a finite set of states Q

1 min read

o JA = X.B o KA = X’

4 min read

The mathematical study of the “Theory of Computation” begins by understanding the Mathematics of strings of symbols. Alphabet: It is defined as a finite set of symbols. Example: Roman alphabet {a, b, ...... z}.

2 min read

Introduction: “Boolean logic” is a system built with two values TRUE and FALSE. “Boolean values” are represented by values 0 and 1. There are many Boolean operations. (a) Negation: It means the NOT operation, represents by . Example: 0 = 1 and 1 = 0.

2 min read

An Illustration of homomorphisms: In parsing a programming language such as C, the parser appeals to a tokenizer that first recognizes the structure of tokens (sometimes called lexemes) such as integers, floating-point numbers, variable declarations, keywords, and such. The tokenizer pattern-matches according to regular expressions, while the parser analyzes the structure of the token stream using a context free grammar (context free grammars are discussed in Chapters 13 and 14; basically, they capture the essential lexical structure of most programming languages, such as nested brackets, begin/end blocks, etc.). Suppose one wants to get rid of the tokenizer and write a context free grammar up to the level of individual characters. Such a grammar can be obtained by substituting the character stream corresponding to each token in place of each token in a modularfashion, according to a homomorphism. For example, if begin were to be a keyword in the language, instead of treating it as a token keyword, one would introduce additional productions of the form begin -> b e g i n

3 min read

Machine types that accept non-regular languages: Consider the language L1 = {aibjck | i, j, k ≥ 0 ∧ if i = 1 then j = k}. In all the strings in this language, the characters a, b, and c appear in that order, with b’s and c’s being equal in number if the number of a’s is 1. This language can obviously be handled using a DPDA, using its stack. In fact,

3 min read

Introduction: There are two systematic methods available for listing the contents of sets of words. The first is known as the lexicographic order, or “order as in a dictionary” while the second is called the numeric order which lists strings by length-groups: all strings of a lower length are listed before a string of a higher length is listed. Within a length-group, the strings are listed in lexicographic order. We now present some details as well as examples. Lexicographic order for strings In this order, given two strings x and y, we compare the characters comprising x and y position by position. We do this for each position i ∈ min(length(x), length(y)) (here, min finds the minimum of two numbers). For example, if we compare apple and pig, we compare for each position i ∈ 3, as pig is the shorter of the two and has length 3.

4 min read

Principle of Pumping Lemma The “pumping lemma” for regular languages is another way of showing that a given infinite language is not regular. The proof is always done by “contradiction”. The technique that is followed is as outlined below: Applying the Pumping Lemma

3 min read

NFA with ε-moves: In forthcoming constructions it turns out to be useful to extend the notion of NFA by allowing spontaneous transitions. When an NFA executes a spontaneous transition, known as an "-move, it changes its state without reading any input letter. Any number of ε-moves are allowed. Example: Here's an example of an NFA with ε-moves:

2 min read

Solution (a) R.E = (b c)* a (b c)* [for all strings containing exact one a] (b) All strings containing no more than three a’s: We can describe the string containing zero, one, two or three a’s (and nothing else) as

3 min read

Myhill-Nerode Relations Isomorphism: Two DFAs given by M QM m sm Fm = ( , S,d , , ) and N QN n sn Fn = ( , S,d , , ) are said to be “isomorphic” if there is a one-to-one and onto mapping f : QM ®QN such that

1 min read

Regular Expressions to NFA

3 min read

Introduction: Despite their simple appearance, DFAs are incredibly powerful and versatile! Here are some examples of their power: Most questions about DFAs are algorithmically decidable. In particular, the following questions about DFAs are decidable: Does a given DFA accept a given input?

2 min read

Definition: A finite-state machine M = (Q, S,O,d, l, q ) 0 consists of a finite set Q ofstates, a finite input alphabet S, a finite output alphabet O, a transition functiond that assigns to each state and input pair a new state, an output function l thatassigns to each state and input pair an output, and an initial state q0. Let M = (Q, S,O,d, l, q ) 0 be a finite state machine. A state table is used to denote the values of the transition function d and the output function l for all pairs of states and input. Mealey Machine: Usually the finite automata have binary output, i.e., they accept the string or do not accept the string. This is basically decided on the basis of whether the final state is reached by the initial state. Removing this restriction, we are trying to consider a model where the outputs can be chosen from some other alphabet.

2 min read

Simplification of CFG-Introduction: In a Context Free Grammar (CFG), it may not be necessary to use all the symbols in V ÈT, or all the production rules in P while deriving sentences. Let us try to eliminate symbols and productions in G which are not useful in deriving sentences. Let G = (V,T, S, P) be a context-free grammar. Suppose that P contains a production of the form

2 min read

Pumping Lemma for CFG: A “Pumping Lemma” is a theorem used to show that, if certain strings belong to a language, then certain other strings must also belong to the language. Let us discuss a Pumping Lemma for CFL. We will show that , if L is a context-free language, then strings of L that are at least ‘m’ symbols long can be “pumped” to produce additional strings in L. The value of ‘m’ depends on the particular language.

5 min read

A Pumping Lemma for CFLs: Consider any CFG G = (N, Σ,P,S). A Pumping Lemma for the language of this grammar, L(G), can be derived by noting that a “very long string” w ∈ L(G) requires a very long derivation sequence to derive it from S. Since we only have a finite number of non-terminals, some non-terminal must repeat in this derivation sequence, and furthermore, the second occurrence of the non-terminal must be a result of expanding the first occurrence (it must lie within the parse tree generated by the first occurrence). For example, consider the CFG S -> (S) |T| e T -> [T] |T T| e. Here is an example derivation: S => ( S ) => ((T)) => (( [T] )) => (( [ ] )) Occurrence-1 Occurrence-2 Occurrence-1 involves Derivation-1: T => [ T ] => [ ] Occurrence-2 involves Derivation-2: T => e Here, the second T arises because we took T and expanded it into [ T ] and then to [ ]. Now, the basic idea is that we can use Derivation-1 used in the first occurrence in place of Derivation-2, to obtain a longer string: S => (S) => ((T)) => (( [ T ] )) => (( [[ T ]] )) => (( [[ ]] )) ^ ^ Occurrence-1 Use Derivation-1 here In the same fashion, we can use Derivation-2 in place of Derivation-1 to obtain a shorter string, as well: S => ( S ) => ( ( T ) ) => ( ( ) ) ^ Use Derivation-2 here When all this happens, we can find a repeating non-terminal that can be pumped up or down. In our present example, it is clear that we can manifest (([i ]i)) for i ≥ 0 by either applying Derivation-2 directly, or by applying some number of Derivation-1s followed by Derivation-2. In order to conveniently capture the conditions mentioned so far, it is good to resort to parse trees. Consider a CFG with |V | non-terminals, and with the right-hand side of each rule containing at most b syntactic elements (terminals or non-terminals). Consider a b-ary tree built up to height |V | 1, as shown in Figure 13.7. The string yielded on the frontier of the tree w = uvxyz. If there are two such parse trees for w, pick the one that has the fewest number of nodes. Now, if we avoid having the same non-terminal used in any path from the root to a leaf, basically each path will “enjoy” a growth up to height at most |V | (recall that the leaves are terminals). The string w = uvxyz is, in this case, of length at most b|V |. This implies that if we force the string to be of length b|V | 1 (called p hereafter), a parse tree for this string will have some path that repeats a non-terminal. Call the higher occurrence V1 and the lower occurrence (contained within V1) V2. Pick the lowest two such repeating pair of non-terminals. Now, we have these facts:

2 min read

Accepting Strings with NPDA (Formal Version) The notation “|–” is used to indicate a single move of an NPDA. “|–* ” is used to indicate a sequence of zero or more moves.

4 min read

Equivalence (Preorder plus Symmetry): An equivalence relation is reflexive, symmetric, and transitive. Consider the BB relation for three basketball players A, B, and C. Now, consider a “specialization” of this relation obtained by leaving out certain edges: ≡_BB = {A,A, A,B, B,A, B,B, C,C}. This relation is an equivalence relation, as can be easily verified. Note that ≡_BB =≤_BB ≤∩ ⁻¹ _BB. In other words, this equivalence relation is obtained by taking the preorder ≤ _BB and intersecting it with its inverse. The fact that BB ∩ ^−1 BB is an equivalence relation is not an accident. The following section demonstrates a general result in this regard. Intersecting a preorder and its inverse: Theorem 4.1. The relation obtained by intersecting a preorder r with its inverse r−1 is an equivalence relation. Proof: First we show that R∩R−1 is reflexive. Let R be a preorder over set S. Therefore, R is reflexive, i.e., it contains x, x pairs for every x ∈ S. From the definition of R−1, it also contains these pairs. Hence, the intersection contains these pairs. Therefore, R ∩ R−1 is reflexive. Next we show that R ∩ R−1 is symmetric. That is, to show that for every x, y ∈ S, x, y ∈ R ∩ R−1 implies y, x ∈ R ∩ R−1. If the antecedent, i.e., x, y ∈ R ∩ R−1 is false, the assertion is vacuously true. Consider when the antecedent is true for a certain x, y. These x and y must be such that x, y ∈ R and x, y ∈ R−1. The former implies that y, x ∈ R−1. The latter implies that y, x ∈ R. Hence, y, x ∈ R ∩ R−1. Hence, R ∩ R−1 is symmetric. Next we prove that R∩R−1 is transitive. Since R is a preorder, it is transitive. We now argue that the inverse of any transitive relation is transitive. From the definition of transitivity, for every x, y, z ∈ S, from the antecedents x, y ∈ R and y, z ∈ R, the consequent x, z ∈ R follows. From these antecedents, we have that y, x ∈ R−1 and z, y ∈ R−1 respectively. From the above conclusion x, z ∈ R, we can infer that z, x ∈ R−1. Hence, R−1 is transitive and so is the conjunction of R and R−1. Identity relation: Given a set S, the identity relation R over S is {x, x | x ∈ S}. An identity relation is one extreme (special case) of an equivalence relation. This relation is commonly denoted by the equality symbol, =, and relates equals with equals. Please note the contrast with Theorem 4.1. Universal relation: The universal relation R over S is S × S, and represents the other extreme of relating everything to everything else. This is often an uninteresting binary relation.2 Equivalence class: An equivalence relation R over S partitions elements(R) = domain(R)∪ codomain(R) into equivalence classes. Intuitively, the equivalence classes Ei are those subsets of elements(R) such that every pair of elements in Ei is related by R, and Eis are the maximal such subsets. More formally, given an equivalence relation R, there are two cases:

5 min read

Transitive, and Related Notions: To define transitivity in terms of graphs, we need the notions of a broken journey and a short cut. There is a broken journey from dot x to dot z via dot y, if there is an arrow from x to y and an arrow from y to z. Note that dot x might be the same as dot y, and dot y might be the same as dot z. Therefore if a, a ∈ R and a, b ∈ R, there is a broken journey from a to b via a. Example: there is a broken journey from Utah to Nevada via Arizona. There is also a broken journey from Utah to Nevada via Utah. There is a short cut just if there is an arrow direct from x to z. So if a, b ∈ R and b, c ∈ R and also a, c ∈ R, we have a broken journey from a to c via b, together with a short cut. Also if a, a ∈ R and a, b ∈ R, there is a broken journey from a to b via a, together with a short cut. Example: There is a broken journey from Utah to Nevada via Arizona, and a short cut from Utah to Nevada. R is transitive if for all x, y, z ∈ S, x, y ∈ R ∧ y, z ∈ R ⇒ x, z ∈ R. Equivalently, There is no broken journey without a short cut. R is intransitive if, for all x, y, z ∈ S, x, y ∈ R ∧ y, z ∈ R ⇒ x, z /∈ R. Equivalently,

2 min read

Greibach Normal Form: In Chomsky’s Normal Form (CNF), restrictions are put on the length of right sides of a production, whereas in Greibach Normal Form (GNF), restriction are put on the positions in which terminals and variables can appear. GNF is useful in simplifying some proofs and making constructions such as Push Down Automaton (PDA) accepting a CFG. Definition: A context-free grammar is said to be in Greibach Normal Form (GNF) if all productions have the form A-> ax,

5 min read

A Pumping Lemma for CFLs: Consider any CFG G = (N, Σ,P,S). A Pumping Lemma for the language of this grammar, L(G), can be derived by noting that a “very long string” w ∈ L(G) requires a very long derivation sequence to derive it from S. Since we only have a finite number of non-terminals, some non-terminal must repeat in this derivation sequence, and furthermore, the second occurrence of the non-terminal must be a result of expanding the first occurrence (it must lie within the parse tree generated by the first occurrence). For example, consider the CFG S -> (S) |T| e T -> [T] |T T| e. Here is an example derivation: S => ( S ) => ((T)) => (( [T] )) => (( [ ] )) Occurrence-1 Occurrence-2 Occurrence-1 involves Derivation-1: T => [ T ] => [ ] Occurrence-2 involves Derivation-2: T => e Here, the second T arises because we took T and expanded it into [ T ] and then to [ ]. Now, the basic idea is that we can use Derivation-1 used in the first occurrence in place of Derivation-2, to obtain a longer string: S => (S) => ((T)) => (( [ T ] )) => (( [[ T ]] )) => (( [[ ]] )) ^ ^ Occurrence-1 Use Derivation-1 here In the same fashion, we can use Derivation-2 in place of Derivation-1 to obtain a shorter string, as well: S => ( S ) => ( ( T ) ) => ( ( ) ) ^ Use Derivation-2 here When all this happens, we can find a repeating non-terminal that can be pumped up or down. In our present example, it is clear that we can manifest (([i ]i)) for i ≥ 0 by either applying Derivation-2 directly, or by applying some number of Derivation-1s followed by Derivation-2. In order to conveniently capture the conditions mentioned so far, it is good to resort to parse trees. Consider a CFG with |V | non-terminals, and with the right-hand side of each rule containing at most b syntactic elements (terminals or non-terminals). Consider a b-ary tree built up to height |V | 1, as shown in Figure 13.7. The string yielded on the frontier of the tree w = uvxyz. If there are two such parse trees for w, pick the one that has the fewest number of nodes. Now, if we avoid having the same non-terminal used in any path from the root to a leaf, basically each path will “enjoy” a growth up to height at most |V | (recall that the leaves are terminals). The string w = uvxyz is, in this case, of length at most b|V |. This implies that if we force the string to be of length b|V | 1 (called p hereafter), a parse tree for this string will have some path that repeats a non-terminal. Call the higher occurrence V1 and the lower occurrence (contained within V1) V2. Pick the lowest two such repeating pair of non-terminals. Now, we have these facts:

3 min read

Right- and Left-Linear CFGs: A right-linear CFG is one where every production rule has exactly one non-terminal and that it also appears rightmost. For example, the following grammar is right-linear: S -> 0 A | 1 B | e A -> 1 C | 0 B -> 0 C | 1 C -> 1 | 0 C. Recall that S -> 0 A | 1 B | e is actually three different production rules S -> 0 A, S -> 1 B, and S -> e, where each rule is right-linear. This grammar can easily be represented by the following NFA obtained almost directly from the grammar: IS - 0 -> A IS - 1 -> B IS - e -> F1 A - 1 -> C A - 0 -> F2 B - 0 -> C B - 1 -> F3 C - 0 -> C C - 1 -> F4. A left-linear grammar is defined similar to a right-linear one. An example is as follows: S -> A 0 | B 1 | e A -> C 1 | 0 B -> C 1 | 1 C -> 1 | C 0. A purely left-linear or a purely right-linear CFG denotes a regular language. However, the converse is not true; that is, if a language is regular, it does not mean that it has to be generated by a purely leftlinear or purely right-linear CFG. Even non-linear CFGs are perfectly capable of sometimes generating regular sets, as in S -> T T | e T -> 0 T | 0. It also must be borne in mind that we cannot “mix up” left- and rightlinear productions and expect to obtain a regular language. Consider the productions S -> 0 T | e T -> S 1. In this grammar, the productions are linear - left or right. However, since we use left- and right-linear rules, the net effect is as if we defined the grammar S -> 0 S 1 | e which generates the non-regular context-free language {0n1n | n ≥ 0}. Conversion of purely left-linear grammars to NFA: Converting a left-linear grammar to an NFA is less straightforward. We first reverse the language it represents by reversing the grammar. Grammar reversal is approached as follows: given a production rule S → R1R2 . . .Rn, we obtain a production rule for the reverse of the language represented by S by reversing the production rule to: Sr → R^r_nR^r_n−1 . . .R^r₁ . Applying this to the grammar at hand, we obtain Sr -> 0 Ar | 1 Br | e Ar -> 1 Cr | 0 Br -> 1 Cr | 1 Cr -> 1 | 0 Cr. Once an NFA for this right-linear grammar is built, it can be reversed to obtain the desired NFA.

2 min read

Simplifying CFGs: The productions of context-free grammars can be coerced into a variety of forms without affecting the expressive power of the grammar. (a) Empty Production Removal If the empty string does not belong to a language, then there is no way to eliminate production of the form A-> l from the grammar.

3 min read

Proof of Pumping Lemma (a) Suppose we have a CFL given by L. Then there is some context-free Grammar G that generates L. Suppose There are only a finite number of variables in a grammar and the productions for each variable have finite lengths. The only way that a grammar can generate arbitrarily long strings is if one or more variables is both useful and recursive.

3 min read

Error-correcting DFAs: Consider another experiment that shows the value of tool-assisted debugging of machines. In this experiment, a DFA has to be designed to recognize all strings that are a Hamming distance of 2 away from the set of strings denoted by the regular expression (0101) . For instance, 010101 and 010110 are a Hamming distance of 2 apart, as are 010111 and 000110. Definition: (Hamming Distance) Given two strings V1 and V2, of equal length and over {0, 1}∗, they are a Hamming distance of d apart if they differ in exactly d positions. The DFA we are to design can be regarded as an error-correcting DFA which corrects two-bit errors. We shall derive this DFA using two distinct approaches, each time by following two different lines of logic: We shall find the minimal DFAs corresponding to these constructions. If correctly performed, we must obtain isomorphic minimal DFAs, again serving to verify our construction methods. We discuss these constructions in the following sections. DFA constructed using error strata

3 min read

Ultimate Periodicity and DFAs: Ultimate periodicity is a property that captures a central property of regular sets (recall the definition of ultimate periodicity given in Definition 5.1, page 76). Theorem . If L is a regular language over an alphabet Σ, then the set Len = {length(w) | w ∈ L} is ultimately periodic. Note: The converse is not true. For example, the language {0ⁿ1ⁿ | n ≥ 0} has strings whose lengths are ultimately periodic, and yet this language is not regular. A good way to see that Theorem 10.3 is true is as follows. Given any DFA D over some alphabet Σ, consider the NFA N obtained from D by first replacing every transition labeled by a symbol in Σ \ {a} by a. In other words, we are applying a homomorphism that replaces every symbol of the DFA by a. Hence, the resulting machine is bound to be an NFA, and the lengths of strings in its language will be the same as those of the strings in the language of the original DFA (in other words, what we have described is a length-preserving homomorphism). Now, if we convert this NFA to a DFA, we will get a machine that starts out in a start state and proceeds for some number (≥ 0) of steps before it “coils” into itself. In other words, it attains a lasso shape. It cannot have any other shape than the ‘coil’ (why?). This coiled DFA shows that the length of strings in the language of any DFA is ultimately periodic with the period defined by the size of the coil. We now take an extended example to illustrate these ideas. Consider the DFA built over Σ = {a, b, c, d, f} using the following command pipeline: echo ’(ad)* ((abc)((acf)* (da)*)d)’ | retofm | fmdeterm | fmmin | grail2ps.perl - | gv -

3 min read

Usage of Pumping Lemma: The Pumping Lemma can be used to show that certain languages are not context free. Let us show that the language

1 min read

Developing CFGs Developing CFGs is much like programming; there are no hard-andfast rules. Here are reasonably general rules of the thumb for arriving at CFGs: 1. (Use common idioms): Study and remember many common patterns of CFGs and use what seems to fit in a given context. Example: To get the effect of matched brackets, the common idiom is S -> ( S ) | e. 2. Break the problem into simpler problems: Example: {ambn | m = n, m, n ≥ 0}. a) So, a’s and b’s must still come in order. b) Their numbers shouldn’t match up.

4 min read

The Power Relation between Machines: Fig. 4.2. The binary relation Power is shown. The dotted edges are some of the edges implied by transitivity. Undotted and dotted means the same in this diagram. Therefore, Power actually contains: (i) the pairs corresponding to the solid edges, (ii) the pairs indicated by the dotted edges, (iii) and those pairs indicated by those dotted transitive edges not shown. An example that nicely demonstrates the versatility of preorders is the one that defines the “power” of computing machines. Let MT = {dfa, nfa, dpda, npda, lba, dtm, ndtm} represent the set of machine types studied in this book. These acronyms stand for deterministic finite automata, nondeterministic finite automata, deterministic push-down automata, nondeterministic pushdown automata, linear bounded automata, deterministic Turing machines, and nondeterministic Turing machines, respectively. A binary relation called Power that situates various machine types into a dominance relation is shown in Figure 4.2. Each ordered pair in the relation shows up as an arrow (→). We draw an arrow from machine type m1 to m2 if for every task that a machine of type m1 can perform, we can find a machine of type m2 to do the same task. Spelled out as a set, the relation Power is

2 min read

Introduction: A ‘derivation tree’ is an ordered tree which the the nodes are labeled with the left sides of productions and in which the children of a node represent its corresponding right sides. Definition of a Derivation Tree: Let G = (V, T, S, P) be a CFG. An ordered tree is a derivation tree for G iff it has the following properties: Sentential Form: For a given CFG with productions S ® aA, A® aB, B® bB, B® a. The derivation tree is as shown below.

1 min read

Example 1: Give some example of context-free languages. Solution

3 min read

DEFINITIONS: Let us consider a finite automata which accepts the language We see that M moves from q0 to q1, on the occurence of a’s. On seeing ‘b’, M moves from q1 to q2 and continues to be in the state q2 on getting more b’s. Assume that the input string is given by

2 min read

Definition of CFG: A context-free grammar is a 4-tuple (V, T, S, P) where If u, v and w are strings of variables and terminals, and A-> w is a rule of the grammar, we say that uAv yields uwv, written uAv Þuwv. Example of CFG: Given a grammar G = ({S}, {a, b}, R, S). The set of rules R is

2 min read

PARSING: A grammar can be used in two ways: “Parsing” a string is finding a derivation (or a derivation tree) for that string. Parsing a string is like recognizing a string. The only realistic way to recognize a string of a context-free grammar is to parse it. Exhaustive Search Parsing: The basic idea of the “Exhaustive Search Parsing” is to parse a string w, generate all strings in L and check if w is among them. Problem arises when L is an infinite language. Therefore a systematic approach is needed to achieve this, as it is required to know that no strings are overlooked. And also it is necessary so as to stop after a finite number of steps. The idea of exhaustive search parsing for a string is to generate all strings of length no greater than | w |, and see if w is among them.

3 min read

DECISION ALGORITHMS THEOREM: Given L is a regular set, i.e., a language accepted by a finite automaton. There exists a constant ‘n’ such that if ‘s’ in any string in L and | s| ³ n, then s = uvw such that | uv| £ n, | v| ³1 and for all i ³ 0, uv iwÎL. Proof: Let us assume that L = T(M) where M = (Q, S,d, q , F ) 0 and ‘n’ be the number of states in Q.

2 min read

CFG to NPDA: For any context-free grammar in GNF, it is easy to build an equivalent nondeterministic pushdown automaton (NPDA). Any string of a context-free language has a leftmost derivation. We set up the NPDA so that the stack contents “corresponds” to this sentential form: every move of the NPDA represents one derivation step. The sentential form is

2 min read

NORMAL FORMS: Let us show how to find the formula given the Truth Table.

3 min read

NPDA to CFG (a) We have shown that for any CFG, an equivalent NPDA can be obtained. We shall show also that, for any NPDA, we can produce an equivalent CFG. This will establish the equivalence of CFGs and NFDAs. We shall assert without proof that any NPDA can be transformed into an equivalent NPDA which has the following form:

5 min read

Binary Relation Basics: A binary relation R on S is a subset of S × S. It is a relation that can be expressed by a 2-place predicate. Examples: (i) x loves y, (ii) x > y. Set S is the domain of the relation. Theoretically, it is possible that the domain S is empty (in which case R will be empty). In all instances that we consider, the domain S will be non-empty. However, it is quite possible that S is non-empty and R is empty. We now proceed to examine various types of binary relations. In all these definitions, we assume that the binary relation R in question is on S, i.e., a subset of S×S. For a relation R, two standard prefixes are employed: irr- and non-. Their usages will be clarified in the sequel. Relations can be depicted as graphs. Here are conventions attributed to Andrew Hodges in [63]. The domain is represented by a closed curve (e.g., circle, square, etc) and the individuals in the domain by dots labeled, perhaps, a, b, c, and so on. The fact that a, b ∈ R will be depicted by drawing a single arrow (or equivalently one-way arrow) from dot a to dot b. We represent the fact that both a, b ∈ R and b, a ∈ R by drawing a double arrow between a and b. We represent the fact that a, a ∈ R by drawing a double arrow from a back to itself (this is called a loop). We shall present examples of these drawings in the sequel. We shall use the following examples. Let S = {1, 2, 3}, R1 = {x, x | x ∈ S}, R2 = S × S, and R3 = {1, 1, 2, 2, 3, 3, 1, 2, 2, 1, 2, 3, 3, 2}. All these (and three more) relations are depicted in Figure 4.1. Reflexive, and Related Notions: R is reflexive, if for all x ∈ S, x, x ∈ R. Equivalently, In R’s graph, there is no dot without a loop. Informally, “every element is related to itself.” A relation R is irreflexive if there are no reflexive elements; i.e., for no x ∈ S is it the case that x, x ∈ R. Equivalently, In R’s graph, no dot has a loop.

1 min read

Example 2: Show that the grammar S ® S | S, S ® a is ambiguous. Solution: In order to show that G is ambiguous, we need to find a wÎL(G), which isambiguous. Assume w = abababa.

5 min read

Push-down Automata: A push-down automaton (PDA) is a structure (Q,Σ, Γ, δ, q0, z0, F) where Q is a finite set of states, Σ is the input alphabet, Γ is the stack alphabet (that usually includes the input alphabet Σ), q0 is the initial state, F ⊆ Q is the set of accepting states, z0 the initial stack symbol, and δ : Q × (Σ ∪ {ε}) × Γ → 2Q×Γ∗. In each move, a PDA can optionally read an input symbol. However, in each move, it must read the top of the stack (later, we will see that this assumption comes in handy when we have to convert a PDA to a CFG). Since we will always talk about an NPDA by default, the δ function returns a set of nondeterministic options. Each option is a next-state to go to, and a stack string to push on the stack, with the first symbol of the string appearing on top of the stack after the push is over. For example, if q1, ba ∈ δ(q0, x, a), the move can occur when x can be read from the input and the stack top is a. In this case, the PDA moves over x (it cannot read x again). Also, an a is removed from the stack. However, as a result of the move, an a is promptly pushed back on the stack, and is followed by a push of b, with the machine going to state q1. The transition function δ of a PDA may be either deterministic or nondeterministic. DPDA versus NPDA: A push-down automaton can be deterministic or nondeterministic. DPDA and NPDA are not equivalent in power; the latter are strictly more powerful than the former. Also, notice that unlike with a DFA, a deterministic PDA can move on ε. Therefore, the exact specification of what deterministic means becomes complicated. We summarize the definition from [60]. A PDA is deterministic if and only if the following conditions are met: In this book, I will refrain from giving a technically precise definition of DPDAs. It really becomes far more involved than we wish to emphasize in this chapter, at least. For instance, with a DPDA, it becomes necessary to know when the string ends, thus requiring a right end-marker .

4 min read

We now summarize the formal machines, as well as languages, studied in this book in the table given in Figure 13.5. This is known as the Chomsky hierarchy of formal languages. For each machine, we describe the nature of its languages, and indicate the nature of the grammar used to describe the languages. It is interesting that simply by varying the nature of production rules, we can obtain all members of the Chomsky hierarchy. This single table, in a sense, summarizes some of the main achievements of over 50 years of research in computability, machines, automata, and grammars. Here is a summary of the salient points made in this table, listed against each of the language classes:2 Regular languages: DFAs and NFAs serve as machines that recognize regular languages. Context-free grammars written with only left-linear or only right-linear productions can generate or recognize regular languages. The linearity of the production rules means that there is only one non-terminal allowed on the RHS of each production, which appears leftmost or rightmost. Hence, these non-terminals can be regarded as states of an NFA.

3 min read

Transition Functions for NPDA: The transition function for an NPDA has the form d : Q ´ (Σ ∪ {λ}) ´ Γ -> Finite sub sets of Q X Γ d is now a function of three arguments.

5 min read

Stabilization at a Fixed-Point: In every finite-state system modeled using a finite-state Boolean transition system, the least fixed-point is always reached in a finite number of steps. Let us try to argue this fact first using only a simple observation. The observation is that all the Boolean expressions generated during the course of fixed-point computation are over the same set of variables. Since there are exactly 2^2N Boolean functions over N Boolean variables (see Illustration 4.5.2), eventually two of the approximants in the fixed-point computation process will have to be the same Boolean function. However, this argument does not address whether it is possible to have “evasive” or “oscillatory” approximants Pi, Pi 1, . . . , Pj such that i = j and Pj = Pi. If this were possible, it would be possible to cycle through Pi, . . . , Pj without ever stabilizing on a fixed-point. Fortunately, this is not possible! Each approximant Pi 1 is more defined than the previous approximant Pi, in the sense defined by the implication lattice defined in Illustration 4.5.3. With this requirement, the number of these ascending approximants is finite, and one of these would be the least fixed-point. See Andersson’s paper [7] for additional examples of forward reachability. The book by Clarke et.al. [20] gives further theoretical insights. An example with multiple fixed-points: Consider the state transition system in Figure 11.6 with initial state s0 (called MultiFP). The set of its reachable states is simply {s0} (and is characterized by the formula a ∧ b), as there is no reachable node from s0. Now, a fixed-point iteration beginning with the initial approximant for the reachable states set to P0 = false will converge to the fixedpoint a ∧ b. What are the other fixed-points one can attain in this system? Here they are: Hence, in this example, there are three distinct fixed-points for the recursive formula defining reachable states. Of these, the least fixedpoint is a∧b, and truly characterizes the set of reachable states; a∨b is the intermediate fixed-point, and 1 is the greatest fixed-point. It is clear that (a ∧ b) ⇒ (a ∨ b) and (a ∨ b) ⇒ 1, which justifies these fixed-point orderings. Figure 11.6 also describes the BED commands to produce this intermediate fixed-point.

6 min read

Introduction: Recursion is a topic central to computer science. Lambda calculus offers us a very elegant (and fundamental) way to model and study recursion. In a book on computability and automata, such a study also serves another purpose; to concretely demonstrate that Lambda calculus provides a universal mechanism to model computations, similar to the role played by Turing machines. While this chapter can be skimmed, or even skipped, we have taken sufficient pains to make this chapter as “friendly” and intuitive as possible, permitting it to be covered without spending too much time. Covering this chapter will permit fixed-point theory to be used as a conceptual “glue” in covering much important material, including studying context-free grammars, state-space reachability methods, etc. Recursive Definitions: Let’s get back to the discussion of function ‘Fred’ introduced in Chapter 2, Section 2.6. Now consider a recursively defined function, also called ‘Fred.’ We fear that this will make it impossible to ‘de-Fred:’ function Fred x = if (x=0) then 0 else x Fred(x-1) It is quite tempting to arrive at the following de-Freded form: function(x) = if (x=0) then 0 else x self(x-1) However, it would really be nice if we can avoid using such ad hoc conventions, and stay within the confines of the Lambda notation as introduced earlier. We shall soon demonstrate how to achieve this; it is, however, instructive to examine one more recursive definition, now involving a function called Bob: function Bob(x) = Bob(x 1). One would take very little time to conclude that this recursive definition is “plain nonsense,” from the point of view of recursive programming. For example, a function call Bob(3) would never terminate. However, unless we can pin down exactly why the above definition is “nonsense,” we will have a very ad hoc and non-automatable method for detecting nonsensical recursive definitions - relying on human visual inspection alone. Certainly we do not expect humans to be poring over millions of lines of code manually detecting nonsensical recursion. Here, then, is how we will proceed to “de-Fred” recursive definitions (i.e., create irredundant names for them):

3 min read

= (λx.if (x = 0) then 0 else if (x = 1) then x 0 else x ⊥) = (λx.if (x = 0) then 0 else if (x = 1) then 1 else ⊥) which (calling it f2) is yet another function that defined for one more input value. In summary, substituting f0 for f, one gets f1, and substituting f1, one gets f2. Continuing this way, each fi turns into a function fi 1 that is defined for one more input value. While none of these functions satisfies the equation, in the limit of these functions is a total function that satisfies the equation, and hence is a fixed-point (compared with earlier examples, such as the cos function, which seemed to “stabilize” to a fixed-point in a few steps on a finite-precision calculator; in case of the fi series, we achieve the fixed-point only in the limit). This limit element happens to be the least fixed-point (in a sense precisely defined in the next section), and is written μx.(if (x = 0) then 0 else x f(x − 1)). Let this least fixed-point function be called h. It is easy to see that h is the following function: h(n) = Σn i=0 i. It is reassuring to see that the least fixed-point is indeed the function that computes the same “answers” as function Fred would compute if compiled and run on a machine. It turns out that in recursive programming, the “desired solution” is always the least fixed-point, while in other contexts (e.g., in reachability analysis of finite-state machines demonstrated in Chapter 9), that need not be true. The ‘solution’ point of view for recursion also explains recursive definitions of the form function Bob(x) = Bob(x 1). The only solution for function Bob is the everywhere undefined function λx. ⊥. To see this more vividly, one can try to de-Bob the recursion to get Bob = Y (lambda y . lambda x . y(x 1)). Suppose H = (lambda y . lambda x . y(x 1)). Now, supplying a value such as 5 to Bob, and continuing as with function Fred, one obtains the following reduction sequence: Bob 5 = (Y H) 5 = H (Y H) 5 = (lambda y . lambda x . y(x 1)) (Y H) 5 = (lambda x . (Y H)(x 1)) 5 = (Y H)(5 1) = (Y H) 6 = ... = (Y H) 7 = ... = (non-convergent). In other words, Bob turns out to be the totally undefined function, or “bottom function.”

4 min read

The least fixed-point: In the above example, we obtained a fixed-point h which we asserted to be the “least” in a sense that will now be made clear. In general, given a recursive program, if there are multiple fixed-points, The desired meaning of recursive programs corresponds to the least fixed-point, and The fixed-point finding combinator Y is guaranteed to compute the least fixed-point [114]. To better understand these assertions, consider the following four definitions of functions of type Z × Z → Z, where Z is the integers (this example comes from [78]): f1 = λ(x, y) . if x = y then y 1 else x 1 f2 = λ(x, y) . if x ≥ y then x 1 else y − 1 f3 = λ(x, y) . if x ≥ y and x− y is even then x 1 else ⊥ Now consider the recursive definition: F(x, y) = if x = y then y 1 else F(x, F(x − 1, y 1)). We can substitute f1, f2, or f3 in place of F and get a true equation! Exercise 6.8 asks you to demonstrate this. However, of these functions, f3 is the least defined function in the sense that whenever f3(x) is defined, fi(x) is defined for i = 1, 2, but not vice versa, and there is no other function (say f4) that is less defined than f3 and also serves as a solution to F. To visualize concepts such as “less defined,” imagine as if we were plotting the graphs of these functions. Now, when a function is undefined for an x value, we introduce a “gap” in the graph. In this sense, the graph of the least fixed-point function is the “gappiest” of all; it is a solution, and is the most undefined of all solutions – it has the most number of “gaps.” These notions can be captured precisely in terms of least upper-bounds of pointed complete partial orders [107]. In our example, it can be shown that f3 is the least fixed-point for the recursion. Fixed-points in Automata Theory: We will have many occasions to appeal to the least fixed-point idea in this book. Here are some examples: It is also worth noting that while least fixed-points are most often of interest, in many domains such as temporal logic, the greatest fixedpoints are also of interest. The functional (higher order function) H from Section 6.1.1, namely H = (λy.λx.if (x = 0) then 0 else x y(x − 1)) has an interesting property: it works as a “bottom refiner!” In other words, when fed the “everywhere undefined function” f0 (called the “bottom function”), it returns the next better approximation of the least fixed-point h in the form of f1. When fed f1, it returns the next better approximation f2, and so on. It may sound strange that the meaning of recursive programs is determined starting from the most uninteresting of functions, namely the ‘bottom’ or ⊥ function. However, this is the most natural approach to be taking, because

4 min read

Introduction: : Throughout the entire 150 years (or so) history of computer science, one can see an attempt on part of researchers to understand reasoning as well as computation in a unified setting. This direction of thinking is best captured by Hilbert in one of his famous speeches made in the early 1900s in which he challenged the mathematical community with 23 open problems. Many of these problems are still open, and some were solved only decades after Hilbert’s speech. One of the conjectures of Hilbert was that the entire body of mathematics could perhaps be “formalized.” What this meant is basically that mathematicians had no more creative work to carry out; if they wanted to discover a new result in mathematics, all they had to do was to program a computer to systematically crank out all possible proofs, and check to see whether the theorem whose proof they are interested in appears in one of these proofs! In 1931, Kurt G¨odel dropped his ‘bomb-shell.3 He formally stated and proved the result, “Such a device as Hilbert proposed is impossible!” By this time, Turing, Church, and others demonstrated the true limits of computing through concrete computational devices such as Turing machines and the Lambda calculus. The rest “is history!” The Automaton/Logic Connection: Scientists now have a firm understanding of how computation and logic are inexorably linked together. The work in the mid 1960s, notably that of J.R. B¨uchi, furthered these connections by relating branches of mathematics known as Presburger arithmetic and branches of logic known as WS1S4 with deterministic finite automata. Work in the late 1970s, notably by Pnueli, resulted in the adoption of temporal logic as a formal logic to reason about concurrency. Temporal logic was popularized by Manna and Pnueli through several textbooks and papers. Work in the 1980s, notably by Emerson, Clarke, Kurshan, Sistla, Sifakis, Vardi, and Wolper established deep connections between temporal logic and automata on infinite words (in particular B¨uchi automata). Work in the late 1980s, notably by Bryant, brought back yet another thread of connection between logic and automata by the proposal of using binary decision diagrams, essentially minimized deterministic finite automata for the finite language of satisfying instances of a Boolean formula, as a data structure for Boolean functions. The symbolic model checking algorithm proposed by McMillan in the late 1980s hastened the adoption of BDDs in verification, thus providing means to tackle the correctness problem in computer science. Also, spanning several decades, several scientists, including McCarthy, Wos, Constable, Boyer, Moore, Gordon, and Rushby, led efforts on the development of mechanical theorem-proving tools that provide another means to tackle the correctness problem in computer science.

1 min read

BED Commands for SimpleTR:: The BED commands given in Figure 11.5 compute the reachable set of states using forward reachability in our example. We can see that P2, the least fixed-point, is indeed true — namely, the characteristic predicate for the set of all states. (Note: In BED, the primed variables must be declared immediately after the unprimed counterparts). In addition to the explicit commands to calculate the least fixed-point, BED also provides a single command called reach. Using that, one can calculate the least fixed-point in one step. In our present example, RS and P2 end up denoting the BDD for true. let RS = reach(I,T) upall RS view RS Section 11.3.4 discusses another example where the details of the fixedpoint iteration using BED are discussed.

2 min read

has (000000 010010 001001 100100 011011 101101 110110 111111). When converted to minimized DFAs, these regular expressions yield Figures 11.2(a) and (b), where the size difference due to the variable orderings is very apparent. The BDD for Figure 11.2(b) created using the BED tool appears in Figure 11.3. The commands used to create this BDD were: bed> var a c e b d f % declares six variables bed> let exp4 = (a=b) and (c=d) and (e=f) % defines the desired expn. bed> upall exp4 % builds the BDD - bed> view exp4 % displays the BDD By comparing Figure 11.3 against Figure 11.2(b), one can see how, in general, BDDs eliminate redundant decodings. BDDs are efficient data structures for representing Boolean functions and computing the reachable states of state transition systems. In these applications, they are very often ‘robust,’ i.e., their sizes remain modest as the computation advances. As many of these state transition systems have well over 2150 states (just to pick a large number!), this task cannot be accomplished in practice by explicitly enumerating the states. However, BDDs can often very easily represent such large state-spaces by capitalizing on an implicit representation of states as described in Section 11.3. However, BDDs can deliver this ‘magic’ only if a “good” variable ordering is chosen.

1 min read

Logical Identities: If two propositional forms are logically equivalent one can be substituted for the other in any proposition in which they occur. Table below shows a list of important equivalences, which are called “identities.” The symbols P, Q , and R represent arbitrary propositional forms. The symbol “1” is used to represent either a “tautology” or a true proposition. Similarly, “0” represents a false proposition or a contradiction. All the above identities can be proved by constructing truth tables. The following table gives a list of tautologies which are implications.

3 min read

CONTEXT SENSITIVE GRAMMARS AND LANGUAGES: A context-sensitive Language is a language generated by a context sensitive grammar. Definition 1: A context-sensitive grammar is one whose productions are all of the form xAy-> xvy

2 min read

BOOLEAN SATISFIABILITY: Assume we have n Boolean variables, viz., A, B, C, .... and an expression in the propositional Calculus i.e., we can use and, or and not to form the expression. Is there an assignment of truth values to the variables, (for example, A = true, B = true, C = false), that will make the expression true? Here is a nondeterministic algorithm to solve the problem: For each Boolean variable, assign if the proper truth value. This is a linear algorithm. We can find a deterministic algorithm for this problem in much the same way as we did for the integer bin problem. Effectively, the idea is to set up a systematic procedure to try every possible assignment of truth values to variables. The algorithm terminates when a satisfactory solution is found, or when all 2n possible assignments have been tried. Again, the deterministic solution requires exponential time.

2 min read

QUANTIFIERS AND LOGICAL OPERATORS: The transcription of mathematical statements involves predicates, quantifiers and logical operators. Assume that “Universe of discourse” is I and let (i) Every integer is even or odd. (ii) The only even prime is two

2 min read

ADDITIONAL NP PROBLEMS: The following problems have a polynomial-time solution, but an exponential-time solution on a deterministic machine. There are literally hundreds of additional examples. NP-COMPLETE PROBLEMS: All the known NP problems have a remarkable characteristic: They are all reducible to one another. What this means is that, given any two NP problems X and Y, (a) There exists a polynomial-time algorith to restate a problem of type X as a problem of type Y, and

1 min read

Example 1: State the converse and contrapositive of the following statements: (a) If it rains, I am not going. (b) I will stay only if you go.

3 min read

PROPOSITIONS: Mathematics is the study of the properties of mathematical structures. A mathematical structure is defined by a set of “axioms”. An “axiom” is a true statement about the properties of the structure. “Logic” is the discipline that deals with the methods of reasoning. It gives a set of rules and techniques to determine whether a given argument is valid or not. True assertions which can be inferred from the truth of axioms are called “theorems”. A “proof” of a theorem is an argument that establishes that the theorem is true for a specified mathematical structure. A “proposition” or “statement” is any declarative sentence which is true (T) or false (F). We refer to T or F as the truth value of the statement.

2 min read

NORMAL FORMS: Let us show how to find the formula given the Truth Table.

2 min read

COMPOSITION AND RECURSION: If g1, g2, g3 and h are previously defined functions, these functions can be combined to form new functions. These functions can be combined only in precisely defined ways. (a) Composition: f (x, y) = h(g (x, y), g (x, y)) 1 2 . This allows us to use functions as arguments to functions. (b) Primitive Recursion: This is a structured “recursive routine” with the form:

4 min read

FORMAL SYSTEMS: The necessary properties of a satisfactory formal system are as follows: (a) Completeness: It should be possible either to prove or disprove any proposition that can be expressed in the system. (b) Consistency: It should not be possible to both prove and disprove a proposition in the system.

4 min read

Predicates : A predicate is a statement containing one or more variables. Proposition : If values are assigned to all the variables in a predicate, the resulting statement is a proposition. e.g. 1. x < 9 is a predicate 2. 4 < 9 is a proposition Propositional Function : Let a be a given set. A propositional function (or : on open sentence or condition) defined on A is an expression P(x) which has the property that P(a) is true or false for each a ∈ A. The set A is called domain of P(x) and the set Tp of all elements of A for which P (a) is true is called the truth set of P(x). i.e. Another use of predicates is in programming Two common constructions are “if P(x), then execute certain steps” and “while Q(x), do specified actions.” The predicates P(x) and Q(x) are called the guards for the block of programming code often the guard for a block is a conjunction or disjunction. e.g. Let A = {x / x is an integer < 8} Here P(x) is the sentence “x is an integer less than 8”. The common property is “an integer less than 8”. P(1) is the statement “1 is an integer less than 8”. P(1) is true, 1 ∈ A etc

3 min read

Connectives: In order to make use of some keywords like and, ‘or’, ‘not’, etc. which are called “sentential connectives”, it is required to have some ground rules before making use of them. Let us now discuss about the different forms of connectives. (a) Negation (NOT):The negation of p is the statement ~p, which is read as “not P”. Its truth value is defined by the following truth table.

1 min read

THE CHOMSKY HIERARCHY: The Chomsky Hierarchy, as originally defined by Noam Chomsky, comprises four types of languages and their associated grammars and machines. EXTENDING THE CHOMSKY HIERARCHY: So far we have discussed about other types of languages besides those in the “classical Chomsky hierarchy. For example, we noted that deterministic pushdown automaton were less powerful than nondeterministic pushdown automata. The table below shows a table of some of the language classes we have covered that fit readily into the hierarchy.

4 min read

POLYNOMIAL-TIME ALGORITHMS: A polynomial-time algorithm is an algorithm whose execution time is either given by a polynomial on the size of the input, or can be bounded by such a polynomial. Problems which can be solved by a polynomial-time algorithm are called “tractable” problems. As an example, most algorithms on arrays can use the array size, n, as the input size. In order to find the largest element in any array requires a single pass through the array, so the algorithm which does this is of O(n), or it is a “linear time” algorithm. Sorting algorithms take O(n log n) or O(n2) time. Bubble sort takes linear time in the least case, but O(n2) time in the average and worst cases. Heapsort takes O(n log n) time in all cases. Quicksort takes O(n log n) time on average, but O(n2) time in the worst case. As far as O(n log n) is concerned, it must be noted that the base of the logarithms is irrelevant, as the difference is a constant factor, which is ignored. All programming tasks we know have polynomial solutions. It is not due to the reason that all practical problems have polynomial-time solutions.

2 min read

UNRESTRICTED GRAMMAR: The grammars in the Chomsky hierarchy allows productions of the form a->b where a and b are arbitrary strings of grammar symbols, with a ≠ λ.

2 min read

Introduction to Complexity Theory: There are two kinds of measures with Complexity Theory: (a) time and (b) space.

1 min read

Tautology, Contradiction and Contingency (a) Tautology: A Tautology is a propositional form whose truth value is true for all possible values of its propositional variables. Example: pÚ ¬ p.

1 min read

ACKERMANN’S FUNCTION: Ackermann’s function is an example of a function that is mu-recursive but not primitive recursive. Mu-recursive functions are said to have the power of a Turing machine. It is defined as follows: A(x, y) can be computed for every (x, y). Hence A (x,y) is a total function. But Ackermann’s function is not primitive recursive but recursive.

5 min read

Encoding conventions: We now define the encoding conventions for natural numbers employed in our automaton construction. We define natural numbers in base 2 using a bit-serial format, with the least significant bit (LSB) appearing leftmost. This means that when viewed as inputs of DFA, numbers will be consumed LSB-first. For example, 13 is written as 1011 (or as 10110, or in general, with as many zeros to the right). Pairs of natural numbers are represented as a sequence of tuples, and in general k-tuples of natural numbers are represented as a sequence of k-tuples. k-tuples of zeros may be added to the right without changing the meaning of these representations. For example, 13, 6 is represented as 1, 00, 11, 11, 0. Example 1 — representing x ≤ 2

3 min read

Conversion algorithm: Presburger formulas to automata: Let us review the conversion algorithm presented thus far, again keeping the example (x y) = 1 in mind, referring to Figure 20.3. The machines we build employ bit-serial conventions, meaning: (i) they begin in a start state where initially it has not seen any inputs (by convention, we assume that x = y = 0). If the formula is satisfied for these Starting DFA for ∃y.(x y) = 1:

3 min read

Halting Problem: The input to a Turing machine is a string. Turing machines themselves can be written as strings. Since these strings can be used as input to other Turing machines. A “Universal Turing machine” is one whose input consists of a description M of some arbitrary Turing machine, and some input w to which machine M is to be applied, we write this combined input as M w. This produces the same output that would be produced by M. This is written as Universal Turing Machine (M w) = M (w).

2 min read

Post’s correspondence problem (PCP): At first glance, a PCP instance is a simple puzzle about finite sequences3 of pairs of strings of the form 01, 101, ε01, 01, 101. It is customary to think of the above as “tiles” (or “dominoes”), with each tile at the respective index portrayed thus: The question is: is there an arrangement of one or more of the above tiles, with repetitions allowed, so that the top and bottom rows read the same? Here is such an arrangement: In obtaining this solution, the tiles were picked, with repetition, according to the sequence given by the indices 3,2,0,3,1: Given a PCP instance S of length N (N = 4 in our example), a solution is a sequence of numbers i1, i2, . . . , ik where k ≥ 1 and each ij ∈ {0 . . .N − 1} for j ∈ {1 . . . k} such that S[i1]S[i2] . . .S[ik] has the property of the top and bottom rows reading the same. By the term “solution” we will mean either the above sequence of integers or a sequential arrangement of the corresponding tiles. Note that 3,2,0 is another solution, as is 3,1. The solution 3,1 is:

5 min read

Introduction: Reactive computing systems are hardware/software ensembles that maintain an ongoing interaction with their environment, coordinating as well as facilitating these interactions. They are widely used in all walks of life—often in areas that directly affect life. Examples of reactive systems include device drivers that control the operation of computer peripherals such as disks and network cards, embedded control systems used in spacecraft or automobiles, cache coherency controllers that maintain memory consistency in multiprocessor machines, and even certain cardiac pacemakers that measure body functions (such as body electric fields and exercise/sleep patterns) to keep a defective heart beating properly. Model checking has already been employed in most of these areas, with its use imminent in critical areas such as medical systems. Clearly, knowing a little bit about the inner workings of a model checker can go a long way towards their proper usage. Why model checking? The design of most reactive systems is an involved as well as exacting task. Hundreds of engineers are involved in planning, analyzing, as well as building and testing the various hardware and software components that go into these systems. Despite all this exacting work, at least two vexing problems remain: Formal methods based on model checking are geared towards eliminating the above difficulties associated with late cycle debugging. While model checking is not a panacea, it has established a track record of finding many deep bugs missed by weeks or months of testing. Specifically,

2 min read

Examples of interpretations: Manna’s book provides many insightful examples, some of which are summarized below. We focus on the notion of interpretations, which, in case of first-order logic: (i) chooses domains for constants, predicates, and function symbols to range over, and (ii) assigns to them. Examples below will clarify. Example 1: Consider the formula Fmla1 = ∃F.F(a) = b ∧(∀x).[p(x) ⇒ F(x) = g(x, F(f(x)))] We will now provide three distinct interpretations for it. Interpretation 1. D = Nat a = 0 b = 1 f = λx.(x = 0 → 0, x − 1) g = * p = λx.x > 0 Interpretation 2. D = Σ∗ a = ε b = ε f = λx.(tail(x)) g(x,y) = concat(y,head(x)) p = λx.x = ε Interpretation 3. D = Nat a = 0 b = 1 f = λx.x g(x,y) = y 1 p = λx.x > 0 It is clear that under Interpretation 1, Fmla1 is true, because there indeed exists a function F, namely the factorial function, that makes the assertion true. It is also true under Interpretation 2, while it is false under Interpretation 3 (Exercise 18.4 asks for proofs). Hence, this formula is not valid — because it is not true under all interpretations. Example 2: Consider the formula

3 min read

B¨uchi automata, and Verifying Safety and Liveness: B¨uchi automata are automata whose languages contain only infinite strings. The ability to model infinite strings is important because of the fact that all bugs can be described in the context of infinite executions. We now elaborate on these potentially unusual sounding, but rather simple, ideas. Broadly speaking, all errors (bugs) in reactive systems can be classified into two classes: safety (property) violations and liveness (property) violations. − two people who, following a faulty protocol, walk opposite in a narrow dark corridor and collide; − an elevator which, when requested to go to the 13th floor, proceeds to do so with its doors wide open; − a process P which acquires a lock L and dies, thus permanently blocking another process, say Q, from acquiring L. All finite executions of the form s1 . . . sk can be modeled as infinite executions that infinitely repeat the last state, namely s1s2 . . . (sk)ω. Modeling finite executions as infinite executions allows one to employ B¨uchi automata.

3 min read

First-order Logic (FOL) and Validity: Below, we will introduce many notions of first-order logic intuitively, through examples. We refer the reader to one of many excellent books in first-order logic for details. One step called skolemization merits some explanation. Basically, skolemization finds a witness to model the existential variable. In general, from a formula of the form ∃X.P(X), we can infer P(c) where c is a constant in the domain. Likewise, from P(c), we can infer ∃X.P(X); in other words, for an unspecified constant c in the domain, ∃X.P(X) ⇔ P(c). We will use this equivalence in the following proofs. There is another use of skolemization illustrated by the following theorem (which we won’t have occasion to use): ∀X.∃Y.P(X, Y ) ⇔ P(X, f(X)). Here, f is an unspecified (but fixed) function. This equivalence is valid because of two reasons: A warm-up exercise: Suppose we are given the following proof challenge: Some patients like every doctor. No patient likes a quack. Therefore, prove that no doctor is a quack. It is best to approach problems such as this using predicates to model the various classes of individuals2 instead of employing ‘arbitrary constants’ such as p and d to denote patients, doctors, etc. Introduce predicate p to carve out a subset of people (P) to be patients, and similarly d for doctors. Let l (for “likes”) be a binary relation over P. Our proof will consist of instantiation of formulas, followed by Modus ponens, and finally proof by contradiction. A1: The statement, “Some patients like every doctor:” ∃x ∈ P : (p(x) ∧ ∀y : (d(y) ⇒ l(x, y))). A2: The statement, “No patient likes a quack:” ∀x, y ∈ P : (p(x) ∧ q(y)⇒ ¬l(x, y)). Proof goal: “No doctor is a quack.” ∀x ∈ P : (d(x) ⇒¬q(x)). Negate the proof goal: ∃x ∈ P : (d(x) ∧ q(x)). Skolemize negated proof goal: (x0 ∈ P ∧ d(x0) ∧ q(x0). Skolemize A1: c ∈ P ∧ (p(c) ∧ ∀y : (d(y) ⇒ l(c, y))) (we will suppress domain membership assertions such as c ∈ P from now on). Specialize: From A1, we specialize y to x0 to get: p(c) ∧ (d(x0) ⇒ l(c, x0)). But since d(x0) is true in the negated proof goal, we get: p(c) ∧ l(c, x0) (more irrelevant facts suppressed). Since q(x0) is true in the negated proof goal, we also get: p(c) ∧ l(c, x0) ∧ q(x0). Use A2 and specialize x to c and y to x0 to get ¬l(c, x0). Contradiction: Since we have l(c, x0) and ¬l(c, x0), we get a contradiction.

4 min read

Greibach’s Theorem: There is a theorem analogous to Rice’s Theorem for PDAs. Known as Greibach’s Theorem, the high-level statement of the theorem (in terms of its practical usage) is as follows: It is impossible to algorithmically classify (using, of course, a Turing machine) context-free grammars on the basis of whether their languages are regular or not. The Computation History Method: As we mentioned , it is possible to “teach” LBAs (and NPDAs) to answer certain difficult questions about Turing machines. This idea is detailed in Section 17.3.2 through 17.3.4. We first recap basic facts about linear bounded automata (LBA) and present a decidability result about them (Section 17.3.1). Thereafter, we present three undecidability results based on the computation history method: (i) emptiness of LBA languages (Section 17.3.2), (ii) universality of the language of a CFG (Section 17.3.3), and (iii) Post’s correspondence problem (Section 17.3.4). In Chapter 18, Section 18.2.3, we emphasize the importance of the undecidability of Post’s correspondence problem (PCP) by presenting a classic proof due to Robert Floyd: we reduce PCP to the validity problem for first-order logic. This proof then establishes that the validity problem for first-order logic is undecidable. Decidability of LBA acceptance: LBAs are Turing machines that are allowed to access (read or write) only that region of the input tape where the input was originally presented. To enforce such a restriction, one may place two distinguished symbols, say and , around the original input string.1 With these conventions, it can easily be seen that instantaneous descriptions of an LBA that begin as q0w will change to the general form lqr, where |lr| = |w|. Therefore, there are a finite number, say N, of these IDs (see Exercise 17.1). A decider can simulate an LBA starting from ID q0w, and see if it accepts within this many IDs; if not, the LBA will not accept its input. Hence, LBA acceptance is decidable.

3 min read

Axiomatization of Propositional Logic: We now present one axiomatization of propositional calculus following the Hilbert style. Let the syntax of well-formed formulas (wff) be as follows: In other words, a formula is a propositional variable, the negation of a propositional formula, an implication formula, or a parenthesized for mula. This grammar defines a complete set of formulas in the sense that all Boolean propositions can be expressed in it (prove this assertion). Following Church, a Hilbert calculus for propositional logic can be set up based on three axioms (A1-A3) and two rules of inference (R1-R2) shown below. Here, p and q stand for propositional formulas.

2 min read

Presburger formulas: The basic terms in Presburger arithmetic consist of first-order variables x, y, x1, x , . . ., the constants 0, and 1, and sums of basic terms. For instance, x x 1 1 1 is a basic term, which we also write as 2x 3. The atomic formulas are equalities and inequalities between basic terms. For instance, x 2y = 3z 1 is an atomic formula. The formulas of Presburger logic are first-order formulas built on the atomic formulas. For instance, ∀x.∃y.(x = 2y ∨ x = 2y 1) is a formula. The free variables of formula ϕ are defined as usual: for instance, FV (ϕ1 ∨ ϕ2) = FV (ϕ1) ∪ FV (ϕ2), and FV (∃x.ϕ) = FV (ϕ) \ {x}. A formula without free variables is called a sentence. Sentences are true (valid) or false (non-valid). Any first-order formula with nested quantifiers, for example ∀x.(p(x) ⇒ [∃y.q(x, y)]) may be rewritten as a logically equivalent formula, in this example as ∀x.∃y.[p(x) ⇒ q(x, y)] using a transformation process called prenexing or arriving at the prenex normal form. As another example, the prenex normal form for the formula ∀x.([∃y.q(x, y)] ⇒ p(x))

3 min read

Temporal Logics Kripke structures: Kripke structures are finite-state machines used to model concurrent systems. A Kripke structure is a four-tuple S, s0,R, L where S is a finite set of states, s0 is an initial state, R ⊆ S × S is a total relation known as the reachability relation, and L : S → 2P is a labeling function, with P being a set of atomic propositions. It is standard practice to require that R be total, as Kripke structure are used to model infinite computations (in modeling finite computations, terminal states are equipped with transitions to themselves, thus in effect making R total). The fact that we choose one initial state is a matter of convenience. Figure 22.1 (bottom) presents two Kripke structures. In the Kripke structure on the left, S = {s0, s1, s2}, s0 = s0, R is shown by the directed edges, and L by the subsets of {a, b} that label the states. In its behavior over time, this Kripke structure asserts a and b true in the first time step, b true in the second time step, and a in the third time step. In the fourth time step, it may assert either a or b. One of these sequences is shown in the middle – namely, choosing to assert a in the fourth time step, and b in the fifth. When a label is omitted (e.g., there is no b in state s2), we are effectively asserting ¬b. Therefore, the assertion in state s3 is ¬a∧¬b. The corresponding “waveforms2” (as if viewed on an oscilloscope) are shown at the top of this figure. From these discussions it is clear that we model the behavior of systems in terms of the truth values of a set of Boolean variables. This is the most common approach taken when modeling systems as finitestate machines.We therefore let P be the set of these Boolean variables. There are of course other ways to model systems. For instance, if one were to employ a set of Boolean variables B and a set of integer variables I to model a system, P would consist of B as well as propositions over integers, such as i > 2 or i = j 1. In any case, knowing the truth of the atomic propositions P, it is possible to calculate the truth of any Boolean proposition built over P. Each state s ∈ S is an equivalence class of time points, while R models how time advances. Whenever the system is at a state s ∈ S, a fixed set of Boolean propositions determined by L are true. Since S is finite, we can immediately see that the temporal behavior of systems modeled using Kripke structures recur over time, thus basically generating a regular language of truth values of the propositions in P. For example, Figure 22.1 shows how the truth of the Boolean proposition a ∨ b varies with time. Since either a or b is always true, a ∨ b is always true for the Kripke structure on the left; that is not the case for the Kripke structure on the right, as we can enter state s3 where both a and b are false.

4 min read

In Automaton/Logic Connection, Symbolic Techniques, we took our first step towards presenting another perspective of computation, namely one based on mathematical logic. Specifically, in Automaton/Logic Connection, Symbolic Techniques, we demonstrated that We connected these ideas to the real world by demonstrating how to encode the familiar game of tic-tac-toe using BDDs, as well as computing all possible draw configurations in one fell swoop. In Basic Notions in Logic including SAT, we examined the power of machines to decide the validity of first-order logic sentences, and proved that Turing machines cannot be programmed to algorithmically carry out this decision. In Complexity Theory and NP-Completeness, we showed that Turing machines can decide Boolean logic, but the apparent complexity is exponential (the NPC class). DFA for Presburger Arithmetic through Model Checking: Algorithms will again pursue the automaton/logic connection, but in the context of verifying reactive systems. This section illustrates another instance of automaton-logic connection. In contrast to the undecidability of full first-order logic, there is a fragment of first-order logic called Presburger arithmetic that is decidable. A widely used decision procedure for Presburger arithmetic consists of building a DFA for the satisfying instances of Presburger formulas. In this connection, an interesting contrast with Automaton/Logic Connection is the following. BDDs are essentially DFA whose languages are a finite set of finite strings,1 with each string specifying assignments to the Boolean variables of the BDD. In contrast, the languages of the Presburger DFA built in this chapter are finite or infinite sets of finite but unbounded strings. Each string encodes the assignments to the quantified individual variables of a Presburger formula. In this chapter we present the following results: − The DFA for the conjunction of two Presburger formulas f1 and f2 may be obtained by first obtaining the DFA d1 and d2 for the individual formulas and then performing a DFA product construction for intersection. Similar results are obtained for disjunction and negation. − Existential quantification can be modeled by hiding the quantified symbol from the interface of the corresponding automaton. The result may be an NFA that can then be determinized.

2 min read

LTL vs. CTL through an example: The differences between LTL and CTL are actually quite subtle. Consider Figure 22.4, and the CTL formula AG (EFx). In order for this formula to be true over this Kripke structure, in all paths starting from s0, everywhere along those paths, EFx must be true. This, in turn, means that there must exist a path where x is eventually found. Starting either from s0 or s1, we see that there exists a path on which x is found true eventually. Hence, AG (EFx) is true of this Kripke structure. Let us try to pretend that the CTL formula AG (EF x) is equivalent to the LTL formula G (F x). An LTL formula is true of a Kripke structure if and only if it is true of every infinite path in the Kripke structure considered separately! Now consider the infinite path of spinning in state s0. For this infinite path, ¬x is permanently true. Therefore, we will violate Fx, and hence G (Fx). In short, this one path serves as the “death knell” for G (F x) with respect to this Kripke structure—whatever other paths might exist in this Kripke structure.

1 min read

DIMACS file encoding: At this point, having generated the gate net-list and their clauses, we now need to generate a file format representing the conjunction of these clauses. The standard format employed is the so called DIMACS format, where the literals in each clause are listed on separate lines, terminated by 0. Given such a DIMACS file, one can feed the file to a Boolean satisfiability solver. The result of feeding the above file to zchaff is shown below:

3 min read

Model (proctype) and property (never) automata: A typical Promela model consists of multiple proctypes and one never automaton. The proctypes are concurrent processes whose atomic statements interleave in all possible ways. The collection of proctypes represents the “system” or “model.” Formally, one can say that the asynchronous or interleaving product of the model automata represents the set of all behaviors of interest. A never or property automaton observes the infinite runs of this interleaving product (all model runs). Conceptually, after every move of the model (a move of one of the constituent proctypes), one move of the property automaton is performed to check whether the model automaton move left the system in a good state. Formally, one can say that the synchronous product of the model and property automata are performed. In Figure 21.2, the property automaton represents the complement5 of the desired property—hence, the keyword never. One of the desired properties in our example is that progress is infinitely often set true. This means that infinitely often, every philosopher gets to eat. If there is even one philosopher who, after a finite amount of eatings, is never allowed to eat again, we certainly would like to know that. The never automaton accepts a run (or a computation) if the run visits one of the final states infinitely. The never automaton defined in Figure 21.2 can nondeterministically loop in its initial do/od loop. In fact, it can even stay in its initial state if progress is false. However, it may also choose to go to the final state labeled accept when progress is false. Here, it can continue to visit accept so long as progress is false. Hence, this never automaton accepts only an infinite sequence of progress being false—precisely when our desired liveness property is violated. When we ran the description in Figure 21.2 through the SPIN model checker (which is a model checker for descriptions written in Promela), it quickly found a liveness violation which indicates that, indeed, there exists at least one philosopher who will starve forever. SPIN produces a message sequence chart (MSC) corresponding to this error; this is shown in Figure 21.3. An MSC displays the “lifelines” (time lines of behaviors) of all the processes participating in the protocol. Ignoring the never and init lifelines that are at the left extremity, the main lifelines shown are vertical lines tracing the behaviors of various process instances, specifically phi1:1, fork:2, phi1:3, fork:4, phi1:5, and fork:6. Reading this MSC, we find out how the bug occurs:

3 min read

Properties of Boolean Formulas Boolean satisfiability: an overview: Research on Boolean satisfiability methods (SAT) is one of the “hottest” areas in formal methods, owing to the fact that BDDs are often known to become exponentially sized. The idea of model checking without BDDs was introduced. This work also coincided with the arrival on the scene, of efficient Boolean satisfiability methods. These modern SAT solvers utilization in carrying out these algorithms. Easily modifiable versions of these tools are now freely available. Boolean SAT methods are now able to often handle extremely large system models, establish correctness properties, and provide explanations when the properties fail. Andersson presents many of the basic complexity results, including the inevitability of exponential blow up, even in the domain of SAT. We discuss a summary of these issues, and offer a glimpse at the underlying ideas behind modern SAT tools. Unfortunately, space does not permit our detailed presentation of the use of SAT techniques or some of their unusual applications in system verification. The reader may find many tutorials on the Internet or web sites. Normal forms We now discuss several properties of Boolean (or propositional) formulas to set the stage for discussions about the theory of NP-completeness. There are two commonly used normal forms for Boolean formulas: the conjunctive normal form (CNF) and the disjunctive normal form (DNF). Given a Boolean expression (function) over n variables x1 . . .xn, a sum-of-products (SOP) or disjunctive normal form (DNF) expression for it is one where products of literals are disjoined (OR-ed) – a literal being a variable or its negation. For example, nand(x, y) is expressed in SOP (DNF) as

3 min read

Acceptance, Halting, Rejection: Given a Turing machine M = (Q,Σ, Γ, δ, q0,B, F), the transition function δ is partial - it need not be defined for all inputs and states. When not defined, the machine becomes “stuck” - and is said to halt. Therefore, note that a TM can halt in any state. Also, by convention, no moves are defined out of the control states within F. Therefore, a TM always halts when it reaches a state f ∈ F. Here are further definitions: A TM accepts when halting at f ∈ F. A TM rejects when halting in any other state outside F. A TM loops when not halting. “Acceptance” of a TM closely examined Compared to DFAs and PDAs, the notion of acceptance for a TM is unusual in the following sense: a TM can accept an input without fully reading the input—or, in an extreme situation, not even reading one cell of the input (e.g., if q0 ∈ F)! Hence, curiously, any TM with q0 ∈ F has language Σ∗. On the other hand, if a TM never accepts, its language is ∅. This can be the result of the TM looping on every input, or the TM getting stuck in a reject state for every input. As a final illustration, given an arbitrary language L1, a TM that accepts any string within the set L1 and does not accept (loops or rejects) strings outside L1, has L1 as its language. Instantaneous descriptions: While capturing the ‘snapshot’ of a TM in operation, we need to record the control state of the machine, the contents of the tape, and what the head is scanning. All these are elegantly captured using an instantaneous description containing the tape contents, w, with a single state letter q placed somewhere within it. Specifically, suppose that the string lqr represents that the tape contents is lr, the finite-state control is in state q, and the head is scanning r[0]. The initial ID is q0w, for initial input string w. We define, the ‘step’ function that takes IDs to IDS, as follows: l1par1 l1bqr1 if and only if δ(p, a) = (q, b,R). The TM changes the tape cell contents a to b and moves right one step, facing r1[0], the first character of r1. Similarly, l1cpar1 l1qcbr1 if and only if δ(p, a) = (q, b,L). The TM changes an a to a b and moves left one step to now face c, the character that was to the left of the tape cell prior to the move.

3 min read

Computations vs. computation trees: In general, it is not sufficient to view the behavior of a system in terms of computational sequences, such as captured by waveforms. To see why, consider Figure 22.2, where two scenarios of a user interacting with a machine (say, a vending machine) are shown in the top and bottom half. In each scenario, the behavior shown to the left of the " sign is that of the vending machine, while the behavior shown to the right of the " sign is that of the human customer. The upper vending machine accepts a coin-drop (shown as a), and decides to allow the user to bang open its trap door (b). Since there are two (nondeterministic) ways to open the trap door, the user may be faced with a candy (c) or a donut (d) – never both at the same time! Since the user is always insistent on collecting a candy (c) after a b event, the system will deadlock if the machine chooses d instead of a c. Unfortunately, these “internal choices” made by the machine cannot3 often be controlled from outside, and so such machines do exist in real life. The machine in the bottom half is not

2 min read

CNF-conversion using gates: To contain the size explosion during the conversion of Boolean formulas to CNF or DNF, one can resort to a circuit-based representation of clauses. This keeps the sizes of formulas linear, but introduces a linear number of new intermediate variables. Theoretically, therefore, the exponential cost remains hidden. This is because during Boolean satisfiability, an exponential number of assignments can be sought for these new variables. In practice, however, we can often avoid suffering this cost. We now illustrate the idea of CNF conversion using gates through an example. Consider converting the DNF expression xyzw pqrs to CNF. We build a circuit net-list as follows, by introducing temporary nodes t1 through t7: t1 = and(x,y) ; t2 = and(z,w) ; t3 = and(p,q) ; t4 = and(r,s) t5 = and(t1,t2) ; t6 = and(t3,t4) ; t7 = or(t5,t6) Now, we convert each gate to its own CNF representation. We now illustrate one conversion in detail: The following ML functions accomplish the conversion of AND gates and OR gates into clausal form (t1 = x ∧ y was an example of the former):

2 min read

Pitfalls to Avoid: Let us do another example that points out a real pitfall. Consider the formulas Ff = ∀x.∃y.(x − y) = 1 and Ft = ∀y.∃x.(x − y) = 1. Over natural numbers, Ff is false (consider x = 0) while Ft is true. Following the method for DFA construction all the way through, however, Figure 20.6 (which only represents the common matrix of these formulas) will reduce to the same machine with empty language as shown in Figure 20.5. In other words, our reasoning shows that Ff and Ft are false.

3 min read

PCP is undecidable: The PCP is a fascinating undecidable problem! Since its presentation by Emil L. Post in 1946, scores of theoretical and practical problems have been shown to be undecidable by reduction from the PCP.4 A partial list includes the following problems: • Undecidability of the ambiguity of a given CFG (see Exercise 17.2). • Undecidability of aliasing in programming languages [101]. • Undecidability of the validity of an arbitrary sentence of first-order logic . The impressive diversity of these problems indicates the commonality possessed by this variety of problems that Post’s correspondence problems embody. The main undecidability result pertaining to PCPs can be phrased as follows. Given any alphabet Σ such that |Σ| > 1, consider the tile alphabet T ⊆Σ∗ × Σ∗. Now consider the language PCP = {S | S is a finite sequence over T that has a solution}. Theorem . PCP is undecidable. In, PCP is studied at a detailed level, and a software tool PCPSolver is made available to experiment with the PCP. The following terminology is first defined:

3 min read

CTL syntax: CTL formulas γ are inductively defined as follows: γ → x a propositional variable | ¬γ negation of γ | (γ) parenthesization of γ | γ1 ∨ γ2 disjunction | AG γ on all paths, everywhere along each path | AF γ on all paths, somewhere on each path | AX γ on all paths, next time on each path | EG γ on some path, everywhere on that path | EF γ on some path, somewhere on that path | EX γ on some path, next time on that path | A[γ1 U γ2] onallpaths, γ1 until γ2 | E[γ1 U γ2] on some path, γ1 until γ2 | A[γ1 W γ2] onallpaths, γ1 weak-until γ2 | E[γ1 W γ2] on some path, γ1 weak-until γ2 CTL semantics: The semantics of CTL formulas are defined over computation trees. Our approach to defining this semantics recurses over the structure of computation trees. We will also employ fixed-points to capture this semantics precisely. Some of the reasons for taking a different approach6 are the following:

3 min read

Basic Undecidability Proofs: In this chapter, we define the notion of decidability, semi-decidability, and undecidability. These notions pertain to degrees of solvability of problems by Turing machines. We will present three proof methods in this chapter: (i) through contradiction (Section 16.2.3), (ii) through reductions from languages unknown to be decidable (Section 16.2.4), and (iii) through mapping reductions (Section 16.2.5). Chapter 17 will discuss two additional proof methods: (iv) Rice’s theorem, and (v) computational history method. Methods (ii), (iii), and (iv) are strongly related to each other, in the following sense: The parallels between this chapter and Chapter 19 are worth reiterating. In this section, we present mapping reductions of the form A ≤m B where there exists a function f such that x ∈ A ⇔ f(x) ∈ B.

4 min read

Temporal formulas are Kripke structure classifiers!: CTL formulas can be viewed as classifiers of Kripke structures or as classifiers of computation trees. Both these views are equivalent (knowing the Kripke structure, we can obtain the computation tree, and vice versa). LTL formulas can also be viewed in the same manner. We now explain these ideas, beginning with CTL first. CTL formulas are Kripke structure classifiers: Given a CTL formula ϕ, all possible computation trees fall into two bins—models and non-models.5 The computation trees in the model (‘good’) bin are those that satisfy ϕ while those in the non-model (‘bad’) bin obviously falsify ϕ. Consider the CTL formula AG (EF (EG a)) as an example. Here, The truth of the formula AG (EF (EG a)) can be calculated as follows:

5 min read

Simulations: We show that having multiple tapes or having nondeterminism does not change the inherent power of a Turing machine. Multi-tape vs. single-tape Turing machines: A k-tape Turing machine simply maintains k instantaneous descriptions. In each step, its δ function specifies how each ID evolves. One can simulate this behavior on a single tape Turing machine by placing the k logical tapes as segments, end-to-end, on a single actual tape, and also remembering where the k tape heads are through “dots” kept on each segment. One step of a k-tape Turing machine now becomes a series of k activities conducted one after the other on the k tape segments. Nondeterministic Turing machines: A nondeterministic Turing machine can be conveniently simulated on a single tape deterministic Turing machine. However, it is much more convenient to explain how a nondeterministic Turing machine can be simulated on a multi-tape deterministic Turing machine. For the ease of exposition, we will carry this explanation out with respect to the example given in Figure 15.3. We will employ a 3-tape deterministic Turing machine to simulate the NDTM in Figure 15.3 (hereafter called ww ndtm). The first tape maintains a read-only copy of the initial input string given to ww ndtm. We call it the input tape. The second tape maintains a tree path in the nondeterministic computation tree of ww ndtm. We call it the tree path tape. The third tape is the “working tape.”

5 min read

NDTMs: An NDTM is a Turing machine with nondeterminism in its finite-state control, much like we have seen for earlier machine types such as PDAs. To motivate the incorporation of nondeterminism into Turing machines, consider a problem such as determining whether an undirected graph G has a clique (a completely connected subgraph) of k nodes.4 No efficient algorithm for this problem is known: all known algorithms have a worst-case exponential time complexity. Computer scientists have found that there exist thousands of problems such as this that arise in many practical contexts. They have not yet found a method to construct a polynomial algorithm for these problems. However, they have discovered another promising approach: Guess and check: While all this may sound bizarre, the fundamental ideas are quite simple. The crux of the matter is that many problems can be solved by the “guess and check” approach. For instance, finding the prime factors of very large numbers is hard. As [98] summarizes, it was conjectured by Mersenne that 2⁶⁷ − 1 is prime. This conjecture remained open for two centuries until Frank Cole showed, in 1903, that it wasn’t; in fact, 2⁶⁷−1 = 193707721×761838257287. Therefore, if we could somehow have guessed that 193707721 and 761838257287 are the factors of 2⁶⁷ − 1, then checking the result would have been extremely easy! The surprising thing is that there are two gradations of “difficulty” among problems for which only exponential algorithms seem to exist: those for which short guesses exist, and checking the guesses is easy, and those for which the existence of short guesses is, as yet, unknown. To sum up:

4 min read

Validity of first-order logic is undecidable: Valid formulas are those that are true under all interpretations. For example, ∀x.f (x) = g(x) ⇒ ∃a.f (a) = g(a). Validity stems from the innate structure of the formula, as it must remain true under every conceivable interpretation. We will now summarize Floyd’s proof that the validity problem for firstorder logic is undecidable. First, an abbreviation: for σi ∈ {0, 1}, use the abbreviation fσ1,σ2,...,σn(a) = fσn(fσn−1 (. . . fσ1(a)) . . .). The proof proceeds by building a FOL formula for a given “Post system” (an instance of Post’s correspondence problem). Given a Post system S = {(α1, β1), (α2, β2), . . . , (αn, βn), n ≥ 1 over Σ = {0, 1}, construct the wff WS (we will refer to the two antecedents of WS as A1 and A2, and its consequent as C1): We now prove that S has a solution iff WS is valid. Part 1. (WS valid) ⇒ (S has a solution). If valid, it is true for all interpretations. Pick the following interpretation: a = ε f0(x) = x0 (string ‘x’ and string ‘0’ concatenated) f1(x) = x1 (similar to the above) p(x, y) = There exists a non-empty sequence i1i2 . . . im such that x = αi1αi2 . . .αim and y = βi1βi2 . . .βim Under this interpretation, parts A1 and A2 of WS are true. Here is why: Part 2. (WS valid) ⇐ (S has a solution). If S has a solution, let it be the sequence i1i2 . . . im. In other words, αi1αi2 . . .αim = βi1βi2 . . . βim = Soln. Now, in order to show that WS is valid, we must show that for every interpretation it is true. We approach this goal by showing that under every interpretation where the antecedents ofWS, namely A1 and A2, are true, the consequent, namely C1, is also true (if any antecedent is false, WS is true, so this case is not considered). From A1, we conclude that p(fαi1 (a), fβi1 (a)) is true. Now using A2 as a rule of inference, we can conclude through Modus ponens, that p(fαi2 (fαi1 (a)), fβi2 (fβi1 (a)) is true. In other words, p(fαi1αi2 (a), fβi1βi2 (a)) is true. We continue this way, applying the functions in the order dictated by the assumed solution for S; in other words, we arrive at the assertion that the following is true (notice that the subscripts of f describe the order in which the solution to S considers the α’s and β’s): p(fαi1αi2 ...αim(a), fβi1βi2...βim(a)).

4 min read

Introduction:

7 min read

An Introduction to Model Checking: The development of model checking methods is one of the towering achievements of the late 20th century in terms of debugging concurrent systems. This development came about in the face of the pressing need faced by the computing community in the late 1970’s for effective program debugging methods. The correctness of programs is the central problem in computing, because there are often very designs that are correct, and vastly more that are incorrect. In some sense, defining what ‘correct’ means is half the problem - proving correctness being the other half of the problem. The quest for high performance and flexibility in terms of usage (e.g., in mobile computing applications) require systems (software or hardware) to be designed using multiple computers, processes, threads, and/or function units, thus quickly making system behavior highly concurrent and non-intuitive. With the rapid progress in computing, especially with the availability of inexpensive microprocessors, the computer user community found itself – in the late 1970’s – in a position where it had plenty of inexpensive hardware but close to no practical debugging methods for concurrent systems! We will now examine the chain of events that led to the introduction of model checking in this setting. Model checking in the design of modern microprocessors: All modern microprocessors are designed to be able to communicate with other microprocessors through shared memory. Unfortunately since only one processor can be writing at any memory location at a given time, and since “shared memory” exists in the form of multiple levels of caches, with further levels of caches being far slower to access than nearly levels of caches, extremely complex protocols are employed to allow processors to share memory. Even one bug in one of these protocols can render a microprocessor useless, requiring a redesign that can cost several 100s of millions of dollars. No modern microprocessor is sold today without its cache coherence protocol being debugged through model checking. Model checking in the design of device drivers: Drivers for computer input/output devices such as Floppy Disk Controllers, USB Drivers, and Blue-tooth Drivers are extremely complex. Traditional debugging is unable to weed out hidden bugs unless massive amounts of debugging time are expended. Latent bugs can crash computers and/or become security holes. Projects such as the Microsoft Research SLAM project have technology transitioned model checking into the real world by making the Static Driver Verifier part of the Windows Driver Foundation. With this, and other similar developments, device-driver writers now have the opportunity to model-check their protocols and find deep-seated bugs that have often escaped, and/or have taken huge amounts of time to locate using traditional debugging cycles. Has the enterprise of model checking succeeded? What about social processes? We offer two quotes:

2 min read

3-CNF, =-satisfiability, and general CNF: A 3-CNF formula is a CNF formula in which every clause has three literals. For example, is a 3-CNF formula. As can be seen, there is no requirement on what variables the clauses might involve. Many proofs are rendered easier by standardizing on the 3-CNF form. In many proofs, it will be handy to restrict the satisfying assignments allowed. One useful form of this restriction is the =-satisfiability restriction. Given a 3-CNF formula, a =-assignment is one under which every clause has two literals with unequal truth values. Given a set of N clauses where the ith clause is ci = yi1 ∨ yi2 ∨ yi3, suppose we transform each such clause into two clauses by introducing a new variable zi per original clause, and a single variable b for the whole translation:

5 min read

and left hands (respectively), while P1 would eat with F1 and F2, and P2 with F2 and F0. Clearly, when one philosopher ‘chows,’ the other two have to lick their lips, patiently waiting their turn. It is assumed that despite their advanced state of learning, they are disallowed from trying to eat with one fork or reach across the table for the disallowed fork. In order to pick up a fork, a philosopher sends a message to the fork through the appropriate channel. For example, to acquire F0 or F1, respectively, P0 would send an are_you_free request message through channel C5 or C0, respectively. Such a request obtains a “yes” or a “no” reply. If the reply is “yes,” the philosopher acquires the fork; otherwise he retries (if for the left fork) or gives up the already acquired left fork and starts all over (if for the right fork). Consequently, the deadlock due to all the philosophers picking up their left forks and waiting for their right forks does not arise in our implementation. After finishing eating, a philosopher puts down the two forks he holds by sequentially issuing two release messages, each directed at the respective forks through the appropriate channels. Figure 21.2 describes how the above protocol is described in the Promela modeling language. Consider the init section where we create channels c0 through c5. Each channel is of zero size and carries mtype messages. Communication through a channel of size 0 occurs through rendezvous wherein the sender and the receiver both have to be ready in order for the communication to take place. As one example, consider when proctype phil executes its statement lf!are_you_free. We trace channel lf and find that it connects to a philosopher’s left-hand side fork. This channel happens to be the same as the rp channel as far as fork processes are concerned (rp stands for the ‘right-hand philosopher’ for a fork). These connections are specified in the init section. Hence, proctype fork must reach rp?are_you_free statement at which time both lf!are_you_free and rp?are_you_free execute jointly. As a result of this rendezvous, proctypes phil as well as fork advance past these statements in their respective codes. Continuing with the init section, after “wiring up” the phil and fork processes, we run three copies of phil and three copies of fork in parallel (the atomic construct ensures that all the proctype instances start their execution at the same time). The never section specifies the property of interest, and will be described in Sections 21.4.1 and 22.1. Now we turn our attention to the proctypes phil and fork.

3 min read

Basic Notions in Logic including SAT

2 min read

2-CNF satisfiability A 2-CNF formula is one where each clause has two literals. One can show that the satisfiability of 2-CNF is polynomial-time, as follows: Now, the following results can be shown: – If a literal x (for variable x) is followed by literal ¬x in the graph, assign x false. – If a literal ¬x (for variable x) is followed by x in the graph, assign x true. – Else assign x arbitrarily.

2 min read

2 min read

Unsatisfiable CNF instances Consider the unsatisfiable CNF formula represented by the DIMACS file in Figure 18.4: An important theorem pertaining to unsatisfiable CNF formulas is the following: Theorem 18.1. In any unsatisfiable CNF formula, for any assignment, there will be one clause with all its variables false and another with all its variables true. Proof: We can prove this fact by contradiction, as follows. Suppose Fmla is an unsatisfiable CNF formula and there is an assignment σ under which one of the following cases arise (both violating the ‘one clause with all its variables false and another with all its variables true’ requirement):

3 min read

Proof sketch of the undecidability of PCP: The basic idea behind the proof of undecidability of PCP is to use ATM and the computation history method. In particular, The crux of achieving the above reduction is to generate each set of tiles carefully; here is how we proceed to generate the members of Tiles.6 Here, the following notations are used: if u is the string of characters u1u2 . . .un,

3 min read

RICE’S THEOREM: A Turing machine (TM) is a way to describe a language and the decision problem can be interpreted as belonging to the general class of problems: “Given a Turing machine, does L(TM) have the property P”? In this case P is the property of containing the null string. THEOREM: “If P is a property of languages that is satisfied by some but not all recursively enumerable languages, then the decision problem. D: Given a TM, does L(TM) have property P is unsolvable.”

3 min read

Enumerating Strings in a Language: To enumerate a set is to place the elements of the set in a one-to-one correspondence with the natural numbers. The set of all strings over an alphabet is denumerable. Let us assume that a string is a number is an | S| -ary number system. The strings in a language from a subset of the set of all strings over S. But is it possible to enumerate the strings in a language? If a language is recursive, then there exists a Turing machine for it that is guaranteed to halt. We can generate the strings of S* in a shortest first order to guarantee that every finite string will be generated, test the string with the Turing machine, and if the Turing machine accepts the string, assign that string the next available natural number. We can also enumerate the recursively enumerable languages. We have a Turing machine that will halt and accept any string that belongs to the language; the trick is to avoid getting hung up on strings that cause the Turing machine to go into an infinite loop. This is done using “Time sharing”. Let us illustrate this now.

3 min read

Turing Machine: A Turing Machine is like a Pushdown Automaton. Both have a finite-state machine as a central component, both have additional storage. A Pushdown Automaton uses a “stack” for storage whereas a Turing Machine usea a “tape”, which is actually infinite in both the directions. The tape consists of a series of “squares”, each of which can hold a single symbol. The “tape-head”, or “read-write head”, can read a symbol from the tape, write a symbol to the tape and move one square in either direction. There are two kinds of Turing Machine available.

2 min read

Programming a Turing Machine: As we have the “productions” as the control theme of a grammar, the “transitions” are the central theme of a Turing machine. These transitions are given as a table or list of S-tuples, where each tuple has the form (current state, sym bol read, sym bol writ ten, direc tion, next state) Creating such a list is called “programming” a Turing machine. A Turing machine is often defined to start with the read head positioned over the first (leftmost) input symbol. This is not really necessary, because if the Turing machine starts anywhere on the nonblank portion of the tape, it is simple to get to the first input symbol.

2 min read

CHURCH–TURING’S THESIS: Alan Turing defined Turing machines in an attempt to formalize the notion of an “effective producer” which is usually called as ‘algorithm’ these days. Simultaneously mathematicians were working independently on the same problem. Emil Post -> Production Systems Alonzo Church -> Lambda Calculus

3 min read

COMPLETE LANGUAGES AND FUNCTIONS: A Turing machine has an output function, the contents of the input tape after processing, a given input string can be viewed as the result of computation. Therefore a Turing machine is seen as a computer of functions, from integers to integers. Let us now look at the procedure to compute functions f (n1 , n2 ,. . . nk ) where n1 , n2 , . . . , nk are non-negative integers. (a) Represent the integers n1 , n2 , KK , nk in unary i.e., n1 is written as 0n1 etc. The input (n1 , n2 ,., nk ) is represented by 0ⁿ¹10ⁿ². . . 10^nkwhere the 1’s are used to separate the unary representation of n1 , n2 , . . . . , nk .

3 min read

MODIFICATION OF TURING MACHINES: Two automata are said to be equivalent if they accept the same language. Two transducers are said to be equivalent if they compute the same function. A class of automata e.g., Standard Turing machines is equivalent to another class of automata e.g., nondeterministic Turing machines, if for each transducer in one class, an equivalent transducer can be found in another class. At each move of a Turing machine, the tape head may move either left or right. We can augment this with a “Stay option”, i.e., we will add “don’t move” to the set {L, R}. “Turing machines with a stay option are equivalent to Standard Turing Machines.”

3 min read

RICE’S THEOREM: A Turing machine (TM) is a way to describe a language and the decision problem can be interpreted as belonging to the general class of problems: “Given a Turing machine, does L(TM) have the property P”? In this case P is the property of containing the null string. THEOREM: “If P is a property of languages that is satisfied by some but not all recursively enumerable languages, then the decision problem. D: Given a TM, does L(TM) have property P is unsolvable.”

2 min read

Turing Machines as Transducers: To use a Turing machine as a transducer, treat the entire nonblank portion of the initial tape as input, and treat the entire nonblank portion of the tape when the machine halts as output. A Turing machine defines a function y = f (x) for strings x, yÎS* if

3 min read

LTL syntax: LTL formulas ϕ are inductively defined as follows, through a contextfree grammar: ϕ → x, a propositional variable | ¬ϕ negation of an LTL formula | (ϕ) parenthesization | ϕ1 ∨ ϕ2 disjunction | Gϕ henceforth ϕ | Fϕ eventually ϕ (“future”) | Xϕ next ϕ | (ϕ1U ϕ2) ϕ1 until ϕ2 | (ϕ1W ϕ2) ϕ1 weak-until ϕ2 Note that G is sometimes denoted by
while F is denoted by ♦. We also introduce the X operator into the syntax above to capture the notion of next in a time sense. It is clear that in many real systems— for example, in globally clocked digital sequential circuits—the notion of next time makes perfect sense. However, in reasoning about the executions of one sequential process Pi among a collection of parallel processes P1, . . . , Pn, the notion of next time does not have a unique meaning. As far as Pi is concerned, it has a list of candidate “next” statements to be considered; however, these candidate statements may be selected only after an arbitrary amount of interleavings from other processes. Hence, what is “next” in a local sense (from the point of view of Pi alone) becomes “eventually” in a global sense. While conducting verification, we will most likely not be proving properties involving X. However, X as a temporal operator can help expand other operators such as G through recursion. With this overview, we now proceed to examine the semantics of LTL. LTL semantics: Recall that the semantics of LTL are defined over (infinite) computational sequences. LTL semantics can be defined over computation trees by conjoining the truth of an LTL formula over every computational sequence in the computational tree. Let σ = σ0 = s0, s1, . . ., where the superscript 0 in σ0 emphasizes that the computational sequence begins at state s0. By the same token, let σi = si, si 1, . . ., namely the infinite sequence beginning at si. By σ |= ϕ we mean ϕ is true with respect to computation σ; σ |= ϕ means ϕ is false with respect to computation σ. Here is the inductive definition for the semantics of LTL: σ |= x iff x is true at s0 (written s0(x)) σ |= ¬ϕ iff σ |= ϕ σ |= (ϕ) iff σ |= ϕ σ |= ϕ1 ∨ ϕ2 iff σ |= ϕ1 ∨ σ |= ϕ2 σ |= Gϕ iff σi |= ϕ for every i ≥ 0 σ |= Fϕ iff σi |= ϕ for some i ≥ 0 σ |= Xϕ iff σ1 |= ϕ σ |= (ϕ1U ϕ2) iffσk |= ϕ2 for some k ≥ 0 and σj |= ϕ1 for all j < k σ |= (ϕ1W ϕ2) iffσ |= Gϕ1 ∨ σ |= (ϕ1U ϕ2) LTL example: Consider formula GF x (a common abbreviation for G(F x)). Its semantics are calculated as follows: σ |= GFx iff σi |= Fx, for all i ≥ 0 σi |= Fx iff σj |= x, for some j ≥ i Putting it all together, we obtain the meaning as: x is true infinitely often—meaning, beginning at no point in time is it permanently false.