Finite State Models 1.1 Introduction 1.1.1 Finite state machines belong to a restricted class of Turing machines in which a sequence of symbols is read from an input tape and a resulting sequence of symbols is written to an output tape. Neither input nor output can be referred to at a later stage, the data tape serves solely as the interface with an external environment and cannot be considered to be a form of memory. There is no means of storing any intermediate results, except in the states of the control unit themselves, states which result from application of a sequence of inputs. In effect, the states represent a summary of some aspects of the previous history of the machire. A finite state machine is the only class of Turing machine which car be realised by physical means completely. It represents a sequential machine corresponding to a "black box” concept in which a model reads a sequence of input symbols and outputs a sequence of symbols synchronously. 1.1.8 Finite state machines can be used to formally specify certain types of system. It is an abstraction of the problem for which a specification is required, a model which can be checked for consistency and completeness against the informal problem specification. There are well known proven techniques for automatically analysing and manipulating the models. Consider an example of a rock sample to be treated with one of two fluids A or B, as a result of which heat may be generated. The material of the sample may change into one of three states as a result of applying fluid A or B. Label the states sl, s2 and S3. It is known that A causes a change from state s3 to s2 and no change in any other state. Treatment with B will always Cause a change into s3. Heat is generated when B is applied in ate s2 and in no other case. The system can be represented by means of a finite state model with: a set of state labels: S = [sl,s2,s3], an input alphabet: X = [A,B], an output alphabet: V = [Yes,No], a table of state changes, i.e. state transitions, and a table of outputs. This can be specified in Pascal by reading two arrays NEXT and OUT, whose elements satisfy the following set of declarations: Type rockst = (sl,s2,s3); fluid (A,B); heat = (Yes,No); Var STATE:rockst; INPUT:fluid; OUTPUT:heat; NEXT :array[sl..s3] of array(A..B] of rockst; OUT :array[sl..s3] of array[A..B) of heat; A representation of the model, in tabular form, is shown in Table 1.1 and in graph form in Figure 1.1. Table 1.1 Model of a rock sample in tabular form. Figure 1.1 State Transition Graph for model of rock sample. The properties of the rock sample may have been defined in a slightly different way, the heat generation being observed immediately after the transition, continuing to be observable until the next treatment. The output can then be defined as a property of states, some of which may need to be reconsidered. In particular, state 53 is to be represented in two ways, each associated with a different output, (S3/No and S3/Yes). The alternative system can be represented by means of a finite state model with: a set of state labels: S = [sl,s2,s4,s5], an input alphabet: X = [A,B], an output alphabet: V = [Yes,No], a table of state changes, i.e. state transitions, and a table of outputs. This can be specified in Pascal by reading two arrays NEXT and OUT, whose elements satisfy the following set of declarations: Type rockst=(sl,s2,s4,s5) ; fluid=(A,B); heat(Yes,No) Var STATE:rockst; INPUT:fluid; OUTPUT:heat; NEXT :array[sl. .s3] of array[A. .B] of rockst; OUT :array[sl. .s3] of heat; A representation of the model, in tabular form, is shown in Table 1.2 and in graph form in Figure 1.2. Table 1.2 Model of a rock sample in tabular form. Figure 1.2 State Transition graph for model of a rock sample 1.2 Formal descriptions of finite state machines 1.2.1 A finite state machine is defined by: a) A finite number of states. b) Finite input and output alphabets. Symbols which have been output will not be read back at a later stage, so that it is not necessary that the two alphabets are the same. c) A state transition function which specifies the next state of the machine, the state successor, for every state/input combination. d) An output function. Two types of model have been studied: i) a Mealy model for which a value of the output function is specified for every state/input combination. ii) a Moore model for which a value of the output function is specified for each state. The input, output and time variables are all considered to be discrete, (not continuous), taking values from discrete finite alphabets. The behaviour of the machine is synchronous, state transitions occuring at successive instants in time. Precisely how state transitions take place is not considered as relevant and the state is assumed to remain constant between the state transitions.