Process-oriented programming is one of the approaches to developing control software. A process-oriented program is defined as a sequence of processes. Each process is represented by a set of named states containing program code that define the logic of the process's behavior. Program execution is sequential execution of each of these processes in their current states at every iteration of the control cycle. Processes can interact through changing each other's states and shared variables.

The paper expands a method for classifying temporal requirements for process-oriented programs in order to simplify and automate the deductive verification of such programs. The method consists of the following steps. At the first step, the requirements are formalized in a specialized language DV-TRL, a variant of typed first-order predicate logic with a set of interpreted types and predicate and functional symbols, that reflect specific concepts of control systems in a process-oriented paradigm. At the second step, the formalized requirements are divided into classes, each of which is defined by a pattern — a parametric formula of the DV-TRL language. The correctness conditions generated for process-oriented programs regarding requirements satisfying the same pattern have the same proof scheme. At the third step, appropriate proof schemes are developed.
In our paper, we first give a brief introduction to the poST language, a process-oriented extension to the ST language of the IEC 61131-3 standard. Next, the DV-TRL language is defined. We also provide a collection of natural language requirements for several control systems. Then we define patterns that fully cover all the requirements of this collection. For each of these patterns we give an example of a formalized requirement from the collection and describe a scheme for proving the correctness conditions for this pattern. Statistics on the distribution of requirements from the collection across patterns reveals the most popular patterns. We also analyzed related works.

The process-oriented programming is a paradigm based on the process concept where each process is a concurrent finite state machine inside. The paradigm is intended for PLC (programmable logic controllers) developers to write Industry 4.0-enabled software. The poST language is a promising process-oriented extension of the IEC 61131-3 Structured Text (ST) language designed to provide a conceptual consistency of the PLC source code with technological description of the process under control. This language combines the advantages of FSM-based programming with the standard syntax of the ST language. We propose transformational semantics of poST providing rules for translation of poST language statements to Promela — the input language of the SPIN model checker. Following these semantic rules, our Xtext-based translator outputs a Promela model for the poST program. Our contribution is the poST transformational semantics and the method for automatic generation of the Promela code from poST control programs. The resulting Promela program is ready to be verified with SPIN model checker against linear temporal logic requirements to the source poST program.

In the paper we provide an overview of related work, as well as a brief description of the poST and Promela languages. Further, the Promela poST translation rules cover control flow statements, process creation and state management constructs, and timeout management. Then we define service processes for modeling the external environment and managing high-level LTL specifications. Then we present the main ideas of implementing the translator poST to Promela. We also illustrate our approach using the example of a system for managing electricity consumption and production, including renewable sources.

The article is devoted to the development of an approach to solving the main problems of the theory of supervisory control of logical discrete-event systems (DES), based on their representation in the form of positively constructed formulas (PCF). We consider logical DESs in automata form, understood as generators of some regular languages. The PCF language is a complete first-order language, the formulas of which have a regular structure of alternating type quantifiers and do not contain a negation operator in the syntax. It was previously proven that any formula of the classical first-order predicate calculus can be represented as a PCF. PCFs have a visual tree representation and a natural question-and-answer procedure for searching for an inference using a single inference rule. It is shown how the PCF calculus, developed in the 1990s to solve some problems of control of dynamic systems, makes it possible to solve basic problems of the theory of supervisory control, such as checking the criteria for the existence of supervisory control, automatically modifying restrictions on the behavior of the controlled system, and implementing a supervisor. Due to some features of the PCF calculus, it is possible to use a non-monotonic inference. It is demonstrated how the presented PCF-based method allows for additional event processing during inference. The Bootfrost software system, or the so-called prover, designed to refute the obtained PCFs is also presented, and the features of its implementation are briefly described. As an illustrative example, we consider the problem of controlling an autonomous mobile robot.

The paper discusses the theory and algorithms necessary to construct a minimal covering of generalized typed inclusion dependencies. Traditionally, the construction of minimal covering is used for all types of dependencies in order to obtain a non-redundant and consistent database design. Generalized inclusion dependencies correspond to referential integrity constraints, when several main and several external relations are involved in one constraint, which corresponds to an ultragraph edge. In previous work, based on a study of the properties of dependencies, a system of axioms was presented with proof of consistency and completeness. In this work, the closures were studied for generalized typed inclusion dependencies. An algorithm for constructing closures has been developed and its correctness has been proven. The results obtained are further used to develop an algorithm for constructing a minimal covering. At the end of the article, examples are presented that demonstrate the operation of the algorithms.

The paper examines automatic methods for classifying Russian-language sentences into two classes: ironic and non-ironic. The discussed methods can be divided into three categories: classifiers based on language model embeddings, classifiers using sentiment information, and classifiers with embeddings trained to detect irony. The components of classifiers are neural networks such as BERT, RoBERTa, BiLSTM, CNN, as well as an attention mechanism and fully connected layers. The irony detection experiments were carried out using two corpora of Russian sentences: the first corpus is composed of journalistic texts from the OpenCorpora open corpus, the second corpus is an extension of the first one and is supplemented with ironic sentences from the Wiktionary resource.

The best results were demonstrated by a group of classifiers based on embeddings of language models with the maximum F-measure of 0.84, achieved by a combination of RoBERTa, BiLSTM, an attention mechanism and a pair of fully connected layers in experiments on the extended corpus. In general, using the extended corpus produced results that were 2–5% higher than those of the basic corpus. The achieved results are the best for the problem under consideration in the case of the Russian language and are comparable to the best one for English.

In this paper, we study undirected multiple graphs of any natural multiplicity $k>1$. There are edges of three types: ordinary edges, multiple edges and multi-edges. Each edge of the last two types is a union of $k$ linked edges, which connect 2 or $(k+1)$ vertices, correspondingly. The linked edges should be used simultaneously. If a vertex is incident to a multiple edge, it can be also incident to other multiple edges and it can be the common end of $k$ linked edges of some multi-edge. If a vertex is the common end of some multi-edge, it cannot be the common end of another multi-edge.

We study the problem of finding the Eulerian walk (the cycle or the trail) in a multiple graph, which generalizes the classical problem for an ordinary graph. We prove that the recognition variant of the multiple eulerian walk problem is NP-complete. For this purpose we first prove NP-completeness of the auxiliary problem of recognising the covering trails with given endpoints in an ordinary graph.