We consider while-language programs with variables of two security types: low and high. Security static analysis of information flows of such programs identifies insecure information flows which can cause leaks. Semantic rules of such an analysis which was proposed in [6] assign security types for expressions, operators and compositions of operators. We use these rules to propose an algorithm of security static analysis to discover a security type of the program under consideration. If such a type can be assigned, information flows of the program are secure; otherwise, it contains insecure information flows. We have used flex and bison [5] tools to implement a translator for a while-language into the MMIX computer [2] instruction sequence.

A multi-tenant database cluster is a concept of a data-storage subsystem for cloud applications with the multi-tenant architecture. The cluster is a set of relational database servers with the single entry point, combined into one unit with a cluster controller. This system is aimed to be used by applications developed according to Software as a Service (SaaS) paradigm and allows to place tenants at database servers so that providing their isolation, data backup and the most effective usage of available computational power. One of the most important problems about such a system is an effective distribution of data into servers, which affects the degree of individual cluster nodes load and faulttolerance. This paper considers the data-management approach, based on the usage of a load-balancing quality measure function. This function is used during initial placement of new tenants and also during placement optimization steps. Standard schemes of metaheuristic optimization such as simulated annealing and tabu search are used to find a better tenant placement.

The integrality recognition problem is considered on the sequence M_n,k of the nested Boolean quadric polytope relaxations, including the rooted semimetric Mn and the metric M_n,3 polytopes. Constraints of the metric polytope cut off all faces of the rooted semimetric polytope, containing only fractional vertices, that allows to solve the problem of integrality recognition on M_n in polynomial time. To solve the problem of integrality recognition on the metric polytope, we consider the possibility of cutting off all fractional faces of M_n,3 by some relaxation M_n,k. We represent the coordinates of the metric polytope in a homogeneous form by a three-dimensional block matrix. We show that to answer the question of the metric polytope fractional faces cutting off, it is sufficient to consider only constraints of the triangle inequalities form.

In this article we study the Fano variety of lines on the complete intersection of the grassmannian G(n, 2n) with hypersurfaces of degrees d₁ ..., d_i . A length l path on such a variety is a connected curve composed of l lines. The main result of this article states that the space of length l paths connecting any two given points on the variety is nonempty and connected if ∑d_j < n/4 . To prove this result we first show that the space of length n paths on the grassmannian G(n, 2n) that join two generic points is isomorphic to the direct product F_n ×F_n of spaces of full flags. After this we construct on Fn ×Fn a globally generated vector bundle E with a distinguished section s such that the zeros of s coincide with the space of length n paths that join x and y and lie in the intersection of hypersurfaces of degrees d₁,...,d_k. Using a presentation of E as a sum of linear bundles we show that zeros of its generic and, hence, any section form a non empty connected subvariety of F_n × F_n. Apart from its immediate geometric interest, this result will be used in our future work on generalisation of splitting theorems for finite rank vector bundles on ind-manifolds.

A perfect prismatoid is a convex polytope P such that for every its facet F there exists a supporting hyperplane α k F such that any vertex of P belongs to either F or α. Perfect prismatoids concern with Kalai conjecture, that any centrally symmetric dpolytope P has at least 3^d non-empty faces and any polytope with exactly 3^d non-empty faces is a Hanner polytope. Any Hanner polytope is a perfect prismatoid (but not vice versa). A 0/1-polytope is a convex hull of some vertices of the d-dimensional unit cube. We prove that every perfect prismatoid is affinely equivalent to some 0/1-polytope of the same dimension. (And therefore every perfect prismatoid is a lattice polytope.) Let Λ be a lattice in R^d and D be a polytope inscribed in a sphere B. Denote a boundary of B by ∂B and an interior of B by int B. The polytope D is a lattice Delaunay polytope if Λ∩int B = ∅ and D is a convex hull of Λ∩∂B. We prove that every perfect prismatoid is affinely equivalent to some lattice Delaunay polytope.

A combinatorial optimization problem is called stable if its solution is preserved under perturbation of the input parameters that do not exceed a certain threshold – the stability radius. In [1–3] exact polynomial algorithms have been built for some NP-hard problems on cuts in the assumption of the entrance stability. In this paper we show how to accelerate some algorithms for sufficiently stable polynomial problems. The approach is illustrated by the well-known problem of the minimum cut (MINCUT). We built an O(n²) exact algorithm for solving n-stable instance of the MINCUT problem. Moreover, we present a polynomial algorithm for calculating the stability radius and a simple criterion for checking n-stability of the MINCUT problem.

In this paper we consider the problem of detection of changes and estimation of the degree of these changes in a dynamically changing binary image. The authors introduce the numerical characteristic degree of change areas in dynamically changing binary images, based on the Jaccard similarity coefficient. To calculate this characteristic the authors developed an original architecture of a two-dimensional cellular automaton with the diffusion dynamics. We establish that cellular automaton configurations converge to a stationary configuration. The stationary configuration of a cellular automaton defines the desired characteristics for each area in dynamically changing binary images. The result can be presented as a grayscale image, that greatly facilitates the visual analysis of the dynamics of changes in dynamically changing binary images. The suggested approach can be used to detect and numerically estimate changes in the case when a number of brightness gradation comprises more than two values.

The article extends the cycle of papers dedicated to programming and verificatoin of PLC-programs by LTL-specification. This approach provides the availability of correctness analysis of PLC-programs by the model checking method.

The model checking method needs to construct a finite model of a PLC program. For successful verification of required properties it is important to take into consideration that not all combinations of input signals from the sensors can occur while PLC works with a control object. This fact requires more advertence to the construction of the PLC-program model.

