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.

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.

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.

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.

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.