IDENTIFICATION OF ARGUMENTATIVE RELATIONS IN POPULAR SCIENCE TEXTS

The presented work describes the analysis of argumentative statements included into the same text topic fragment as a recognition feature in terms of its efficiency. This study is performed with the purpose of using this feature in automatic recognition of argumentative structures presented in the popular science texts written in Russian. The topic model of a text is constructed based on superphrasal units (text fragments united by one topic) that are identified by detecting clusters of words and word-combinations with the use of scan statistics. Potential relations, extracted from topic models, are verified through the use of texts with manually annotated argumentation structures. The comparison between potential (based on topic models) and manually constructed relations is performed automatically. Macro-average scores of precision and recall are equal to 48.6% and 76.2% correspondingly.

SOME EXPERIMENTS ON THE CONSTRUCTION AND ANALYSIS OF THE DE BRUIJN GRAPH

This paper describes the experience of solving the problem of finding chains in the De Bruijn graph using parallel computations and distributed data storage.

VERIFICATION OF A PREDICATE HEAPSORT PROGRAM USING INVERSE TRANSFORMATIONS

Deductive verification of the classical J.Williams heapsort algorithm for objects of an arbitrary type was conducted. In order to simplify verification, non-trivial transformations, replacing pointer arithmetic operators by an array element constructs, were applied. The program was translated to the predicate programming language. Deductive verification of the program in the tools Why3 and Coq appears to be complicated and time consuming.

TRANSFORMATION, SPECIFICATION, AND VERIFICATION OF THE PROGRAM CALCULATING THE ELEMENTS NUMBER OF A SET PRESENTED BY A BIT VECTOR

Transformations eliminating pointers in the memweight function in OS Linux kernel library is described. Next, the function is translated to the predicate programming language P. For the obtained predicate program, deductive verification in the Why3 tool was performed. In order to simplify verification, the program model of calculating program inner state was constructed.

ON SOME PROPERTIES OF TIMED FINITE STATE MACHINES

Sequential reactive systems are formal models of programs that interact with the environment by receiving inputs and producing corresponding outputs. Such formal models are widely used in software engineering, computational linguistics, telecommunication, etc. In real life, the behavior of a reactive system depends not only on the flow of input data, but also on the time the input data arrive and the delays that occur when generating responses. To capture these aspects, a timed finite state machine (TFSM) is used as a formal model of a real-time sequential reactive system. However, in most of known previous works, this model was considered in simplified semantics: the responses in the output stream, regardless of their timestamps, follow in the same order in which the corresponding inputs are delivered to the machine. This simplification makes the model easier to analyze and manipulate, but it misses many important aspects of real-time computation. In this paper we study a refined semantics of TFSMs and show how to represent it by means of Labelled Transition Systems. This opens up a possibility to apply traditional formal methods for verifying more subtle properties of real-time reactive behavior which were previously ignored.

VERIFICATION OF A STRING TO INTEGER CONVERSION PROGRAM

Deductive verification of a string to integer conversion program kstrtoul in Linux OS kernel library is described. The kstrtoul program calculates the integer value presented as a char sequence of digits. To simplify program verification the transformations of replacing pointer operators to equivalent actions without pointers are conducted. Model of inner program state are constructed to enhance program specification. Deductive verification was conducted in the tools Why3 and Coq.

ADAPTIVITY ISSUES IN INTELLIGENT E-LEARNING TUTORING SYSTEMS

This paper considers the problems of adaptivity realization in intelligent e-learning tutoring systems, based on adaptive hypermedia technologies and individual learning styles models.

NAMED ENTITY RECOGNITION IN TEXTS OF ADMINISTRATIVE DOCUMENTS WITH DEEP NEURAL NETWORKS

Named Entity Extraction (NER) is the task of extracting information from text data that belongs to predefined categories, such as organizations names, place names, people's names, etc. Within the framework of the presented work, was developed an approach for the additional training of deep neural networks with the attention mechanism (BERT architecture). It is shown that the preliminary training of the language model in the tasks of recovering the masked word and determining the semantic relatedness of two sentences can significantly improve the quality of solving the problem of NER. One of the best results has been achieved in the task of extracting named entities on the RuREBus dataset. One of the key features of the described solution is the closeness of the formulation to real business problems and the selection of entities not of a general nature, but specific to the economic industry.

USING AN EXTENSIONS OF CTL* FOR SPECIFICATION AND VERIFICATION OF SEQUENTIAL REACTIVE SYSTEMS

Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop over time, temporal logics, obviously, could be used as both simple and expressive formalism for specifying the behavior of sequential reactive systems. However, the conventional applied temporal logics (LTL, CTL) do not suit this purpose well, since their formulae are interpreted over omega-languages, whereas the behavior of transducers are represented by binary relations on infinite sequences, i.e. omega-transductions. To provide temporal logic with the ability to take into account this general feature of the behavior of reactive systems, we introduced new extensions of this logic. Two distinguished features characterize these extension: 1) temporal operators are parameterized by sets of streams (languages) admissible for input, and 2) sets (languages) of expected output streams are used as basic predicates. In the previous series of works we studied the expressive power and the model checking problem for Reg-LTL and Reg-CTL which are such extensions of LTL and CTL where the languages mentioned above are regular ones. We discovered that such an extension of temporal logics increases their expressive capability though retains the decidability of the model checking problem. Our next step in the systematic study of expressive and algorithmic properties of new extensions temporal logics is the analysis of the model checking problem for finite state transducers against Reg-CTL* formulae. In this paper we develop a model checking algorithm for Reg-CTL* and show that this problem is in ExpSpace.

DERIVING HOMING SEQUENCES FOR FINITE STATE MACHINES WITH TIMED GUARDS

State identification is the well-known problem in the theory of Finite State Machines (FSM) where homing sequences (HS) are used for the identification of a current FSM state, and this fact is widely used in the area of software testing and verification. For various kinds of FSMs, there exist sufficient and necessary conditions for the existence of preset and adaptive HS and algorithms for their derivation. Nowadays timed aspects become very important for hardware and software systems. In this work, we address the problem of checking the existence and derivation of homing sequences for FSMs with timed guards. The investigation is based on the FSM abstraction of a Timed FSM.