Том 53, № 7 (2019)

This paper presents the ontology of the concurrent processes close to Hoare communicating sequential processes. It is a part of an intellectual system for supporting verification of behavioral properties of such processes. Our ontological representation of the processes is oriented both to the application of formal verification methods and to the extraction of information from technical documentation (by our previously developed system of information extraction from a natural language text). We describe the ontology classes and domains that define communicating concurrent processes. These processes are characterized by sets of local and shared variables, a list of actions on these variables which change their values, a list of channels for the process communication (which, in turn, are characterized by the type of reading messages, capacity, modes of writing and reading, and reliability), and also a list of communication actions for sending messages. In addition to the formal mathematical definition of classes and domains of the ontology, examples of descriptions of some ontological classes, as well as typical properties and axioms for them, are specified in the editor Protégé in the OWL language with the use of the inference rules in the SWRL language. We define the formal operational semantics of communicating processes for their ontological representation. This semantics is a labeled transition system. It is reduced to the local operational semantics of separate process instances in the interleaving model. We specialize several types of processes from the subject domain of automatic control systems that model the typical functional elements of the automatic control system (sensors, comparators and regulators), as well as their combinations. The concepts of the specialized ontology are illustrated by the example of a control part of a bottle-filling system.

Finding graph edit distances (determining the similarity of graph models) is an important task in various areas of computer science, such as image analysis, machine learning, and chemoinformatics. In recent years, due to the development of process mining techniques, it has become necessary to adapt the existing graph matching methods to be applied to the analysis of process models (annotated graphs) discovered from event logs of information systems. In particular, methods for finding the minimum graph edit distance can be used to reveal patterns (subprocesses) and to compare discovered process models. As was shown experimentally and theoretically substantiated, exact methods for finding the minimum edit distance between the discovered process models (and graphs in the general case) have a great time complexity and can be applied only to small-sized process models. In this paper, we estimate the accuracy and time performance characteristics of a genetic algorithm applied to find distances between process models discovered from the event logs. In particular, we find distances between BPMN (Business Process Model and Notation) models discovered from the event logs by using different synthesis algorithms. It is shown that the genetic algorithm proposed in the paper allows us to significantly reduce the computation time and produces results close to the optimal solutions (the minimum edit distances).

The ability to identify semantic relations between words has made a word2vec model widely used in NLP tasks. The idea of word2vec is based on a simple rule that a higher similarity can be reached if two words have a similar context. Each word can be represented as a vector, so the closest coordinates of vectors can be interpreted as similar words. It allows to establish semantic relations (synonymy, relations of hypernymy and hyponymy and other semantic relations) by applying an automatic extraction. The extraction of semantic relations by hand is considered as a time-consuming and biased task, requiring a large amount of time and some help of experts. Unfortunately, the word2vec model provides an associative list of words which does not consist of relative words only. In this paper, we show some additional criteria that may be applicable to solve this problem. Observations and experiments with well-known characteristics, such as word frequency, a position in an associative list, might be useful for improving results for the extraction of semantic relations for the Russian language by using word embedding. In the experiments, the word2vec model trained on the Flibusta and pairs from Wiktionary are used as examples with semantic relationships. Semantically related words are applicable to thesauri, ontologies and intelligent systems for natural language processing.

In the deductive verification of programs written in the imperative programming languages, the generation and proving of the verification conditions corresponding to loops are of particular complexity, as each of them must be provided with an invariant, whose construction is often a challenge. As a rule, the methods for the synthesis of loop invariants have a heuristic character, which complicates their application. An alternative is the symbolic loop invariant elimination method proposed by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in the form of a special replacement operation under certain constraints. Such an operation in the symbolic form expresses the loop effect, which allows introducing an inference rule for the loops without invariants into axiomatic semantics. This work is the further development of this method. It extends the proposed method of mixed axiomatic semantics for the verification of C-light programs. This extension incorporates the method for the verification of iterations over changeable arrays with the possible exit from the loop body in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule has been implemented in the verification condition generator, which is a part of the automated system for the verification of C-light programs. To perform automated verification in the used ACL2 system, two algorithms, one of which generates the replacement operation in the ACL2 language, and the second generates the auxiliary lemmas resulting in the successful automated proof of the obtained verification conditions in the ACL2 system have been developed and implemented. The application of the above mentioned methods and algorithms is illustrated with an example.

