Solving parallel equations for Finite State Machines with Timeouts

Abstract

The problem of designing an unknown component that combined with the known part of a discrete event system satisfies the given overall specification arises in a number of applications. In this paper, we extend the known results for classical Finite State Machines (FSM) to Finite State Machines with Timeouts (TFSM). A TFSM is an FSM augmented with an input and an output timeout functions, prescribing the change of current state if no input is applied until a specified timeout expires and system delays needed to response to applied input, respectively. We represent the behavior of a TFSM by the corresponding regular language. The parallel composition of two TFSMs S and P is defined via composition of languages L(S) and L(P) intersected with L(MC), where MC is a maximal TFSM over input and output alphabets of the composition. The unknown component X is then designed as a solution to the equation where A and X are compared by ≤ with C. Here A is a context, C is a specification, and ≤ is the reduction relation which specifies that the behavior of a system to be designed is contained in that of the specification. Similar to classical FSMs, the equation is transformed to a language equation, the largest solution for which provides the largest solution to the solvable TFSM equation. After the largest solution is derived, a corresponding reduction can be extracted in order to provide the component with required properties. The application areas vary from testing in context to quality optimization of service compositions. Future work includes studying equation solvability criteria and properties of nondeterministic and partial specifications and solutions.