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.
We consider the problem of feasible vertex coloring with the minimum number of colors for connected undirected graphs that contain no self-loops or multiple edges. For every given $k \geq 3$, the problem of checking the existence of a feasible vertex coloring of the graph with k colors is NP-complete. Therefore, studying graph-scaling processes while preserving or limiting their chromatic numbers is of interest. In this paper, we study the nature of changes in the chromatic number of graphs with an increase in the number of vertices and edges using gluing operations by identifying their isomorphic subgraphs. $G = (G_{1} \circ G_{2}) \tilde{G}$ — is the resulting graph of the gluing operation of graphs $G_1$ and $G_2$; $\tilde{G} \subseteq G$ is the subgraph obtained as a result of identifying isomorphic subgraphs $G_1' \subseteq G_1$ and $G_2' \subseteq G_2$; $|V(G)| = |V(G_1)| + |V(G_2)| - |V(\tilde{G})|, |E(G)| = |E(G_1)| + |E(G_2)| - |E(\tilde{G})|$. Gluing operations in which one of the graphs $G_1$ or $G_2$ is isomorphic to another graph or its subgraph and the identification of subgraphs $G_1^{'}\subset G_1$ and $G_2^{'} \subset G_2$ is carried out in accordance with the isomorphism $G_1' \cong G_2'$, are called cloning operations. A constructive description of a class of 2-chromatic graphs is obtained based on the gluing and cloning operations. Constraints on the gluing and cloning operations that ensure the preservation of the chromatic number of scalable graphs are formulated. It is established that when performing cloning operations, $\chi(G) =\max{\chi(G_1),\chi(G_2)}$. Examples of assembling 2-chromatic graphs using operations satisfying these constraints are given. For an arbitrary gluing operation $\chi(G) \leqslant \max {\chi(G_1),\chi(G_2)} + |V(\tilde{G})| - |V(\tilde{G'})|$, where $\tilde{G'}$ is the maximal complete subgraph of $\tilde{G}$. The possible growth of the chromatic number of graphs is estimated when scaling with various restrictions on the superposition of gluing operations.
The paper investigates the impact of training set size on the quality of automatic short answers grading, formulated as a classification task. The impact was evaluated using a method based on measuring the similarity between the assessed answer and a given reference answer, calculated via embedding vectors, in combination with a logistic regression classifier. Experiments were conducted on corpora of answers to questions in computer science, history, and software development using Qt framework. The sizes of the corpora were 547, 522, and 931 answers, respectively. Two experiments were conducted during the study. In the first experiment, the change in classification quality was assessed as the training set size was reduced. It showed that when the binary classification is utilized (an answer can be either correct or incorrect), reducing the size of the training set leads to a smaller decline in quality compared to ternary classification (which includes a class of partially correct answers). In the second experiment, the possibility of improving classification quality by expanding small‑sized training sets through data augmentation was investigated. It demonstrated that augmentation performed using the DeepSeek generative model can significantly improve results in several cases, which is important for practical applications under data scarcity conditions. Additionally, the experiments revealed that when different language models are used to generate embeddings, the magnitude of change in classification quality with varying training set sizes can differ significantly. Specifically, using certain models — such as rubert‑tiny2 and MiniLM‑L12‑v2 — to produce embeddings yields more stable results than using other models.
This paper investigates the task of automatic word alignment in parallel texts, a fundamental step for training machine translation systems, conducting comparative linguistic studies, and creating linguistic resources. Given the scarcity of annotated data for many language pairs, the applicability of Large Language Models (LLMs) becomes particularly relevant due to their high generalization capabilities and ability to solve tasks without extensive fine-tuning on target datasets. This study presents a comparative analysis of the effectiveness of modern general-purpose LLMs versus specialized alignment algorithms using Russian-English parallel data. The research involved testing ten state-of-the-art models (including Gemini 3 Pro, GPT-5.2, and Claude Sonnet 4.5) using various prompting strategies (zero-shot, few-shot), alongside five baseline approaches ranging from statistical methods (fast-align, eflomal) to neural network architectures (AwesomeAlign, AccAlign, BinaryAlign). Performance was evaluated based on Precision, Recall, F-measure, and Alignment Error Rate (AER) metrics using annotated data from the Russian National Corpus. Experimental results indicated that the specialized BinaryAlign algorithm maintains the lead in overall alignment quality (F-measure 0.883, AER 0.113). However, leading LLMs, specifically Gemini 3 Pro Preview and GPT-5.2, demonstrated results surpassing those of most classic and early neural network baselines. Notably, for the most effective models, including in-context examples often reduced performance compared to the zero-shot setting. Thus, modern LLMs can serve as a reliable tool for high-quality alignment in the absence of training data, opening new perspectives for processing low-resource language pairs.
We analyzed 133 linguistic features for automated proficiency classification under the Common European Framework of Reference (CEFR) in a two-tier architecture: deterministic Tier 1 (lexical, morphological, and syntactic measures) and machine-learning-based Tier 2 (semantic coherence, topic structure, cohesion, and error-analysis signals). Experiments were conducted on a corpus of 3,205 learner texts from mixed sources, with triangulated validation against expert-verified Cambridge examination subsets. The materials were collected in 2022--2025 and included a substantial institutional corpus of over 3,000 essays and other writing texts produced by students of Moscow Institute of Physics and Technology (MIPT) studying English as a foreign language and regularly assessed by our AI-powered testing system ISTOK (Intelligent System for Testing General Language Competencies). Feature matrices were standardized after missing-value handling (fold-local median imputation for cross-validation and zero-fill for held-out reporting). In supervised evaluation, the best Tier 1+2 model reaches 66.72% exact accuracy (macro F1 = 0.69) and 94.53% adjacent accuracy (within one CEFR level) on a 3,198-sample CEFR-labeled benchmark split; an extended comparison including preliminary Tier 3 features achieves 67.50%. Unsupervised analyses show strong structure for extreme levels (A1 99.5% purity; C2 82.4% purity) and moderate alignment with professional Cambridge labels (Adjusted Rand Index = 0.303). We report block ablations and compact subset searches, with strongest signals from morphological complexity and lexical sophistication, and consistent incremental gains from error-based features. The results provide a validated, interpretable feature inventory and practical guidance for feature selection in automated language assessment systems.
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.
The large states pace of programs makes their direct verification by model checking difficult or impossible. The presence of symmetry in a program often allows simplifying the model and reducing its state space, leading to significant decrease of verification time. The classical approach consists in detecting a symmetry group and constructing a quotient model based on it — a simplified model for verification purposes. However, not all tools provide support for symmetry, and those that do may still struggle because finding an appropriate symmetry group is computationally complex problem.This work proposes an approach to program development based on explicit symmetry exploitation, which is an alternative to the classical one. In the program, a core is extracted — a coordination center working under consideration of symmetry and responsible for ensuring temporal properties. The core coordinates computations outside itself — those placed in the wrapper surrounding the core. As a result, the core has a small state space, replace the quotient model and allows verification using a model checker without symmetry support. The wrapper cannot interfere in the operation of the verified core and violate its properties. The approach is demonstrated by the example of the development and verification of the Mars rover resource arbiter. The arbiter coordinates access of n processes to m resources where both n and m are natural numbers. Programming languages C/C++ and the Spin model checker tool are used. The behavioral model of the core is automatically extracted by the Spin tool from the C code. Temporal properties expressed via Linear Temporal Logic (LTL) are subject to verification.
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.
The article examines the application of deep reinforcement learning methods to solve the problem of automated scheduling of driver shifts for urban passenger transport. The Crew Scheduling Problem belongs to the class of NP-hard combinatorial optimization problems and is characterized by a multitude of complex constraints related to labor legislation and the operational specifics of the transport network. The problem formulation, considering route changes, is described. The problem is formalized as a Markov Decision Process, taking into account specific constraints of the transport industry: maximum working hours, lunch breaks, and minimum rest time between trips. The state space is formulated, including features of control stops, the current trip, and candidate shifts. A mechanism for prioritized selection of candidate shifts is described to reduce the dimensionality of the action space. A multi-component reward function is described, considering the number of shifts utilized, deadhead travel time, and driver utilization. The agent's architecture is implemented based on the Actor-Critic method with the Proximal Policy Optimization algorithm. An experimental study was conducted on real data from the transport network of the city of Yaroslavl, including 6 routes and 974 trips. A comparative analysis was conducted with alternative methods: DQN, REINFORCE, and a heuristic approach represented by a greedy algorithm. The comparative analysis of the results demonstrated the superiority of the PPO algorithm over the other approaches. As a result of the study, it was concluded that reinforcement learning methods can be used to solve transportation optimization problems.
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.
