Hereditary graph properties are those that can be inherited from the graph to all its subgraphs (such as planarity). Modular nets of active resources is a (Petri nets)- powerful formalism with simple modular syntax. Boundedness and liveness are fundamental semantic properties for Petri net models. It is shown that boundedness and liveness, being not hereditary in general, are downward-hereditary (net-to-subnet) and upward-hereditary (subnet-to-net) for the particular types of AR-subnets. It is also shown that boundedness is downward-hereditary and unboundedness is upward-hereditary for arbitrary subnets after a specific module interface transformation (so-called R-normalization).

A technique of the computing grid verification using invariants of infinite Petri nets was presented. Models of square grid structures in the form of parametric Petri nets for such edge conditions as connection of edges and truncated devices were constructed. Infinite systems of linear algebraic equations were composed on parametric Petri nets for calculating p-invariants; their parametric solutions were obtained. P-invariant Petri nets are structuraly conservative and bounded that together with liveness are the properties of ideal systems. Liveness investigation based on siphons and traps can be implemented by using p-invariants of modified nets.

A deductive approach to verification of telecommunication systems written in C is proposed. The approach is based on the extension of C by declarative statements and on reduction of verification of parallel communicating components of these systems to separate verification of components written in this extension. An example of verification of a data link protocol is considered.

To verify real-time properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of real-time systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.

We consider the well-known Sliding Window Protocol which provides reliable and efficient transmission of data over unreliable channels. A formal proof of correctness for this protocol faces substantial difficulties caused by a high degree of parallelism which creates a significant potential for errors. Here we consider a version of the protocol that is based on selective repeat of frames. The specification of the protocol by a state machine and its safety property are represented in the language of the verification system PVS. Using the PVS system, we give an interactive proof of this property of the Sliding Window Protocol.

Nowadays most of software contains code duplication that leads to serious problems in software maintenance. A lot of different clone detection approaches have been proposed over the years to deal with this problem, but almost all of them do not consider semantic properties of the source code. We propose to reinforce traditional tree-based clone detection algorithms by using additional information about variable slices. This allows to find intertwined/gapped clones on variables; preliminary evaluation confirms applicability of our approach to real-world software.

In this paper we propose an approach to efficient automating test technology for industrial software projects, that uses a formal model of the system, automatically performs a symbolic verification, generation and concretization of the symbolic traces, the generation of test suites for concretized traces, and also includes tools for analysis of the testing results, allowing users to automate the full cycle of testing. Particular emphasis is placed on the presentation of the algorithm concretization and setting of test scenarios.

The Yaroslavl International Conference on Discrete Geometry dedicated to the centenary of A. D. Alexandrov was organized by the International B.N. Delaunay Laboratory "Discrete and Computational Geometry" and took place from August 13 to 18, 2012 at the P.G. Demidov Yaroslavl State University. The purpose of this note is to highlight the main results presented at the conference and to discuss the role of the meeting in the development of the field of Discrete and Computational Geometry in Yaroslavl. The article is published in the author’s wording.

We provide an effective description of graphs of polyhedra for GRAPH PARTITIONING and COMPLETE BIPARTITE SUBGRAPH problems. We establish the fact, that the clique number for each of this problems increases exponentially with the dimension of the space.

In this paper we consider theorems which are generalizations of the well-known corollaries of the Helly theorem

We study some problems of nodes localization in a Delaunay triangulation and problem-solving procedures. For the problem of the set of nodes the computationally efficient approach that uses Euclidean minimum spanning tree of Delaunay triangulation is proposed. Efficient estimations for computational comlexity of the proposed methods in the average and in the worst cases are proved.

computational geometry, geometric search, Delaunay triangulation, merging of overlapping triangulations, unregular discrete mesh, computational complexity

We proved in [10] that each Platonic polyhedron P can be folded into a flat multilayered face of P by a continuous folding process of polyhedra. In this paper, we give explicit formulas of continuous functions for such a continuous flattening process in R³ for a regular tetrahedron.

The article is published in the author’s wording.

In this paper we introduce and study a class of centrally symmetric polytopes – perfect prismatoids – and some its properties related to the famous conjecture concerning face numbers of centrally symmetric polytopes are proved. It is proved that any Hanner polytope is a perfect prismatoid and any perfect prismatoid is affine equivalent to some 0/1-polytope.

 

The present paper contains a sketch of the proof of an upper bound for the variance of the number of hyperfaces of a random polytope when the mother body is a simple polytope. Thus we verify a weaker version of the result in [1] stated without a proof. The article is published in the author’s wording.

We present an algorithm for simplifying linear cartographic objects and results obtained with a computer program implementing this algorithm.

It is known that for each simplicial polyhedron P in 3-space there exists a monic polynomial Q depending on the combinatorial structure of P and the lengths of its edges only such that the volume of the polyhedron P as well as one of any polyhedron isometric to P and with the same combinatorial structure are roots of the polynomial Q. But this polynomial contains many millions of terms and it cannot be presented in an explicit form. In this work we indicate some special classes of polyhedra for which these polynomials can be found by a sufficiently effective algorithm which also works in spaces of constsnt curvature of any dimension.

It is a new proof of the Euler formula for a convex polyhedron in R³.