Cellular resource driven automata nets (CRDA-nets) is a generalization of the concept of two-level resource nets (Petri nets) with an infinite regular system grid. This formalism is a hybrid of Petri nets and asynchronous Cellular Automata and is designed for modeling multi-agent systems with dynamic spatial structure. Spatial boundedness is a property that guarantees the preservation of the finiteness of “geometric dimensions” of the active part of the system (for example, the living space) during its lifetime. Three variants of spatial boundedness for cellular RDA-nets are defined: localization, bounded diameter and bounded area. The properties of the corresponding algorithmic problems are investigated, their undecidability in the general case is proved. A non-trivial criterion for the localization of an one-dimensional CRDA-net is proposed, based on the new concept of the RDA propagation graph. An algorithm is described for constructing a propagation graph, using the method of saturation of generating paths. A method for estimating the diameter of an 1-dim CRDA with a bounded propagation graph is presented.

The paper is devoted to the tree centroid properties clarification. Attention of the authors was attracted by the popular problem of (binary) partition of a graph. The solution is known only by brute force algorithm. It was found that for a ”economical” partition of a tree it makes sense to consider partitions in the neighborhood of centroid vertices, the definition of which is presented. In the paper, we proposed proofs connected with the limitation of their weight. It is also proved that if there are two centroid vertices in a tree, they are adjacent. In what follows, it is noted that three such vertices can not be in the tree. The corresponding statements are made. According to the first one, any vertex of a tree with a certain restriction on its weight is centroid. According to one of the points of the second statement, if there are two centroid vertices in the tree, the order of the tree is an even number. The third statement says that if a tree has a centroid vertex of limited weight, there is another centroid vertex of the same weight and adjacent to the first one. To prove the propositions, we consider the branch of greatest weight with a centroid vertex and take in this branch another vertex adjacent to the centroid. In this paper, Jordan’s theorem is used, three images are used in the presentation of the material.

First-order program schemata is one of the simplest models of sequential imperative programs intended for solving verification and optimization problems. We consider the decidable relation of logical-thermal equivalence of these schemata and the problem of their size minimization while preserving logical-thermal equivalence. We prove that this problem is decidable. Further we show that the first-order program schemata supplied with logical-thermal equivalence and finite state deterministic transducers operating over substitutions are mutually translated into each other. This relationship implies that the equivalence checking problem and the minimization problem for these transducers are also decidable. In addition, on the basis of the discovered relationship, we have found a subclass of firstorder program schemata such that their minimization can be performed in polynomial time by means of known techniques for minimization of finite state transducers operating over semigroups. Finally, we demonstrate that in general case the minimization problem for finite state transducers over semigroups may have several non-isomorphic solutions.

In this paper, a modern CPU architecture with several different cache levels is described, and current CPU performance limitations such as silicone physical limitations or frequency increase bounds are mentioned. As usual, changes of the currently existing architecture are proposed as a way of increasing CPU performance, data rates on the internal and external CPU interfaces must be known. It would help to assess applicability of proposed solutions and allow to optimize them. This paper is aimed at getting real values of traffic on L2-L3 cache interface inside CPU and CPU-RAM bus load as well as show dependencies of total traffic on the interfaces of interest on the number of active cores, CPU frequency and test type. Measurements methodology using Intel Performance Counter Monitor by Intel is provided and equations that allow to get data rates from internal CPU counters are explained. Both real life and synthetic tests are described. Dependency of total traffic on the number of active cores and dependency of total traffic on CPU frequency are provided as plots. Dependency of total traffic on test type provided as bar plot for multiple CPU frequencies.

In this work, a model for computer system security threats formulated in terms of Markov processes is investigated. In the framework of this model the functioning of the computer system is considered as a sequence of failures and recovery actions which appear as results of information security threats acting on the system. We provide a detailed description of the model: the explicit analytical formulas for the probabilities of computer system states at any arbitrary moment of time are derived, some limiting cases are discussed, and the long-run dynamics of the system is analysed. The dependence of the security state probability (i.e. the state for which threats are absent) on the probabilities of threats is separately investigated. In particular, it is shown that this dependence is qualitatively different for odd and even moments of time. For instance, in the case of one threat the security state probability demonstrates non-monotonic dependence on the probability of threat at even moments of time; this function admits at least one local minimum in its domain of definition. It is believed that the mentioned feature is important because it allows to locate the most dangerous areas of threats where the security state probability can be lower then the permissible level. Finally, we introduce an important characteristic of the model, called the relaxation time, by means of which we construct the permitting domain of the security parameters. Also the prospects of the received results application to the problem of finding the optimal values of the security parameters is discussed.

