In this paper, we study polyhedral properties of two spanning tree problems with additional constraints. In the first problem, it is required to find a tree with a minimum sum of edge weights among all spanning trees with the number of leaves less than or equal to a given value. In the second problem, an additional constraint is the assumption that the degree of all nodes of the spanning tree does not exceed a given value. The recognition versions of both problems are NP-complete. We consider polytopes of these problems and their 1-skeletons. We prove that in both cases it is a NP-complete problem to determine whether the vertices of 1-skeleton are adjacent. Although it is possible to obtain a superpolynomial lower bounds on the clique numbers of these graphs. These values characterize the time complexity in a broad class of algorithms based on linear comparisons. The results indicate a fundamental difference between combinatorial and geometric properties of the considered problems from the classical minimum spanning tree problem.

We consider a problem of constructive description and justification of the algorithms necessary for a practical implementation of the majority decoder for group codes specified as left ideals of group
algebras. In addition to the algorithms needed to implement a classical decoder of J. Massey, it is built a generalization of the classical decoder for codes with unequal protection of characters, which in some cases could be better than the classic one. For use as a classical decoder of J. Massey and its generalization to group codes it was developed an algorithm for constructing decoding trees that lie at the core of these algorithms for majority decoding. Because group codes are defined as left ideals of group algebras, the decoding algorithm for constructing decoding trees allows to build all decoding trees from one tree. On the basis of the generalized decoding algorithm it was developed an algorithm for decoding group codes induced on the subgroup. Application of the developed decoders was illustrated by an example of Reed-Muller-Berman codes and group codes induced by them on a non-Abelian group of affine transformations. In particular, for Reed–Muller–Berman code description and justification of the algorithm for constructing one decoding tree are provided. This three is used for constructing all decoding trees and then it is a built decoder for Reed-Muller-Berman codes and codes induced by them.

Let G be a finite nontrivial group with an irreducible complex character χ of degree d = χ(1). It is known from the orthogonality relation that the sum of the squares of degrees of irreducible characters of G is equal to the order of G. N. Snyder proved that if |G| = d(d + e), then the order of G is bounded in terms of e, provided e > 1. Y. Berkovich proved that in the case e = 1 the group G is Frobenius with the complement of order d. We study a finite nontrivial group G with an irreducible complex character Θ such that |G| ≤ 2Θ(1)2 and Θ(1) = pq, where p and q are different primes. In this case we prove that G is solvable groups with abelian normal subgroup K of index pq. We use the classification of finite simple groups and prove that the simple nonabelian group whose order is divisible by a prime p and of order less than 2p4 is isomorphic to L2(q), L3(q), U3(q), Sz(8), A7, M11 or J1.

In 1973, Allenby and Gregoras proved the following statement. Let G be a split extension of a finitely generated group A by the group B. 1) If in groups A and B all subgroups (all cyclic subgroups) are finitely separable, then in group G all subgroups (all cyclic subgroups) are finitely separable; 2) if in group A all subgroups are finitely separable, and in group B all finitely generated subgroups are finitely separable, then in group G all finitely generated subgroups are finitely separable. Recall that a group G is said to be a split extension of a group A by a group B, if the group A is a normal subgroup of G, B is a subgroup of G, G = AB and A ∩ B = 1. Recall also that the subgroup H of a group G is called finitely separable if for every element g of G, which does not belong to the subgroup H, there exists a homomorphism of G on a finite group in which the image of an element g does not belong to the image of the subgroup H. In this paper we obtained a generalization of the Allenby and Gregoras theorem by replacing the condition of the finitely generated group A by a more general one: for any natural number n the number of all subgroups of the group A of index n is finite. In fact, under this condition we managed to obtain a necessary and sufficient condition for finite separability of all subgroups (of all cyclic subgroups, of all finitely generated subgroups) in the group G.

The article is devoted to the approach to constructing and verification of discrete PLC-programs by LTL-specification. This approach provides an ability of correctness analysis of PLC-programs by the model checking method. The linear temporal logic LTL is used as a language of specification of the program behavior. The correctness analysis of LTL-specification is automatically performed by the symbolic model checking tool Cadence SMV. The article demonstrates the consistency of the approach to constructing and verification of PLC programs by LTL-specification from the point of view of Turing power. It is proved, that in accordance with this approach for any Minsky counter machine can be built an LTL-specification, which is used for machine implementation in any PLC programming language of standard IEC 61131-3. Minsky machines equipollent Turing machines, and the considered approach also has Turing power. The proof focuses on representation of a counter machine behavior in the form of a set of LTL-formulas and matching these formulas to constructions of ST and SFC languages. SFC is interesting as a specific graphical language. ST is considered as a basic language because an implementation of a counter machine in IL, FBD/CFC and LD languages is reduced to rewriting blocks of ST-program. The idea of the proof is demonstrated by an example of a Minsky 3-counter machine, which implements a function of squaring.

The purpose of this work is to develop a unitary mechanism of adaptive routing of different kinds, basing on the current requirements on the quality of service. The software configuration of a network is the technology of the future. The trend in communication systems constantly confirms this fact. However, the application of this technology in its current form is justified only in large networks of technology giants and telecom operators. Today we have a large number of dynamic routing protocols to route big volume traffic in communication networks. Our task is to create the solution that can use the opportunities of each node to make a decision on the transmission of information by all possible means for each type of traffic. Achieving this goal is possible by solving the problem of the development of generalized metrics, which details the links between devices in the network, and the problem of establishing a framework of adaptive logical network topology (route management) to ensure the quality of the whole network in order to meet the current requirements on the quality of a particular type service.