Nowadays, the methods of program-targeted management for the development of various socio-economic systems of complex structure, such as agricultural areas, have become ubiquitous. Therefore, the current tasks at hand are the verification of already created development programs and the development of “proper” programs for the development of such systems, by analogy with the verification and development of proper computer programs through advanced disciplines in theoretical programming. In this paper, in order to solve the problem of the verification of development programs for agricultural territories, a structural scheme of the program is first constructed, through which an axiomatic theory is created using the Hoare’s algorithmic logic system. The main problem in the construction of the axiomatic theory is the development of the axioms of the theory that reflect preconditions and effects of the implementation of meaningful actions indicated in the text of the development program. The verification of the development program corresponds to the provability check of some Hoare triplet, according to the initial and target conditions of the program. For the task of elaborating proper development programs, we describe the mechanism for constructing a domain model using the PDDL family description languages. The description of a specific model is purely declarative in nature and consists of descriptions of predicates and actions of the chosen subject area. In this paper, using the described model with the help of intelligent planners, including temporal planners such as OPTIC, we show how to automatically build solutions to the targets of development programs. Based on expert knowledge and industry standards, a model of an agricultural territory is constructed, a brief description of which is given in this work. The conducted experiments showed the effectiveness of the proposed approach for the development of proper development programs.

The article considers a file distribution model in a peer-to-peer file-sharing network based on ordinary differential equations. Phase variables describing the file-sharing state are determined (in the first approximation, this is the number of users, i.e., seeders and leechers of the shared file). The factors affecting file sharing and the change in the number of peers are analyzed. The system of differential equations describing the evolution of a torrent, or a file-sharing session (FSS), i.e., the dynamic FSS evolution model, is constructed based on the analysis. The life cycle of a FSS in the file-sharing network consisting of four stages, i.e., file sharing initiation, rapid increase in the number of leechers, stabilization, and fading (for files that lose relevance over time), is considered. Each stage is characterized by its own ratio of model parameters. The parameters change over time. The process of measuring the state of real FSSs is described. An example of a trajectory corresponding to the evolution of a real FSS on a large torrent tracker is given. Next, the FSS stabilization stage characterized by parameters that are constant in the first approximation is considered. Equilibrium points of the dynamic model of the FSS evolution are investigated. Their possible number and type are described. All generic position configurations that are possible in the FSS evolution model of a peer-to-peer file-sharing network are described. Phase portraits of each configuration are presented. The impact of various administrative measures on FSS stability margin is analyzed. The ambiguity of the effect of the rating system on FSS stability is shown. The positive effects of a system of time bonuses, feedback, and absorption of FSSs are also shown.

The paper overviews the existing digital Russian-language thesauri and the methods of their automatic construction and application. The authors have analyzed the main characteristics of thesauri published in open access for scientific research, evaluated trends of their development, and their effectiveness in solving natural language processing tasks. Statistical and linguistic methods of thesaurus construction that allow automation of their development and reduce the labor costs of expert linguists have been studied. In particular, algorithms for extracting keywords and semantic thesaurus relations of all types have been considered and the quality of the thesauri generated with the use of these tools was assessed. To illustrate features of various methods of constructing thesaurus relations, the authors developed a combined method that fully automatically generates a specialized thesaurus based on a text corpus of a selected domain and several existing linguistic resources. The proposed method was used to conduct experiments on two Russian-language text corpora that represent two different domains: articles on migration and tweets. The resulting thesauri were analyzed by means of an integrated assessment that had been developed by the authors in a previous study and allows one to determine various aspects of the analyzed thesaurus and appraise the quality of the methods of its generation. The analysis revealed the main advantages and disadvantages of various approaches to thesaurus construction and extraction of semantic relations of different types, and also made it possible to identify potential focus areas for future research.