In this paper we propose to describe a consistent behavior of sensors by three groups of LTL-formulas. They will affect the program model, approximating it to the actual behavior of the PLC program. The idea of LTL-requirements is shown by an example.

A PLC program is a description of reactions on input signals from sensors, switches and buttons. In constructing a PLC-program model, the approach to modeling a consistent behavior of PLC sensors allows to focus on modeling precisely these reactions without an extension of the program model by additional structures for realization of a realistic behavior of sensors. The consistent behavior of sensors is taken into account only at the stage of checking a conformity of the programming model to required properties, i. e. a property satisfaction proof for the constructed model occurs with the condition that the model contains only such executions of the program that comply with the consistent behavior of sensors.

Nowadays there exist many different ways to measure a person’s heart rate. One of them assumes the usage of a mobile phone built-in camera. This method is easy to use and does not require any additional skills or special devices for heart rate measurement. It requires only a mobile cellphone with a built-in camera and a flash. The main idea of the method is to detect changes in finger skin color that occur due to blood pulsation. The measurement process is simple: the user covers the camera lens with a finger and the application on the mobile phone starts catching and analyzing frames from the camera. Heart rate can be calculated by analyzing average red component values of frames taken by the mobile cellphone camera that contain images of an area of the skin.

In this paper the authors review the existing algorithms for heart rate measurement with the help of a mobile phone camera and propose their own algorithm which is more efficient than the reviewed algorithms.

Algebraic program models with procedures are designed to analyze program semantic properties on their models called program schemes. Procedural liberisation problem and equivalence problem are stated for program models with procedures in which both defining parameters are chosen independently. Program models with procedures built over a given program model without procedures are investigated. Algorithms for both stated tasks are proposed for models where an additional restriction is applied: the intersection emptiness problem is solvable in the program model without procedures. Polynomial estimates for the complexity of the algorithms are shown. Some topics for further investigation are proposed.

The paper considers algebraic program models with procedures designed to analyze program semantic properties based on program schemes. This leads to the problem of program scheme equivalence and the problem of constructing a complete system of equivalent program scheme transformations. Among algebraic program models with procedures, we focus on gateway models induced by program models without procedures and primitive program schemes belonging to these gateway models. The equivalence problem is decidable for these schemes. In the case where the inducer is a special type of program model without procedures, we construct a complete system of equivalent scheme transformations for a particular subclass of primitive program schemes.

The problem of integer balancing of a three-dimensional matrix with constraints of second type is studied. The elements of the inner part (all three indices are greater than zero) of the three-dimensional matrix are summed in each direction and each section of the matrix; the total sum is also found. These sums are placed into the elements where one or more indices are equal to zero (according to the summing directions). The problem is to find an integer matrix of the same structure, which can be produced from the initial one by replacing the elements of the inner part with the largest previous or the smallest following integer. At the same time, variations of the sums of elements from those in the initial matrix should be less than 2 and the element with three zero indices should be produced with standard rules of rounding-off. Heuristic algorithms for this problem are suggested in the article: layering algorithm being got as generalization of a similar algorithm for the problem with constraints of first type and a new matrix algorithm. The last one consists of three parts: search for the base matrix, search for the maximal matrix and matrix correcting. Each of them is a cyclic change of the integer matrix using from 1 to 3 elements from the inner part. A modification of the matrix algorithm is suggested. The algorithm is directed to more uniform filling of the inner part of the integer matrix. Also, the complexity of all three algorithms is estimated in the article. The comparative analysis of matrix algorithms based on the results of computing experiments is adduced.

Let K be an arbitrary root class of groups. This means that K contains at least one non-unit group, is closed under taking subgroups and direct products of a finite number of factors and satisfies the Gruenberg condition: if 1 ≤ Z ≤ Y ≤ X is a subnormal series of a group X such that X/Y ∈ K and Y/Z ∈ K, there exists a normal subgroup T of X such that T ⊆ Z and X/T ∈ K. In this paper we study the property ‘to be residually a K-group’ of an HNN-extension in the case when its associated subgroups coincide. Let G = (B, t; t¯¹Ht = H, φ). We get a sufficient condition for G to be residually a K-group in the case when B ∈ K and H is normal in B, which turns out to be necessary if K is closed under factorization. We also obtain criteria for G to be residually a K-group provided that K is closed under factorization, B is residually a K-group, H is normal in B and satisfies at least one of the following conditions: Aut_G(H) is abelian (we denote by Aut_G(H) the group of all automorphisms of H which are the restrictions on this subgroup of all inner automorphisms of G); Aut_G(H) is finite; φ coincides with the restriction on H of an inner automorphism of B; H is finite; H is infinite cyclic; H is of finite Hirsh-Zaitsev rank (i. e. H possesses a finite subnormal series all factors of which are either periodic or infinite cyclic). Besides, we find a sufficient condition for G to be residually a K-group in the case when B is residually a K-group and H is a retract of B (K is not necessarily closed under the factorization in this statement).

Process mining is a new emerging discipline related to process management, formal process models, and data mining. One of the main tasks of process mining is the model synthesis (discovery) based on event logs. A wide range of algorithms for process model discovery, analysis, and enhancement is developed. The real-life event logs often contain noise of different types. In this paper we describe the main causes of noise in the event logs and study the effect of noise on the performance of process discovery algorithms. The experimental results of application of the main process discovery algorithms to artificial event logs with noise are provided. Specially generated event logs with noise of different types were processed using the four basic discovery techniques. Although modern algorithms can cope with some types of noise, in most cases, their use does not lead to obtaining a satisfactory result. Thus, there is a need for more sophisticated algorithms to deal with noise of different types.