In the article the problem of finding the maximal multiple flow in the network of any natural multiplicity k is studied. There are arcs of three types: ordinary arcs, multiple arcs and multi-arcs. Each multiple and multi-arc is a union of k linked arcs, which are adjusted with each other. The network constructing rules are described. The definitions of a divisible network and some associated subjects are stated. The important property of the divisible network is that every divisible network can be partitioned into k parts, which are adjusted on the linked arcs of each multiple and multi-arc. Each part is the ordinary transportation network. The main results of the article are the following subclasses of the problem of finding the maximal multiple flow in the divisible network. 1. The divisible networks with the multi-arc constraints. Assume that only one vertex is the ending vertex for a multi-arc in k −1 network parts. In this case the problem can be solved in a polynomial time. 2. The divisible networks with the weak multi-arc constraints. Assume that only one vertex is the ending vertex for a multi-arc in s network parts (1 ≤ s < k − 1) and other parts have at least two such vertices. In that case the multiplicity of the multiple flow problem can be decreased to k − s. 3. The divisible network of the parallel structure. Assume that the divisible network component, which consists of all multiple arcs, can be partitioned into subcomponents, each of them containing exactly one vertex-beginning of a multi-arc. Suppose that intersection of each pair of subcomponents is the only vertex-network source x0. If k = 2, the maximal flow problem can be solved in a polynomial time. If k ≥ 3, the problem is NP-complete. The algorithms for each polynomial subclass are suggested. Also, the multiplicity decreasing algorithm for the divisible network with weak multi-arc constraints is formulated.

This article describes the organization principles for wireless mesh-networks (software-defined net-works of mobile objects). The emphasis is on the questions of getting effective routing algorithms for such networks. The mathematical model of the system is the standard transportation network. The key parameter of the routing system is the node reachability coefficient — the function depending on several basic and additional parameters (“mesh-factors”), which characterize the route between two network nodes. Each pair (arc, node) is juxtaposed to a composite parameter which characterizes the “reacha-bility” of the node by the route which begins with this arc. The best (“shortest”) route between two nodes is the route with the maximum reachability coefficient. The rules of building and refreshing the routing tables by the network nodes are described. With the announcement from the neighbor the node gets the information about the connection energy and reliability, the announcement time of receipt, the absence of transitional nodes and also about the connection capability. On the basis of this information
the node applies the penalization (decreasing the reachability coefficient) or the reward (increasing the reachability coefficient) to all routes through this neighbor node. The penalization / reward scheme has some separate aspects: 1. Penalization for the actuality of information. 2. Penalization / reward for the reliability of a node. 3. Penalization for the connection energy. 4. Penalization for the present connection capability. The simulator of the wireless mesh-network of mobile objects is written. It is based on the suggested heuristic algorithms. The description and characteristics of the simulator are stated in the article. The peculiarities of its program realization are also examined.

In the article a method of automated construction of Petri nets simulating the behaviour of imperative programs is considered from the formal point of view. Petri net samples with certain characteristics are necessary in programming new algorithms for program analysis; in particular, they can be used for developing or optimizing algorithms of Petri nets compositions and decompositions, building the reachability tree, checking invariants and so on. The generation process consists of two stages. At the first stage, construction templates for a resulting net and parameters for construction are described. With the help of these parameters it is possible to regulate the final size and the absolute or relative amount of certain structures in the resulting net. At the second stage, iterative process of automated net construction is used for Petri net generation of any size, limited only by an available computer memory. In the first section of the article the minimum necessary definitions are given and a new version of Petri nets composition operation by places is introduced. Commutative and associative properties of introduced binary operation allow to synchronize any number of Petri nets in arbitrary order. Then construction template is defined as a marked Petri net with input and output interfaces and rules for templates composition using this interfaces. A number of construction templates can be united in a collection, for which the evolution rules are defined. The completeness property of a collection guarantees that the collection evolution results in a Petri net that simulates the imperative program behavior. The article provides a version of the construction templates complete collection and an example of Petri net simulating sequential imperative program construction.

Nowadays, due to software sophistication, programs correctness is more often proved by means of formal verification. The method of deduction based on Hoare logic could be used for any programming
language and it has the capability of partial automation of the proof process. However, the method of deduction is not widely used for verification of parallel programs because of high complexity of the
process. The usage of the functional data-flow paradigm of parallel programming allows to decrease the complexity of the proof process. In this article a proof process of correctness of functional data-flow parallel programs in the Pifagor language is considered. The proof process of a program correctness is considered as a tree where each node is a program data-flow graph, whose edges are marked with formulas in a specification language. The tree root is the initial program data-flow graph with a precondition and a postcondition, which describe restrictions on input variables and correctness conditions of the result of the program execution, respectively. Basic transformations of the data-flow graph are edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the data-flow graph is transformed and finally is reduced to a set of formulas in the specification language. If all these formulas are identically true, the program is correct. Several modules is distinguished in the system: “Program correctness prover”, “Axioms and theorems library management system” and “Errors analysis and output of information about errors”. According to this architecture, the toolkit for supporting formal verification was developed. The main functionality of the system implementation is considered.