This paper considers environmental–economic models of optimal harvesting, given by impulsive differential equations, which depend on random parameters. We assume that lengths of intervals \({{\theta }_{k}}\) between the moments of impulses \({{\tau }_{k}}\) are random variables and the sizes of impulse influence depend on random parameters \({{{v}}_{k}},\)\(k = 1,2, \ldots \) One example of such objects is an impulsive equation that simulates dynamics of the population subject to harvesting. In the absence of harvesting, the population development is described by the differential equation \(\dot {x} = g(x),\) and in time points \({{\tau }_{k}}\) some random share of resource \({{{v}}_{k}},\)\(k = 1,2, \ldots \) is taken from the population. We can control the gathering process so that to stop harvesting when its share will appear big enough to save the biggest possible remaining resource to increase the size of the next gathering. Let the equation \(\dot {x} = g(x)\) have an asymptotic stable solution \(\varphi (t) \equiv K,\) whose attraction region is the interval \(({{K}_{1}},{{K}_{2}}),\) where \(0 \leqslant {{K}_{1}} < K < {{K}_{2}}.\) We construct the control \(u = ({{u}_{1}}, \ldots ,{{u}_{k}}, \ldots ),\) which limits a share of the harvested resource at each moment of time \({{\tau }_{k}}\) so that the quantity of the remaining resource, since some moment \({{\tau }_{{{{k}_{0}}}}},\) would be not less than the given value \(x \in ({{K}_{1}},K).\) For any \(x \in ({{K}_{1}},K)\) the estimates of the average temporal benefit, valid with the probability of one, are obtained. It is shown that there is a unique \(x* \in ({{K}_{1}},K),\) at which the lower estimate reaches the greatest value. Thus, we described the way of population control at which the value of the average time profit can be lower estimated with the probability of one by the greatest number whenever possible.

In 1978, Robert McEliece constructed the first asymmetric code-based cryptosystem using noise-immune Goppa codes; no effective key attacks has been described for it yet. By now, quite a lot of code-based cryptosystems are known; however, their cryptographic security is inferior to that of the classical McEliece cryptosystem. In connection with the development of quantum computing, code-based cryptosystems are considered as an alternative to number theoretical ones; therefore, the problem of seeking promising classes of codes to construct new secure code-based cryptosystems is relevant. For this purpose, noncommutative codes can be used, that is, ideals in group algebras \({{\mathbb{F}}_{q}}G\) over finite noncommutative groups \(G\). The security of cryptosystems based on codes induced by subgroup codes has been studied earlier. The Artin–Wedderburn theorem, which proves the existence of an isomorphism of a group algebra to the direct sum of matrix algebras, is important for studying noncommutative codes. However, the particular form of terms and the construction of the isomorphism are not specified by this theorem; thus, for each group, there remains the problem of constructing the Wedderburn representation. The complete Wedderburn decomposition for the group algebra \({{\mathbb{F}}_{q}}{{D}_{{2n}}}\) over the dihedral group \({{D}_{{2n}}}\) has been obtained by F.E. Brochero Martinez in the case when the cardinality of the field and the order of the group are relatively prime numbers. Using these results, we study codes in the group algebra \({{\mathbb{F}}_{q}}{{D}_{{2n}}}\) in this paper. The problem on the structure of all codes is solved, and the structure of codes induced by codes over cyclic subgroups of \({{D}_{{2n}}}\) is described, which is of interest for cryptographic applications.

