Transformation of a language L* specification of an FSM into an automata equivalent specification in the language L
- PDF / 143,067 Bytes
- 9 Pages / 595.276 x 793.701 pts Page_size
- 57 Downloads / 169 Views
TRANSFORMATION OF A LANGUAGE L* SPECIFICATION OF AN FSM INTO AN AUTOMATA EQUIVALENT SPECIFICATION IN THE LANGUAGE L UDC 519.713.1
A. N. Chebotarev
Abstract. A method is proposed to transform an FSM specification in the language L* into a specification in the language L. Using additional predicate symbols, the former specification is first transformed into a specification of an FSM with finite memory. Then this specification is transformed into an automata equivalent specification in the language L. Keywords: specification language L* , $-formula, two-sided superword, S-automaton, elimination of quantifiers, automata equivalence of specifications. INTRODUCTION The used approach to the provably correct design of reactive algorithms is underlain by a specification of functional requirements on an algorithm in the language of first-order logic with one-place predicates and the formal passage from the specification to a procedural representation of the algorithm. One of main problems connected with the specification of properties of an algorithm is the development of a suitable specification language. In this case, one is forced to search for a compromise between the expressiveness of such a language and complexity of design algorithms. To resolve this contradiction, the following two language levels are used: the language of original specification L* [1] that has an expressiveness sufficient for practical needs and provides the convenience of writing functional requirements on an algorithm, and the language L [2] that has a rather limited expressiveness but is efficiently processed by synthesis procedures. The possibilities of specification in the L language are restricted to FSMs with finite memory [3], which made it possible to develop efficient algorithms of synthesis, consistency check, and verification of temporal properties and also design methods for open systems that include reactive algorithms for specifications in this language. Therefore, the language L* is used (when necessary) for the initial specification that then is transformed into a specification in the language L. In [4], a method of passage to a specification in the language L is considered, but an FSM synthesized from the specification obtained by this method can have additional or the so-called fictitious states. To eliminate fictitious states, the procedure of checking some states of an FSM for fictitiousness [5] is used. This procedure is rather complicated and, in contrast to all other design procedures for algorithms, uses a procedural representation of an FSM in the form of a set of states and transition and output functions rather than in the form of formulas of the specification language. This article proposes a transformation of an original specification into a specification in the L language; the latter specification represents an FSM that is equivalent to the FSM specified by the original specification in the language L* . Since the languages L* and L have different expressiveness, this passage is carried out owing to the introduction
Data Loading...