During the life-cycle of an Information System (IS) its actual behaviour may not correspond to the original system model. However, to the IS support it is very important to have the latest model that reflects the current system behaviour. To correct the model, the information from the event log of the system may be used. In this paper, we consider the problem of process model adjustment (correction) using the information from an event log. The input data for this task are the initial process model (a Petri net) and the event log. The result of correction should be a new process model, better reflecting the real IS behavior than the initial model. The new model could be also built from scratch, for example, with the help of one of the known algorithms for automatic synthesis of the process model from an event log. However, this may lead to crucial changes in the structure of the original model, and it will be difficult to compare the new model with the initial one, hindering its understanding and analysis. It is important to keep the initial structure of the model as much as possible. In this paper, we propose a method for process model correction based on the principle of “divide and conquer”. The initial model is decomposed in several fragments. For each fragment its conformance to the event log is checked. Fragments which do not match the log are replaced by newly synthesized ones. The new model is then assembled from the fragments via transition fusion. The experiments demonstrate that our correction algorithm gives good results when it is used for correcting local discrepancies. The paper presents the description of the algorithm, the formal justification for its correctness, as well as the results of experimental testing by some artificial examples.

This article describes problems of designing automated teaching system for “Computational complexity of algorithms” course. This system should provide students with means to familiarize themselves with complex mathematical apparatus and improve their mathematical thinking in the respective area. The article introduces the technique of algorithms symbol scroll table that allows estimating lower and upper bounds of computational complexity. Further, we introduce a set of theorems that facilitate the analysis in cases when the integer rounding of algorithm parameters is involved and when analyzing the complexity of a sum. At the end, the article introduces a normal system of symbol transformations that allows one both to perform any symbol transformations and simplifies the automated validation of such transformations. The article is published in the authors’ wording.

Nowadays, the behaviour of many systems can be properly described by taking into account time constraints, and this motivates the adaptation of existing Finite State Machine (FSM)- based test derivation methods to timed models. In this paper, we propose a method for deriving conformance tests with the guaranteed fault coverage for a complete possibly nondeterministic FSM with a single clock; such Timed FSMs (TFSMs) are widely used when describing the behaviour of software and digital devices. The fault domain contains every complete TFSM with the known upper bounds on the number of states and finite boundary of input time guards. The proposed method is carried out by using an appropriate FSM abstraction of the given TFSM; the test is derived against an FSM abstraction and contains timed input sequences. Shorter test suites can be derived for a restricted fault domain, for instance, for the case when the smallest duration of an input time guard is larger than two. Moreover, the obtained test suites can be reduced, while preserving the completeness, when all input time guards of the specification and an implementation are right closed (or all intervals are left closed). Experiments are conducted to study the length of test suites constructed by different methods.

Let \(\Omega = A^{N}\) be a space of right-sided innite sequences drawn from a nite alphabet \(A = \{0,1\}\), \(N = \{1,2,\dots\}\). Let
$$\label{rho}
\rho(\boldsymbol{x},\boldsymbol{y}) =\sum_{k=1}^{\infty}|x_{k} - y_{k}|2^{-k}
$$

- be a metric on \(\Omega = A^{N}\), and \(\mu\) - the Bernoulli measure on \(\Omega\) with probabilities \(p_0,p_1>0\), \(p_0+p_1=1\). Denote by \(B(\boldsymbol{x},\omega)\) an open ball of radius \(r\) centered at \(\boldsymbol{\omega}\). The main result of this paper is
$$
\mu\left(B(\boldsymbol{\omega},r)\right) =r+\sum_{n=0}^{\infty}\sum_{j=0}^{2^n-1}\mu_{n,j}(\boldsymbol{\omega})\tau(2^nr-j),
$$
where \(tau(x) =2\min\{x,1-x\}\), \(0\leq x \leq 1\), \(tau(x) = 0, if x<0 or x>1\),

$$mu_{n,j}(\boldsymbol{\omega}) = \left(1-p_{\omega_{n+1}}\right)
\prod_{k=1}^n p_{\omega_k\oplus j_k},\ \ j = j_12^{n-1}+j_22^{n-2}+\dots+j_n$$.

The family of functions \(1,x,\tau(2^nx-j)\), \(j =0,1,\dots,2^n-1\), \(n=0,1,\dots\) is the Faber{Schauder system for the space \(C([0, 1])\) of continuous functions on \([0, 1]\).
We also obtain the Faber{Schauder expansion for the Lebesgue's singular function, Cezaro curves, and Koch{Peano curves.