In the modern world, the efficient use of energy is an extremely important aspect of human activity. In particular, heat supply systems have significant economic, environmental and social importance for both heat consumers and heat supply organizations. The economic status of all participants in the heat supply process depends on the efficiency of the functioning of the heat supply-systems. The reliability of the functioning of systems depends on vital processes such as the work of hospitals and industrial enterprises. With such a close network communication, reliable and efficient operation of power supply systems is critical. In this article, ways to improve the efficiency of heat supply systems are considered. A mathematical model for improved planning of heat supply systems by connecting the optimal set of new heat consumers is presented. For each single customer, when there is an alternative option for connecting this consumer to the existing heat network, it is possible to choose the only optimal solution. This becomes possible due to the restrictions and the procedure for selecting variants from a subset of binary variables corresponding to alternatives. The procedure for finding the optimal number of consumers for connection to the existing heat network is presented, which is the rationale for increasing the number of existing consumers of the heat network. The testing was carried out and the results of the mathematical model by an example of test heat networks are presented. Directions of further study of increasing the efficiency of heat supply systems and integrating the presented mathematical model with modern software complexes are determined.

Smart Building is a technology that is on the rise in developed countries. The idea behind it is that a smart building should be able to recognize a variety of situations in itself and respond accordingly. An automated building management system is set up to automate the controls and to coordinate the separate building engineering systems; the system comprises subsystems to automate this or that segment of the equipment. Mathematical modeling and computer simulation is necessary to study the various modes, in which the engineering subsystems and the system as a whole may operate. From the mathematical standpoint, a smart building is a continuous-discrete or hybrid system that comprises multiple coordinated components of varying nature that can be described as continuous or discrete processes. This paper proposes a smart building model that can simulate the functioning of the core engineering subsystems as well as the algorithms behind them. The model is based on Matlab Simulink and uses the Simscape physical modeling library as well as the Stateflow library. The model employs specialized control algorithms to coordinate subsystems and optimize power consumption.

The paper describes a mathematical model of trade flows between the territories of a region or a country in a transportation network having one or more different types of marine or ground transport. We use the approach of modeling complex communication systems to determine the most probable values of flows in case of incomplete information about the system. Transportation costs between the territories are modeled within the framework of the gravity model. The payment for transportation depends on the distance between regions, the distance is estimated as the shortest way length in a given transportation network or geographical distance. The mathematical formulation of the problem belongs to the class of convex mathematical programming problems and assumes the numerical solution of nonlinear optimization problem with linear constraints. Based on the model, the software is implemented as a cloud service on heterogeneous computing architectures: the simulation module is made on a high-performance server platform, management and visualization modules are produced with IACPaaS cloud platform. Communication between the platforms is established via asynchronous http-queries. For information exchange between the modules the declarative model with JSON format is developed and implemented for the objects considered in the mathematical model which are products, areas and communications. Visualization module allows to present graphically the original and the resulting matrix data and to modify the input parameters of the model interactively. The paper demonstrates the use of software for the simulation of interregional freight traffic of the Russian Far East region based on input data provided by open statistics sources.

In this paper an approach for the construction of nonlinear output tracking control on a finite time interval for a class of weakly nonlinear systems with state-dependent coefficients is considered. The proposed method of control synthesis consists of two main stages. On the first stage, a nonlinear state feedback regulator is constructed using a previously proposed control algorithm based on the State-Dependent Riccati Equation (SDRE). On the second stage, the problem of full-order observer construction is formulated and then is reduced to the differential game problem. The form of its solution is obtained with the help of the guaranteed (minimax) control principle, which allows to find the best observer coefficients with respect to a given functional considering the worst-case uncertainty realization. The form of the obtained equations made it possible to use the algorithm from the first stage to determine the observer matrix. The proposed approach is characterized by the nonapplicability of the estimation and control separation principle used for linear systems, since the matrix of observer coefficients turned out to be dependent on the feedback coefficients matrix. The use of numerical-analytical procedures for determination of observer and feedback coefficients matrices significantly reduces the computational complexity of the control algorithm.

In this paper a criteria of comparison of different tournament organization systems in sporting contests is offered; the criteria uses the probability of winning the fairly strongest player. Two probabilistic models have been analyzed. Calculating formulas for estimating the probability and probability density of score points gained by one or another player were obtained. Some really used tournament systems were analyzed with the stochastic modeling method. The available results also provide an order of objects presenting to experts while organizing the examination by paired comparison. An analytical estimation of probability of tournament results (or pared comparison) was obtained. In many cases it allows to avoid a time-consuming procedure of sorting out possible variants.