Editorials
Articles
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.
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.
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.
We present an algorithm for simplifying linear cartographic objects and results obtained with a computer program implementing this algorithm.
ISSN 2313-5417 (Online)