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.
