Computer System Organization
Theory of Software
The article continues the series of works on development and verification of control programs based on LTL-specifications of a special type. Previously, it was proposed a declarative LTL-specification, which allows describing the behavior of control programs and building program code based on it in the imperative ST-language for programmable logic controllers. The LTL-specification can be directly verified for compliance with specified temporal properties by the model checking method using the nuXmv symbolic verification tool. In general, it is not required translating LTL-formulas of the specification into another formalism — an SMV-specification (code in the input language of the nuXmv tool). The purpose of this work is to explore alternative ways of representing a program behavior model corresponding to the declarative LTL-specification during its verification within the nuXmv tool. In the article, we transform the declarative LTL-specification into various SMV-specifications with accompanying changes of formulation of the verification problem, what leads to a significant reduction in time costs when checking temporal properties by using the nuXmv tool. The acceleration of verification is due to the reduction of the state space of a model being verified. The SMV-specifications obtained as a result of the proposed transformations specify identical or bisimulationally equivalent transition systems. It is ensuring the same verification results when replacing one SMV-specification with another.
Artificial Intelligence
The availability of unmanned aerial vehicles (UAVs) has led to a significant increase in the number of offenses involving their use. This makes the development of UAV detection systems relevant. Solutions based on deep neural networks show the best results in detecting UAVs on video. This article presents a study of various neural network detectors and focuses on identifying objects as small as possible, up to the size of $4\times4$ and even $3\times3$ pixels. The work investigates architectures SSD (VGG16) and YOLOv3 and it's modifications. Precision and recall metrics are calculated separately for different intervals of the object areas. The best result have been shown by YOLOv3 model with bbox parameters chosen as the result of object sizes clustering. Small ($3\times3$ px) drones have been successfully identified with 76% precision and a very small recall of 26%. For objects between 10 and 20 pixels in area, the recall is 64% with an accuracy of 75%. For objects with an area more than 20px the recall is about 90%, the precision is 89%, and the F1 score is 90%. These results show that it is possible to recognize even $4\times4$ pixel drones, which can be used in video surveillance systems.
The paper presents the results of a study of modern text models in order to identify, on their basis, the semantic similarity of English-language texts. The task of determining semantic similarity of texts is an important component of many areas of natural language processing: machine translation, information retrieval, question and answer systems, artificial intelligence in education. The authors solved the problem of classifying the proximity of student answers to the teacher’s standard answer. The neural network language models BERT and GPT, previously used to determine the semantic similarity of texts, the new neural network model Mamba, as well as stylometric features of the text were chosen for the study. Experiments were carried out with two text corpora: the Text Similarity corpus from open sources and the custom corpus, collected with the help of philologists. The quality of the problem solution was assessed by precision, recall, and F-measure. All neural network language models showed a similar F-measure quality of about 86% for the larger Text Similarity corpus and 50–56% for the custom corpus. A completely new result was the successful application of the Mamba model. However, the most interesting achievement was the use of vectors of stylometric features of the text, which showed 80% F-measure for the custom corpus and the same quality of problem solving as neural network models for another corpus.
Computing Methodologies and Applications
Traffic safety in railway transport requires regular inspection of the rail condition to identify and timely eliminate defects. Eddy current flaw detection is one of the popular methods of non-destructive rail testing. The data (defectograms) obtained from eddy current flaw detectors during rail testing are produced in large volume and therefore need in efficient automatic analysis. The analysis means the process of detecting on defectograms the presence of defective areas and identification of structural elements of the rail track, taking into account noise and possible interferences of various natures. The threshold noise level is found to isolate signals from defects and structural elements. Its value can be distorted by electromagnetic influences superimposed on the signals, which have pronounced low frequency and periodicity. This interferences raises the threshold noise level, complicating to detect useful signals. In this regard, there is a need to suppress the effects of the described type. Therefore, there is a need for described interferences reduction. In this paper spectral subtraction was used as a method for interference reduction on eddy current defectograms. The interference function was defined as the sum of the low-frequency harmonics of the Discrete Fourier Transform of the original signal. Then the interference-free signal can be found by subtracting of low-frequency range harmonics. The right boundary of this range was called the threshold harmonic frequency. It was found minimizing the distance of the signal's autocorrelation function and expected autocorrelation. For it two kinds were proposed: the noise autocorrelation and the reference autocorrelation. Both approaches allow to determine the threshold harmonic frequency so that periodic interferences will be best reduced. The based on the Gaussian noise autocorrelation method is somewhat universal for eddy current defectograms. Whereas the based on reference autocorrelation method depends on specific data and recording equipment. For the eddy current defectogram data under consideration, the most suitable threshold harmonic frequency was found. The described approaches to periodic low-frequency interference reduction, in addition to eddy current testing, can be successfully used for other areas.
Algorithms in Computer Science
The individual-based model describes the dynamics of genetic diversity of a population scattered on a spatial continuum in the case of a finite number of individuals. During extinction events in a certain area, a portion of the population dies, after which new individuals with the genotype of the parent are born during recolonization event. In this paper we examine the model, as well as its modification, and derive properties related to population parameters. The study demonstrates that the lifespan of individuals follows an exponential distribution, allele probabilities remain constant over time, and the average heterozygosity, constrained by the number of individuals during extinction and recolonization, equals a similar quantity in the Moran model. The joint distribution of alleles is generalized for populations continuously scattered in space. Joint allele distribution and heterozygosity are computed through simulations.
ISSN 2313-5417 (Online)





