We investigate a model checking problem for the logic of common knowledge and fixpoints µPLC_n in well-structured multiagent systems with perfect recall. In this paper we show that a perfect recall synchronous environment over a well-structured environment forms a well-structured environment provided with a special PRS-order. This implies that the model checking problem for the disjunctive fragment of µPLC_n is decidable.

Bounded model checking (BMC) of C/C++ programs is a matter of scientific enquiry that attracts great attention in the last few years. In this paper, we present our approach to this problem. It is based on combining several recent results in BMC, namely, the use of LLVM as a baseline for model generation, employment of high-performance Z3 SMT solver to do the formula heavy-lifting, and the use of various function summaries to improve analysis efficiency and expressive power. We have implemented a basic prototype; experiment results on a set of simple test BMC problems are satisfactory.  

Software-defined networking (SDN) is an approach to building computer networks that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and flow-table updating was defined in the form of a protocol known as OpenFlow. In this paper we describe an abstract formal model of SDN, introduce a tentative language for specification of SDN forwarding policies, and set up formally model-checking problems for SDN.

The development of the C-light project resulted in the application of new formalisms and implementation techniques which facilitate the verification process. The mixed axiomatic semantics proposes a choice between simplified and full-strength deduction rules depending on program objects and their properties. The LLVM infrastructure helps greatly in writing the C-light program analyzer and translator. The semantical labeling technique, proposed earlier, can now be safely kept in verification conditions during their proof. Two programs from the well-known verification benchmarks illustrate the applicability of the system.

This paper presents an overview of technology of the automated generation of test scenarios based on guides. The usage of this technology can significantly improve the quality of the developed program products. In order to ground the technology creation, the main problems that occur during the development and testing of the large industrial systems, are described, as well as the methodologies of software verification on conformity to product requirements. The potentialities of tools for automatic and semi-automatic generation of a test suite by using a formal model in UCM notation are demonstrated, as well as tools for verification and automation of testing.

An approach to construction and verification of PLC LD-programs for discrete problems is proposed. For the specification of the program behavior, we use the linear-time temporal logic LTL. Programming is carried out in the LD-language (Ladder Diagram) according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLC LD-programs is shown by an example. For a discrete problem, we give a LD-program, its LTL-specification and an SMV-model. The purpose of the article is to describe an approach to programming PLC, which would provide a possibility of LD-program correctness analysis by the model checking method. Under the proposed approach, the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations which increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for speci- fication of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program (LD-program), which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTLspecification of the behavior of each program variable. In addition, an SMV-model of a PLC LD-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.

The International Conference on “Geometry, Topology, and Applications”, dedicated to the upcoming 70th birthday of Nikolai Dolbilin, was organized by the International Delaunay Laboratory on Discrete and Computational Geometry and took place in September 23–27, 2013, at the P.G. Demidov Yaroslavl State University. This note highlights the main results presented at the conference and underlines the role of such meetings in the development of the field of Discrete and Computational Geometry in Russia.

The article is published in the author’s wording.

 

The paper establishes that the rank of a regular polygonal complex in E³ cannot exceed 4, and that the only regular polygonal complexes of rank 4 in E³ are the eight regular 4-apeirotopes in E³ . The article is published in the author’s wording.

Persistent homology probes topological properties from point clouds and functions. By looking at multiple scales simultaneously, one can record the births and deaths of topological features as the scale varies. In this paper we use a statistical technique, the empirical bootstrap, to separate topological signal from topological noise. In particular, we derive confidence sets for persistence diagrams and confi- dence bands for persistence landscapes.

The article is published in the author’s wording.

For a finite Coxeter group W, a subword complex is a simplicial complex associated with a pair (Q, ρ), where Q is a word in the alphabet of simple reflections, ρ is a group element. We describe the transformations of such a complex induced by nil-moves and inverse operations on Q in the nil-Hecke monoid corresponding to W. If the complex is polytopal, we also describe such transformations for the dual polytope. For W simply-laced, these descriptions and results of [5] provide an algorithm for the construction of the subword complex corresponding to (Q, ρ) from the one corresponding to (δ(Q), ρ), for any sequence of elementary moves reducing the word Q to its Demazure product δ(Q). The former complex is spherical or empty if and only if the latter one is empty. The article is published in the author’s wording.

Each convex polytope P = P(α) can be described by a set of linear inequalities determined by vectors p and right hand sides α(p). For a fixed set of vectors p, a type domain D(P₀) of a polytope P₀ and, in particular, of a parallelotope P₀ is defined as a set of parameters α(p) such that polytopes P(α) have the same combinatorial type as P₀ for all α ∈ D(P₀).

In the second part of the paper, a facet description of zonotopes and zonotopal parallelotopes are given.

The article is published in the author’s wording.

We present a new class of random packing, called an “areal random packing”, in the plane. After performing computer simulations, we obtain the areal packing density through statistical analysis. One-dimensional version of areal random packing is also presented. Remarks about the connection to the random disk packing and to other processes are given. The article is published in the author’s wording.

We study homology groups of the space W˜₁(∇^N ) of triangulations of the twodimensional simplex with vertices D₀D₁D₂ endowed with a boundary subdivision with not more than 6 vertices in case when this boundary subdivision is extended to the interior of the simplex without adding new interior vertices. As a result, we obtain a theorem about the homology groups H_n in cases n = 0, . . . , 5.

The article is published in the author’s wording.

We propose a new approach to the problem of calculations of volumes in the Lobachevsky space, and we apply this method to tetrahedra. Using some integral formulas, we present an explicit formula for the volume of a tetrahedron in the function of the coordinates of its vertices as well as in the function of its edge lengths. Finally, we give a direct analitic proof of the famous Schläfli formula for tetrahedra.

In this work, we describe a prototype of an automatic segmentation system and annotation of endoscopy images. The used algorithm is based on the classification of vectors of the topological features of the original image. We use the image processing scheme which includes image preprocessing, calculation of vector descriptors defined for every point of the source image and the subsequent classification of descriptors. Image preprocessing includes finding and selecting artifacts and equalizating the image brightness. In this work, we give the detailed algorithm of the construction of topological descriptors and the classifier creating procedure based on mutual sharing the AdaBoost scheme and a naive Bayes classifier. In the final section, we show the results of the classification of real endoscopic images.

The paper proposes a generalization of entropy as in [1]. At first, to constract the estimator, we select the metrics on the space of sequances. This metrics is based on a matrix that can be interpreted as an edge coloring of a complete graph with loops. A generalization consists in that instead of using the logarithm in the estimation of the entropy, we apply a similar function which may be arbitrary at the given range. The proposed function is not monotone, so the task of optimizing the average deviation which is a quadratic optimization problem, is solved in the whole space and not on the simplex. The main properties of the estimator, such as asymptotic unbiasedness and power decrease dispersion, are proved in a similar way.

A method of modeling the phenomenon of bursting behavior in neural systems based on delay equations is proposed. A singularly perturbed scalar nonlinear differentialdifference equation of Volterra type is a mathematical model of a neuron and a separate pulse containing one function without delay and two functions with different lags. It is established that this equation, for a suitable choice of parameters, has a stable periodic motion with any preassigned number of bursts in the time interval of the period length. To prove this assertion we first go to a relay-type equation and then determine the asymptotic solutions of a singularly perturbed equation. On the basis of this asymptotics the Poincare operator is constructed. The resulting operator carries a closed bounded convex set of initial conditions into itself, which suggests that it has at least one fixed point. The Frechet derivative evaluation of the succession operator, made in the paper, allows us to prove the uniqueness and stability of the resulting relax of the periodic solution.