Finite State Machines: Definitions;VerificationGreg PlaxtonTheory in Programming Practice, Fall 2005Department of Computer ScienceUniversity of Texas at AustinFinite State Machine: Definition• A (deterministic) finite state machine consists of:– A finite number of states, where one state is designated as the initialstate, and a subset of the states are designated as accepting– A state transition function that specifies the next state for each stateand input symbol• A finite state machine accepts or rejects each finite string over theinput alphabet• To determine whether a given finite string is accepted, start in theinitial state and repeatedly update the state according to the nextinput symbol and the state transition function– The input string is accepted if and only if this process terminates inan accepting stateTheory in Programming Practice, Plaxton, Fall 2005Finite State Machine: Correspondence to a “Language”• Let A denote the input alphabet of some FSM M• As we have seen, M accepts some subset of the set of all finite stringsover A• The set of strings accepted by M is the language accepted by MTheory in Programming Practice, Plaxton, Fall 2005Finite State Machine: Pictorial Representation• Each state is depicted by a circle• An arrow labeled “start” points to the initial state• Each accepting state has a double circle• The transition function is specified by drawing arrows labeled by eithera single input symbol or a set of input symbols– The label on an arrow associated with a transition from state u tostate v indicates which input symbols cause this transition to betaken– Normally, a transition is explicitly specified for each state and inputsymbol– Remark: If certain transitions are not explicitly specified, the intendedinterpretation is that any input string leading to an unspecifiedtransition is rejectedTheory in Programming Practice, Plaxton, Fall 2005Verification of FSMs• In a previous lecture we designed a few simple FSMs that seemed tobe correct in terms of accepting a specified language– Example: The finite state machine we designed to accept wordscontaining the five vowels in order• How can we formally verify the correctness of such FSMs?– Our strategy is to label each state with (our guess as to) the set offinite strings leading to that state– These labels may be verified using induction (assuming that ourguesses are correct)Theory in Programming Practice, Plaxton, Fall 2005Verification Procedure• First, annotate each state with a predicate over finite strings– The predicate defines a set of input strings, namely, those for whichthe predicate holds (i.e., evaluates to true)– This corresponds to our guess as to the set of input strings leadingto this state– As such, the sets of input strings defined by the annotations isrequired to partition the set of all input strings• Second, show that the predicate associated with the initial state holdsfor the empty string• Third, prove that for any transition from a state u to a state v on inputsymbol a, if some finite string x satisfies the state u annotation, thenthe finite string xa satisfies the state v annotationTheory in Programming Practice, Plaxton, Fall 2005Verification Procedure: Why Does it Work?• Let x be an arbitrary input string• Let the given FSM M be in state u after processing x– Because M is deterministic, the state u is uniquely defined• Let v denote the unique state for which the associated annotation holdsfor x– The existence/uniqueness of v follows from the requirement that thestate annotations partition the set of all input strings• We prove that u = v by induction on the length of x– The second part of the verification procedure handles the base case– The third part handles the induction stepTheory in Programming Practice, Plaxton, Fall 2005Verification Example: Parity• Design an FSM to accept all finite binary strings with an odd numberof 0s and an odd number of 1s• Verify the correctness of your FSMTheory in Programming Practice, Plaxton, Fall 2005Verification Example: Ascending Digits• Design an FSM to accept any finite string of decimal digits in whicheach successive digit is strictly higher than the preceding one (e.g., 038or 13579)• Verify the correctness of your FSMTheory in Programming Practice, Plaxton, Fall 2005Another Example• Design an FSM to accept all finite binary strings with an equal numberof zeros and ones• Is this possible?Theory in Programming Practice, Plaxton, Fall 2005Some Closure Properties of FSMs• Let FSMs M1and M2accept the languages L1and L2, respectively• Is it possible to give a general procedure to construct an FSM acceptingL1∪ L2from FSMs M1and M2?• What about L1∩ L2?• What about L1?Theory in Programming Practice, Plaxton, Fall