Behaviour examples for synthesizing automaton models by temporal formulas

Authors

  • Dmitry V. Pashchenko Penza State Technological University, 440039, Russia, Penza, 1/11 Baydukova lane/Gagarina St., 1/11
  • Alexey I. Martyshkin Department of Computational Automatons and Systems, Penza State Technological University, 440039, Russia, Penza, 1/11 Baydukova lane/Gagarina St., 1/11
  • Dmitry A. Trokoz Penza State Technological University, 440039, Russia, Penza, 1/11 Baydukova lane/Gagarina St., 1/11
  • Tatyana Yu. Pashchenko Sub-department of Management and Economic Security, Penza State University, 440026, Russia, Penza, Krasnaya Street, 40
  • Mikhail Yu. Babich JSC Research and Production Enterprise “Rubin”, 440000, Russia, Penza, Baydukova St., 2
  • Mikhail M. Butaev JSC Research and Production Enterprise “Rubin”, 440000, Russia, Penza, Baydukova St., 2

DOI:

https://doi.org/10.5377/nexo.v34i01.11285

Keywords:

automaton model, discrete-event simulation, finite state automaton, conflicting situation, methods of accounting for behaviour examples

Abstract

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

Download data is not yet available.

Downloads

Published

2021-04-13

How to Cite

Pashchenko, D. V., Martyshkin, A. I., Trokoz, D. A., Pashchenko, T. Y., Babich, M. Y., & Butaev, M. M. (2021). Behaviour examples for synthesizing automaton models by temporal formulas. Nexo Scientific Journal, 34(01), 61–73. https://doi.org/10.5377/nexo.v34i01.11285

Issue

Vol. 34 No. 01 (2021)

Section

Articles

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 https://creativecommons.org/licenses/by/3.0/, 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.

Similar Articles

You may also start an advanced similarity search for this article.

Most read articles by the same author(s)