This paper discusses the construction of a formal executable operational semantics for Reflex, a process-oriented programming language designed for embedded and distributed microcontroller systems. The work is motivated by the need to improve the reliability of software in such systems, and also by the fact that earlier formal descriptions of Reflex were based on an outdated version of the language and were not executable, which limited their use for automated verification and for building correct tooling. The paper provides basic information about the language and the ABML notation used to formalize the semantic model. The main focus is on building an ontological model of Reflex that describes constants, identifiers, data types, expressions, operators, and declarators as ABML types. This ontology defines the static structure of a valid program and serves as a foundation for further model execution, as well as for formal analysis of syntactic and semantic correctness of program constructs. A separate section discusses the limitations of the proposed semantics. We clarify the assumptions made, including the lack of modeling for interrupts, node concurrency, physical variables, and C embeddings. We describe the preprocessing steps for ontological models: name resolution, detection of implicit type conversions, and normalization of language constructs. These transformations help unify the internal representation of programs and prepare them for formal execution. The paper also formalizes the operational semantics of Reflex using an agent-based model and attribute closures. We define the structure of agents responsible for evaluating models, as well as the environment that stores global static information for the agents and determines the evaluation order. The results provide a formal foundation for further development of deductive verification tools, static analysis, and a verified compiler for the Reflex language.
We consider a boundary value problem for the logistic equation with delay and diffusion modeling population dynamics in a one-dimensional habitat. A homogeneous Neumann condition is imposed at one endpoint, while at the other the flux is proportional to the delayed deviation of the density from equilibrium, the delay $\delta$ modeling a lagged migration response. We study how $\delta$ affects the local stability of the equilibrium and the type of stability loss. A linear stability analysis is performed; the stability boundaries in the $(\gamma,r)$ parameter plane are computed by parameter continuation. For $\gamma>0$, stability can be lost either through a simple zero root of the characteristic equation (steady-state bifurcation) or through a pair of purely imaginary roots (oscillatory instability); for $\gamma\le0$, only the oscillatory scenario occurs. The steady-state boundary is shown to be independent of $\delta$. The stability region expands considerably as $\delta$ approaches 0.5: for suitably chosen parameters, the equilibrium remains stable for $r$ far exceeding the threshold $\pi/2$ of the case $\gamma=0$. Nevertheless, this expansion is bounded: for $d=1$ the supremum $r_*\approx7.6714$ is approached, but not attained, at a unique point $(\delta_*,\gamma_*)\approx(0.4792, 2.6314)$ where the characteristic equation has three pairs of purely imaginary roots. Existence and uniqueness of this point are proved rigorously using interval arithmetic. Thus, a moderate migration lag can offset the destabilizing effect of rapid reproduction, but only up to a limit. The results are confirmed by numerical simulations based on the method of lines and an explicit sixth-order Runge-Kutta scheme.
Object-centric process mining has emerged as a powerful paradigm for analyzing event data involving multiple interacting business objects. Existing discovery techniques often rely on object-centric Petri nets with fixed arc multiplicities, limiting their ability to represent parametric resource consumption and production patterns and to capture quantitative dependencies between interacting object types. In this paper, we introduce a discovery approach for object-centric Petri nets with parametric arcs. The proposed method synthesizes models from object-centric event logs while identifying variable-weight behavioral patterns. It first discovers control-flow behavior for individual object types and combines the resulting models into an object-centric structure. Subsequently, the numbers of objects participating in events of the same activity are analyzed in order to identify recurring quantitative relations between object types. These relations are represented by constants or linear expressions and are assigned as arc weights in the resulting model. We formalize the underlying model, present the discovery algorithm, and prove that, under the stated assumptions on the discovered per-object-type models, the resulting net can perfectly replay the observed multi-object traces. We further evaluate the applicability of the approach on representative real-world and synthetic object-centric event logs. The evaluation demonstrates that the proposed approach can replace unspecified variable multiplicities with explicit parametric relations while preserving the observed behavior represented by the discovered model. The resulting object-centric Petri nets provide a more compact and expressive representation of object-centric processes and make quantitative synchronization patterns between interacting object types explicit.
This paper addresses the technology of model-based program synthesis. The required program properties, according to which a behavior model is developed, are specified in the language of temporal logic. Verification of model compliance with specified properties is carried out by model checking. A program synthesized from a formally verified model inherits all its temporal properties. The program behavior model may be inconsistent with the verified properties if their formalization incorporates erroneous assumptions about the model. Modifying the model for consistency complicates the synthesis procedure, since the adapted model describes a behavior that differs from the program's behavior. To resolve this problem, the present study proposes the application of the Decorator design pattern. The synthesis-oriented model is a decorated object. The property-adapted model is a decorator object that encapsulates the decorated object and modifies its behavior on the fly, accounting for the specifics of the properties being verified. The Decorator pattern allows for adapting the original model to the verified properties without modifying its source structure. To change the behavior for a specific set of properties, only the decorator object needs to be developed, while the decorated object remains unchanged and is directly used for program synthesis. The results of this work are demonstrated through the development and verification of a secure escrow protocol. Computation Tree Logic (CTL) is used to specify the protocol properties. The protocol model is represented as a finite automaton. Implemented as a decorator, the model adapted for CTL properties reproduces intermediate states missing from the finite automaton. The decorator and the decorated object are implemented as modules of the nuXmv model checker. The verified protocol specification is translated into a Java class, which serves as a trusted module in developing a secure escrow-based transaction web service.
The problem of decoding multidimensional time series with high variance and strong covariance between components is considered. Previously proposed prediction methods do not account for the spatial structure of time series. It is proposed to model this structure using graph-based methods, such as graph neural diffusion — a generalization of graph neural networks obtained by solving an anisotropic diffusion equation discretized on a graph. In this work, a model for multidimensional time-series prediction based on the combination of graph neural diffusion and Riemannian geometry of covariance representations is proposed. In the Euclidean domain, diffusion on a graph of signal components is used to analyze correlation dependencies between the components of the series. Simultaneously, on the Riemannian manifold of positive semidefinite matrices, a graph of covariance matrices corresponding to different temporal windows is constructed. Representations on a Riemannian manifold are invariant to linear transformations of time series components and are robust to noise; these properties enable the use of the Riemannian manifold to derive informative features for time series forecasting. Diffusion on this graph is performed in the tangent space of the manifold using logarithmic and exponential mappings. Predictions obtained in both domains are summed in the original space, and model training is performed using a consistency-based loss function. The proposed approach simultaneously captures local temporal dynamics and global inter-component dependencies. Computational experiments on multidimensional EEG data demonstrate improved prediction accuracy compared to autoregressive methods.
The problem of sparse identification of non-linear dynamics is considered. The problem is motivated by the need for interpretable mathematical models in the natural sciences, where the fundamental laws of evolution are either unknown or known only partially. The T‑SINDy method is proposed, which combines time delay embedding, tensor representations, and sparse regression. In contrast to the classical SINDy approach, in which the number of parameters grows exponentially with the number of candidate functions, the proposed tensor map enables parameterization of all possible nonlinear interactions. To reduce computational complexity, canonical decomposition of rank R is used, reducing the number of parameter. Sparsity of the model is achieved through a two‑stage procedure: thresholding of the factor‑matrix elements followed by fine‑tuning of the nonzero coefficients, and then additional truncation of small entries in the unfolded parameter tensor. Computational experiments are performed on the Lorenz system (with two of three variables observed) and on the normal form of the Hopf bifurcation (with a single observed variable) under noise levels ranging from 0 to 10%. It is demonstrated that T‑SINDy provides prediction accuracy comparable to that of the classical SINDy method while reducing training time. The reconstructed equations retain interpretability, explicitly expressing the dynamics in terms of the original variables, which constitutes a distinct advantage over neural‑network‑based methods. The proposed approach offers an efficient and interpretable alternative for the identification of dynamical systems from incomplete, noisy observations.
The paper addresses the task of automatic topic classification of texts in the Tatar language, a low-resource language with rich agglutinative morphology. In the era of rapid development of large language models (LLMs), one of the key methodological challenges is the creation of open corpora, tokenizers, and annotated datasets, which are essential for both effective fine-tuning of modern neural architectures and objective evaluation of their performance. The development of such resources and the establishment of reproducible benchmarks remain an important scientific objective regardless of evolving technological paradigms. This study aims to develop an open resource base for Tatar natural language processing and to validate it experimentally in the task of topic classification. The paper presents and evaluates a set of newly developed resources, including the TatCorp 222M corpus (222 million tokens), the TatarTokenizers toolkit, the Tatar2Vec pre-trained embedding models (FastText, Word2Vec, and CBOW), and a manually annotated dataset containing 13,160 texts from ten thematic categories. The embedding models were trained on the TatCorp 222M corpus and selected from 57 configurations using a proposed composite evaluation metric. A systematic comparison of five text representation methods, including the Tatar2Vec embeddings, TF-IDF, and Bag of Words, combined with seven classification algorithms ranging from linear models and ensemble methods to multilayer perceptrons, was conducted. In addition, the influence of BPE-based subword tokenization on topic classification performance was investigated. The highest Macro $F_1$-score (0.7789) was achieved by combining pre-trained Word2Vec embeddings (without subword tokenization) with a multilayer perceptron (MLP), while a comparable Macro $F_1$-score (0.7760) and the highest ROC AUC (0.9683) were obtained using Bag of Words with XGBoost. The experiments demonstrate that BPE subword tokenization does not improve, but consistently degrades, topic classification performance for an agglutinative language (Macro $F_1$ is reduced by the amount up to 0.0234). The developed open resources and reproducible benchmarks provide a foundation for future comparative studies, including the evaluation of transformer-based models for Tatar and other low-resource Turkic languages.
This paper addresses the problem of reliability assessment for a tethered high-altitude unmanned telecommunication platform using the risk tree analysis method. The aim of the study is to develop and test a methodology for the quantitative estimation of the probability of risk events and the associated material damage during long-term platform operation. A disruption in the provision of broadband wireless communication services by the platform is considered as the resulting risk event. A detailed technical description of the tethered platform “Albatros" is provided, which serves as the basis for identifying risk events. The general theory and methodology for constructing and analyzing a risk tree are presented, including the parameterization of the model with probabilistic and cost characteristics. Using the tethered high-altitude unmanned telecommunication platform as a case study, a comprehensive numerical investigation is carried out. Within this investigation, a sensitivity analysis of key output indicators — namely, the reliability function, quantiles, mean time to failure, and expected damage — is conducted with respect to the statistical properties of failure times, specifically the coefficient of variation and the distribution shape.The practical conclusions derived from the study demonstrate that the use of adequate probabilistic models (as opposed to simplified exponential ones) is critical for obtaining realistic forecasts. The most dangerous risk evolution scenarios are identified, and the contribution of factors influencing the occurrence of these events is quantitatively assessed. The proposed methodology is universal and can be applied to a wide range of complex technical systems, including other tethered platforms whose architectures allow decomposition into key components with established logical relationships between their failures. The obtained results can be used for the evidence-based design of such systems, the planning of scheduled maintenance, and the optimization of technical support strategies.
Declarative process models are widely used in process mining to describe flexible process behavior through sets of constraints. However, models discovered automatically from event logs may contain inconsistent constraints, which can make them difficult to interpret and unusable for execution, conformance checking, or further analysis. Existing methods for consistency analysis either rely on automata-based constructions with high worst-case time complexity or use heuristics based on MIS (minimal inconsistent subsets) that do not provide a full formal characterization of the inconsistency patterns they detect. In this paper, we propose a graph-based approach to the inconsistency analysis for a restricted fragment of Declare process modeling language. We represent dependencies between constraints through the task entailment graph and characterize inconsistency by means of three structural witness types. Based on this characterization, we first detect candidate inconsistent subsets and then verify whether a candidate is a minimal inconsistent subset by dedicated verification procedures. In contrast to automata-based approaches, the proposed method avoids explicit automata products and relies instead on graph-based analysis and constructive trace arguments. We implement the proposed approach and evaluate it on real-life event logs, showing that it is practically feasible and achieves competitive runtime.
This paper studies the problem of ranking SQL query execution plans by execution time. We propose a method in which structural encoding of the plan tree is replaced with a textual description of the plan, which is then converted into a vector representation using a vector representation model. A compact prediction model is trained on top of this representation and used to rank plans. Three approaches are compared: the prediction model from Bao, which relies on structural encoding of the plan tree, the cost estimate produced by the PostgreSQL optimizer, and the proposed method based on textual plan descriptions and vector representation models. In addition, several vector representation models and two variants of textual plan description are investigated: the raw plan text and a normalized description. Experiments are conducted on the CEB benchmark built on IMDb data under two evaluation settings: random splits and query-template splits. Quality is evaluated using pairwise accuracy and Spearman correlation. The results show that under random splits, the best configuration based on jina-code-embeddings-0.5b outperforms both the Bao model and the optimizer cost estimate on both ranking metrics. For all considered models, the raw textual plan description is more informative than the normalization scheme used in this work. Under query-template splits, the quality of all learned approaches decreases; in this setting, the best model based on vector representations and the Bao model remain comparable to each other, but both are outperformed by the optimizer cost estimate. These results indicate that textual plan descriptions and vector representation models can serve as a basis for predictive plan-ranking methods, although robust generalization to previously unseen query templates remains an open problem.
The dynamics of large non-periodic chains with advective connections between elements is considered. The main assumption is that the number $N$ of chain elements is sufficiently large, so a small parameter $\varepsilon=N^{-1}$ naturally arises. This assumption allows us to move from a system of $N$ delayed equations to the study of a spatially distributed integro-differential equation containing a small parameter and use asymptotic methods to investigate the dynamic properties of this equation. The connections between the chain elements are a difference approximation of the advection operator, which is why they are called advective. Another assumption is that the chains are not circular, i.e., the boundary conditions for the systems under consideration do not have periodic properties. Non-classical boundary conditions are considered, which lead to the emergence of new dynamic effects. Critical cases in the problem of equilibrium stability are identified, and it is shown that they have infinite dimension in the sense that an infinite number of roots of the characteristic equation approach the imaginary axis as a small parameter approaches zero. In this situation, the known research methods based on the use of invariant integral manifolds and normal forms are not directly applicable. We use methods of quasi-normal forms, whose non-local dynamics determine the local behavior of the solutions of the considered chains. The main results consist in constructing quasi-normal forms using special asymptotic methods. This allows us to obtain the main approximations of the solutions of the original chain with respect to the parameter $\varepsilon$.
This article addresses the problem of mathematical modeling of square wave noise in electromagnetic signals, particularly in eddy current defectograms, to generate high-quality synthetic samples for training machine learning algorithms to detect and suppress square wave noise in data. A comprehensive study of naive models is conducted: a deterministic square wave signal, a square wave signal with white noise, and a telegraph process with white noise. The telegraph process with white noise serves as the central object of the study. For this model, stationary characteristics are analytically derived: the limiting probability density function and the autocorrelation function. To estimate the model parameters, a fully Bayesian approach is proposed and implemented for the first time, utilizing Gibbs sampling and the Forward Filtering Backward Sampling (FFBS) algorithm to efficiently marginalize the hidden Markov states. The parameter estimation algorithm converges rapidly, reaching an overall variance of $1e{-}6$ value by the 1500th iteration. It is established that classical models possess fundamental limitations due to the unrealistic assumption of a strictly constant period and duty cycle. It is shown that while the telegraph process resolves the issue of stochastic pulse durations, ignoring the continuity of transition fronts leads to a mathematical artifact — a shift in the modes of the theoretical limiting distribution compared to the empirical one. Furthermore, it is demonstrated that the absence of a low-pass filtering mechanism deprives the model's autocorrelation function of its characteristic oscillating component. The experimental confirmation of the significance of these factors justifies the direction for further research: the development of modified stochastic models integrating smooth state-switching mechanisms for the adequate simulation of square wave noise. Eddy current rail defectograms served as the empirical base for testing the models. Nevertheless, the developed mathematical framework can be successfully applied to model square wave noise in other types of electromagnetic signals, such as in ECG and magnetotelluric sounding.
A critical factor in ensuring the quality of software written in current and next-generation programming languages is the ability to rely on a formal operational semantics of the language. This gives developers a systematic, well-founded way to address reliability, performance, and security in the target software. We introduce a new formal framework where operational semantics can be developed and used not as a traditional non-executable abstract system, but as runnable code. That brings several advantages: easier modification, the ability to run across different execution environments, testing and debugging, version control, and more. We illustrate our approach using a practically relevant subset of the widely used C programming language. The strengths of our semantics framework are demonstrated by comparing it against the most popular current approaches across a set of practically relevant criteria. The paper presents the Attribute-Based Modeling Language (ABML) — a new domain-specific language designed for ontological modeling of programs and for defining their operational semantics in executable form. We describe the proposed method for building executable operational semantics with ABML. A worked example shows how our approach applies to a practically relevant subset of C. We then build an enriched ontology of C by adding semantic attributes, define algorithms for computing those attributes in ABML, and discuss how the enriched ontology influences the development of operational semantics. A detailed review of related work lets us compare our approach to state-of-the-art frameworks in terms of meeting current requirements for operational semantics development.
Process-oriented programming is an approach to developing control software where a program is structured as a set of processes. PoST is a process-oriented extension of ST language from the IEC 61131-3 standard. Since control systems often have high reliability requirements, formal verification of their software plays an important role. One formal verification method is deductive verification, which involves building a formal specification, generating verification conditions, and proving them. We use the Isabelle/HOL theorem prover for the proof step. Only the generation of verification conditions is fully automated. Deductive verification itself is labor-intensive, so automating it as much as possible is desirable. Control software involves temporal requirements, which in deductive verification of process-oriented programs are expressed as control loop invariants. However, these requirements are insufficient invariants, making it necessary to introduce extra invariants that carry auxiliary information about the program. An earlier approach to proving verification conditions used patterns for both the requirements and the extra invariants, with pattern-specific lemmas satisfying predefined schemas used in the proofs. This paper looks at automating the proof of both the verification conditions and the lemmas used in those proofs. We describe the previously proposed approach to automating deductive verification and give an introduction to Isabelle/HOL. Revised schemas for patterns and lemmas are presented, along with an algorithm for generating lemma proofs. We discuss the implementation of this algorithm and of the previously developed algorithm for generating verification condition proofs. The proposed approach is demonstrated with an example. A review of related work is provided.
The study of various processes leads to the need to clarify (expand) the boundaries of the applicability of computational structures and modeling tools. The purpose of this article is to develop the Taylor expansion for functions of several variables based on the concept of $S$-differentiability. A function $f$ from $L_1[Q_0]$, where $Q_0$ is an $m$-dimensional cube, is called $S$-differentiable at an interior point $x_0$ of this cube, if there exists an algebraic if there exists an analgebraic polynomial $P(x)$ of degree not greater than first for which it is uniform over all vectors $v$ of the unit sphere ${\mathbb R}^m$ the integral of $t$ within $0$ and $h$ from the expression $f(x_0 + t \cdot v)-P(t \cdot v)$ is $o(h^2)$ for $h \to 0{+}$. It is shown that with this definition, differentiation of a composite function with a linear interior component is valid, and the vector-gradient principle holds. The following result is proved. Let the function $f$ have continuous partial derivatives up to order $n$ inclusive in some neighborhood of the interior point $x_0 \in Q_0$ that are $S$-differentiable at the point $x_0$, then the Taylor expansion the function $f$ with accuracy $o\big(\Vert x - x_0\Vert^{n + 1}\big)$ holds in this neighborhood.
The logistic equation with delay and diffusion, which is important in mathematical ecology, is considered. It is assumed that the boundary conditions at one end of the interval [0,1] contain a parameter. The question of local — in the neighborhood of the equilibrium state — dynamics of the corresponding boundary value problem for all values of the boundary condition parameters is investigated. Critical cases in the problem of stability of the equilibrium state are identified and normal forms — scalar complex ordinary differential equations of the first order — are constructed. Their nonlocal dynamics determine the behavior of solutions of the original problem in a small neighborhood of the equilibrium state.
The development of high-quality tools for automatic determination of text levels according to the CEFR scale allows creating educational and testing materials more quickly and objectively. In this paper, the authors examine two types of modern text models: linguistic characteristics and embeddings of large language models for the task of classifying Russian-language texts by six CEFR levels: A1-C2 and three broader categories A, B, C. The two types of models explicitly represent the text as a vector of numerical characteristics. In this case, dividing the text into levels is considered as a common classification task in the field of computational linguistics. The experiments were conducted with our own corpus of 1904 texts. The best quality is achieved by rubert-base-cased-conversational without additional adaptation when determining both six and three text categories. The maximum F-measure value for levels A, B, C is 0.77. The maximum F-measure value for predicting six text categories is 0.67. The quality of text level determination depends more on the model than on the machine learning classification algorithm. The results differ from each other by no more than 0.01-0.02, especially for ensemble methods.
The use of multimodal data in emotion recognition systems has great potential for applications in various fields: healthcare, human-machine interfaces, operator monitoring, and marketing. Until recently, the development of emotion recognition systems based on multimodal data was constrained by insufficient computing power. However, with the advent of high-performance GPU-based systems and the development of efficient deep neural network architectures, there has been a surge of research aimed at using multiple modalities such as audio, video, and physiological signals to accurately detect human emotions. In addition, physiological data from wearable devices has become important due to the relative ease of its collection and the accuracy it enables. This paper discusses architectures and methods for applying deep neural networks to analyse multimodal data to improve the accuracy and reliability of emotion recognition systems, presenting current approaches to implementing such algorithms and existing open multimodal datasets.
The article addresses the development of a methodology for hierarchical multi-task learning of neural networks, inspired by the ERNIE 3 architecture, and its experimental validation using the FRED-T5 model for Russian-language text analysis and generation tasks. Hierarchical multi-task learning represents a promising approach for creating universal language models capable of efficiently solving a variety of natural language processing (NLP) tasks. The proposed methodology integrates specialized encoder blocks for natural language understanding (NLU) tasks with a shared decoder for natural language generation (NLG) tasks, thus improving model performance and reducing computational costs. This paper presents a comparative analysis of the developed methodology’s performance using the open Russian SuperGLUE benchmark and the pre-trained Russian-language model FRED-T5-1.7B. Experimental results confirm a significant improvement in model quality in both zero-shot and few-shot scenarios compared to the baseline configuration. Additionally, the paper explores practical applications of the developed approach in real NLP tasks and provides recommendations for further advancement of the methodology and its integration into applied systems for processing Russian-language texts.
This paper proposes a systematic approach to developing combinatorial generation algorithms for sets of discrete structures whose cardinality is determined by the coefficients of algebraic generating functions and their powers. The study is based on the relationship between operations on generating functions and combinatorial sets. It uses the mathematical apparatus of AND/OR trees as a foundation, which allows combining combinatorial generation algorithms for simple substructures into complex combinatorial objects. The main theoretical result of the work is the derivation of new efficient recurrence formulas for calculating the values of the coefficients of algebraic generating functions and their powers with polynomial computational complexity $O((n_1 + \ldots + n_m + m) \cdot n^2)$ for time and $O(n^2)$ for memory. Based on proven theorems on recurrence formulas, the proposed approach enables the construction of algorithms with polynomial computational complexity estimates, making them applicable to solving practical problems in applied discrete mathematics and theoretical computer science. Moreover, the use of coefficients of generating function powers expands the generation capabilities, since it allows us to construct not only objects of the original combinatorial set associated with the generating function, but also tuples of such objects. Validation of the proposed approach is demonstrated using examples of deriving recurrence formulas and generation algorithms based on them for classical numerical sequences, such as the Fibonacci, Pell, Catalan, Motzkin, and Schroder numbers. The proposed approach opens up new possibilities for solving problems of optimization, modeling, and coding complex discrete structures, for example, in fields such as bioinformatics and cryptography.
