Behaviour examples for synthesizing automaton models by temporal formulas
DOI:
https://doi.org/10.5377/nexo.v34i01.11285Keywords:
automaton model, discrete-event simulation, finite state automaton, conflicting situation, methods of accounting for behaviour examplesAbstract
The paper deals with researching and developing the methods that make it possible to account behaviour examples when synthesizing automaton models by temporal formulas. Definitions of the terms and concepts used in work are given; the problem of synthesizing automaton systems according to the specification in the form of temporal formulas and behaviour examples is formulated; a promising algorithm for reducing the problem of synthesizing automaton systems to the Boolean formula satisfiability problem is described; an analysis of the domain and other approaches is carried out. New methods of taking into account behaviour examples in the synthesis of automaton systems according to a specification given in the form of temporal formulas are proposed. Algorithms for constructing graphs of scripts and methods for dividing graphs into clusters are described; they are designed to increase the efficiency of representing behaviour examples used for coding the behaviour examples in the form of Boolean formulas. An experimental study of the proposed methods of accounting for behaviour examples and basic approaches to the presentation of behaviour examples is carried out. The experimental results showed the superiority of the newly developed methods regarding the presentation of scripts in the form of temporal formulas. In summary, the main conclusions of the work carried out are presented.
Downloads
604
Downloads
Published
How to Cite
Issue
Section
License
The authors who publish in Nexo Scientific Journal agree to the following terms:
- Authors retain the copyright and grant the journal the right of the first publication under the license Creative Commons Attribution License, which allows others to share the work with a recognition of the authorship of the work and the initial publication in Nexo Scientific Journal.
- Authors may separately establish additional agreements for the non-exclusive distribution of the version of the work published in the journal (for example, in an institutional repository or a book), with the recognition of the initial publication in Nexo Scientific Journal.
- Authors are allowed and encouraged to disseminate their works electronically (for example, in institutional repositories or in their own website) before and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published works.