The work is devoted to an attempt to use Golang programs for the specification and verification of distributed systems. The A.P. Ershov Institute of Informatics Systems, SB RAS, has been developing this approach for years. A distributed system described in terms of an SDL specification, which is first translated to...
Nowadays, the creation of custom electronic devices of varying degrees of complexity is available for a wide audience. The applications vary from simple devices such as clocks and weather stations to automated homes and manufacturing control systems. In the last decade, the Arduino platform [1] has significantly simplified the development...
This paper presents a comparison of ELMO-based models. The comparison was performed on data in the Russian language for the task of named entity recognition (NER). The paper also discusses a comparison of the architectures based on the Simple Recurrent Unit (SRU) and Gated Recurrent Unit (GRU). All the models...
This paper describes a pipeline for extracting the author’s terms and definitions from mathematical texts. We used two models: one, for detecting mathematical formulas to clear text from noise and the other, for converting images into LaTeX formulas to restore the deleted formulas. Experimental data show that noise clearing is...
The paper is devoted to the development of two new cellular automata models of phase separation with synchronous and asynchronous modes. Cell transition functions with integer alphabet of states for these models are formulated. Their sequential and parallel program implementations based on the library of cellular automata topologies have been...
A two-dimensional asynchronous cellular automaton covering the cellular array with a maximum number of domino tiles is considered. For the purpose of parallel implementation, a transition to the synchronous operation mode was made. The paper presents asynchronous and synchronous cellular automata implementations. Their evolution and performance characteristics are analyzed. It...
The paper presents new software named Cellular Automata Topologies Library (CATlib). It includes a set of system routines written in the C language, and can be used by application programmers to programmatically implement CAE systems that use the necessary cellular automata as solvers. The CATlib software contains three subsets of...
Fault tolerance support automation is a relevant problem, because it is both demanded for large scale computations and hard to implement manually. General approaches exist, but they lack efficiency which is required in high performance computing as compared to particular approaches, which exploit peculiarities of subject domain and applied algorithm...
A stochastic iterative algorithm for solving the elastostatics Lamé equation in a two-dimensional domain is suggested. The Dirichlet boundary value problem for a system of two coupled second order elliptic equations for the displacement vector components is considered. We approximate the Lamé equations with finite differences and transform the resulting...
This paper describes the experiments for the task on information extraction from news texts in Russian in a setting with a wide variety of types of entities and relations. We have adapted the SpERT model which uses the BERT network as a core for the joint extraction of entities and...
The paper considers the problem of evaluating the possibilities of alleviating the transportation discrimination of the population of Asian Russia. The authors suggest extending the MIX-PROSTOR system for transportation stream modeling by including tools for evaluating the options of multimodal passenger transportation.
The paper is devoted to modern trends in the application of functional programming to the problems of organizing parallel computations. Functional programming is considered as a meta-paradigm for solving the problems of developing multi-threaded programs for multiprocessor complexes and distributed systems, as well as for solving the problems associated with...
Entity alignment algorithms aim to find equivalent entities in cross-lingual knowledge graphs, which is important for the task of obtaining information about real-world objects. Recently, several studies have been conducted on entity alignment algorithms on various datasets. Algorithms using information about entity names have shown a wide range of results...
One of the most significant drawbacks of the PCISPH algorithm (predictive corrective SPH), which is often used for the simulation of incompressible viscous liquid dynamics, is the complexity of the organization of distributed calculations on a computational cluster. At the same time, the algorithm supports the data parallelism relative to...
When published on the internet, cassettes can be used by various information systems needing this information block. This mechanism gives us the opportunity of a flexible system configuration and a realization of distributed information systems.
This approach was implemented in the information systems created by the A.P. Ershov Institute of...
Nowadays, entity resolution is being intensively investigated in the context of the integration of heterogeneous data sets. Collecting data from heterogeneous data sets and integrating them in a query able environment increases completeness and correctness as well as ensures a more effective analysis. Of special interest is the problem of...
In this paper we report on new black-box and white-box approaches implemented in ksmt-solver for checking satisfiability of non-linear constraints over the reals. These approaches are applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and beyond. A prototypical implementation has been evaluated...
In this paper, we deal with event-oriented models of concurrent processes which are generalizations of the well-studied model of prime event structures. In particular, we translate flow event structures into structures for resolvable conflict (the most expressive event-oriented model) and back, define two structurally different methods of generating transition systems...
We consider the time Petri nets (an extension of Petri nets), where every transition has its time interval. The policies of time-elapsing and the memory policies define different semantics for time Petri nets. The decidability of many standard problems with an infinite discrete structure depends on the choice of semantics...
The most important and cryptographically significant goal of a stream cipher is to produce a pseudorandom sequence of bits or words using a fixed length secret key, often paired with a fixed length public initialization vector. Over the last three decades of research and development in stream ciphers, a number...
When constructing a Cellular Automata (CA) model of a natural process one meets a problem of determining scaling relations, i.e. the quantitative relationships between the CA dimensionless parameters and corresponding values characterizing the prototype process given in terms of a physical system of units. The problem has no general solution...
In this paper, we propose an approach to constructing the user interface to be based on the ontological description. Its advantages are pondered. The main value using the ontology is the reduced complexity and development time as well as the increased quality of resulting implementation. The requirements to a system...
This paper presents the results of mathematical modeling of the problem of elasticity theory. The problem consists in the calculation of a model problem in a two-dimensional formulation aimed at finding the displacements around a crack.
This paper presents a computer-aided simulation to calculate the heating of a tungsten plate with different crack geometries forming in the process of a pulsed thermal load. The results of model testing, numerical calculations and comparison with experimental data are presented. The dependence of the surface temperature on the location...
This paper presents the results of a research into the anisotropy factor introduced by the hexagonal structure of a cellular array in a discrete model of a gas-powder flow with an integer alphabet and a hexagonal neighborhood structure at the stage of calculating the average values of pressure and flow...
The paper proposes an efficient parallel implementation of the Ramalingam algorithm for the dynamic update of the all-pairs shortest paths of a directed weighted graph after deleting an edge. To this end, a model of associative parallel systems with vertical data processing (the STAR-machine) is used. With this model, the...
Presented in this paper are the software techniques to improve the performance of the Particle-in-Cell method for general-purpose computers equipped with processors like Intel Xeon/Nehalem or AMD Phenom. The software techniques include particle storing in cells in either fixed size array or list, field values kept together in one array...
An algorithm for tracking objects in a videostream based on the use of a hierarchical Bayesian network is proposed. A specific feature of the algorithm proposed is the use of multi-dimensional scaling, which made possible to significantly reduce the network training time. The algorithm is resistant to temporary monitored object...
In this study, the problem of the utility network design is treated by the hypernet approach according to the compatibility of different types of resources with allowance for their laying in the same track. Also, we study the reliability aspect of the designed utility network for obtaining the optimal laying...
The intention of this paper is to extend classical results concerning the relationships between K- and N-density to their generalizations and modifications in the framework of the class of relational structures with distinct, irreflexive relations on countable sets of systems events.
The Russian language has an inflective structure and does not have a strict word order, which generates processing problems such as part-of-speech homonymy. The paper addresses this issue. The existing approaches to resolving the morphological homonymy problem can be divided into the following groups: rule-based approaches, statistical approaches, machine learning...
We are considering the problem of the analysis of transport network development in the MIX-PROSTOR system. The “what-if” analysis allows for setting some variations of the network parameters and calculating their consequences. In a sense, we are trying to solve the inverse problem: what ranges of network parameter modification leads...
In the paper, variations of the strip-method are investigated. Namely, we considered variants based on using different matrices: Hadamard, Haar, Frobenius, S-matrices, etc. These variants of the strip-method were implemented. The main purpose is to study the quality of restoration of one-dimensional signals (images are not considered) for various matrices...
The purpose of this work is the development and search of the analysis algorithms for textural features and various orthonormal spectral decompositions of the images obtained by the transmission electronic microscopy. The research is carried out for the Institute of Solid State Chemistry and Mechanochemistry of the Siberian Branch of...
The paper presents a method of the development of operational semantics for imperative programming languages. It is based on the ontological approach to formal programming language specification implemented by information transition systems and conceptual transition systems. The method is illustrated by a fragment of the C language.
The increasing volumes of Internet information and rapid development of social networks make the problem of automated text processing more and more topical. We have studied the use of link grammar for the Kazakh and Turkish languages and considered the possibility of creating dictionaries in these languages and connecting them...
We suggest an approach to the resolution of context-dependent lexical and syntactic ambiguity in a framework of ontology population from natural language texts. We show that a set of maximally determined ontology instances can be represented as a Scott information system with an entailment relation as a collection of information...
The paper proposes an associative version of the Ramalingam algorithm for the dynamic update of the all-pairs shortest paths of a directed weighted graph after inserting an edge. To this end, a model of associative (content addressable) parallel systems with vertical processing (the STAR–machine) is used. The associative version of...
Due to a growing interest in chemical and biological phenomena, simulation of reaction-diffusion processes on micro-level becomes urgently wanted. Asynchronous cellular automata are promising mathematical models to be used as a base for creating computer simulation systems, which gives reason for the investigation of their capability. In particular, since the...
The area of wireless sensor networks (WSNs) has recently received a lot of attention. Nevertheless, the major problem is the finite electrical batteries in sensors, which prevents the wide use of WSNs. However, technologies of the wireless energy transfer may be applied to solve energy problems in WSNs with the...
The software of geographical information system for studying the Earth's natural disasters (GIS-ENDDB), focused on the research into the cause- and-effect relations of catastrophic events in the history of our planet, contains data on seismic activity of the Earth, heat ows, detailed relief, and anomalies of the gravitational field as...
This paper proposes an efficient parallel representation of the Ramalingam algorithm for the dynamic update of the all-pairs shortest paths of a directed weighted graph after deleting an edge. To this end, a model of associative parallel systems with vertical processing (the STAR-machine) is used. The associative version is given...
In this paper, we present the simulation of an abstract model of SIMD type with vertical data processing (the STAR-machine) on GPU with CUDA framework. There is a number of algorithms developed for the STAR-machine. The research conducted recently shows that such a model is extremely efficient when used to...
Neural network models for the analysis of the document ranking algorithms are proposed. The models use the Kohonen neural network and a multilayer perceptron. These models were verified using test data, and their application features were revealed depending on the input data.
The problems of programming memristor arrays (memristor crossbars) are considered. An estimate for the pulse width to set the desired memristor resistance (memristance) value is obtained. The implementation of the Winner-Take-All (WTA) neural network on the memristor crossbar and the NMOS transistors for binary images recognition is proposed. The proposed...
The methodology of the operational semantics development for programming languages based on the operational ontological approach, conceptual transition systems and CTSL, the language for the specification of such systems, is proposed. The development of operational semantics is illustrated by an example of procedural programming languages from the family MPL of...
Bodin has applied SPIN to solve puzzles like the Japanese river puzzle, an advanced version of the famous wolf-goat-cabbage puzzle. Defining a Promela model can become cumbersome and debugging can be very time-consuming, since SPIN does the syntax check (e.g. type checking) only at runtime and developers might have decided...
The paper describes the generalization of the summarization algorithm of Niraj Kumar. The method proposed in the article uses the Link Grammar Parser. Our investigations are oriented to processing news articles, reviews from social networks, etc. We consider the possibility of applying this algorithm to estimate the relevance of posts...
The paper discusses several subsystems of the MIX system aimed to support various experimental researches in the field of economic modeling. The ultimate objection for each of these subsystems is to provide means for what-if analysis, impact estimation of strategic move, and decision making. Based on a comparative analysis of...
The paper concerns a topical problem of System Informatics, namely, the study and development of the methods of analysis, comparison and formal definition of the programming paradigms. The importance of this topic arises from the increase in the number of new-generation programming languages oriented towards the application and development of...
Causal trees represented by Darondeau and Degano are one of the truly concurrent model for distributed systems and processes. The model is more basic than other truly concurrent models because it defines concurrency and causality with respect to a branch, but on the other hand it is more expressive than...
The problem of validation of standard mathematical functions and libraries is well-recognized by industrial and academic professional community but still is poorly understood by freshmen and inexperienced developers. The paper gives and discusses two examples (from the author's pedagogical experience) when formal specification and verification of standard functions do help...
We propose a novel notion of fluid bisimulation equivalence that allows one to compare and reduce the behavior of labeled fluid stochastic Petri nets (LFSPNs) while preserving their discrete and continuous properties. The underlying stochastic model for the discrete part of the LFSPNs is a continuous time Markov chain (CTMC)...
The paper gives the background and history of the foundation, in 1990, of the Institute of Informatics Systems, Siberian Branch, Russian Academy of Sciences (IIS SB RAS). The institute is rightfully considered the successor to the academic tradition of the Novosibirsk programming school created by Academician A.P. Ershov, head of...
The paper presents a new object model of domain-specific transition systems, a formalism designed for the specification and validation of formal methods for assuring software reliability. A formal definition of a model programming language is given on the basis of this model.
This paper describes approaches to the vocabulary normalization and cross-language identity resolution problems that arise when the LOD datasets are used to populate the content of scholarly knowledge bases. We have proposed several new heuristics, using additional information extracted from the full text sources of data. The first heuristics uses...
The paper describes the methods of comparison of the sentences in a natural language for estimation of their similarity. To solve this problem, it is possible to use the semantic-syntactical relations between words constructed by the software system Link Grammar Parser. The results of our research are planned to be...
The random-access machine invented by Aho, Hopcroft, and Ullman is one of the several known versions of abstract register machines, which are an important computation model. Using a formal framework developed for this architecture in our previous work, we consider a challenging example – a search program that computes the...
Successful development of the theoretical foundations of C program verification in the project C-light allowed us to address an interesting practical task. We would like to develop a self-applicable verification system for C programs. The first step towards this goal was a series of experiments to verify some fragments of...
The paper describes a method for construction and annotation of a cor- pus of short texts made up on the basis of Russian posts from Twitter. This corpus is intended to train a sentiment classifier that sorts the general topic texts into three classes: "positive", "negative", and "neutral". The corpus...
The paper discusses the problems of the development and maintenance of information systems on the basis of ontology and Wiki-technology. In particular, an approach including the method of constructing information systems using Wikitechnology and ontology of subject domain and the method of ontology extraction from the already existing Wiki-systems is...
Alias calculus was proposed by Bertrand Meyer in 2011 for a toy programming language with a single data type for abstract pointers. This original calculus is a set-based formalism insensitive to the control flow; it is a set of syntaxdriven rules how to compute an upper approximation aft(S, P) for...
Recognition of potential for protein-RNA interaction is an important problem in bioinformatics. The solution may present a clue for understanding gene regulation. Formalization of the problem leads to in silico search for a complex motif in the 15-letter UIPAC alphabet in RNA sequences considering their secondary structure. The genetic algorithm...
The paper presents information about the development of the Visual Graph system, its application area, as well as the main problems encountered during the system design and their solutions.
Two models of an artificial biological cell, built in a fine-grain structure, are presented. They can be elements of computing structures that mimic the properties of living organisms - growth, self-reproduction, self-healing. The models are built on the basis of the Parallel Substitution Algorithm, which is a spatial system for...
The CA-model was modified in order to take into account the birthrates seasonal dependency and the influence of water streams on movements of organisms. The model was verified within the production-to-biomass and the relative average quantity criteria. A difference in the verification results and the assessments of physical values is...
Simulating large-scale phenomena by Cellular Automata (CA) meets the problem of designing CA models that could be efficiently implemented on supercomputers with distributed memory. Since most of large-scale spatially distributed processes contain diffusion as a component which takes a significant part of computational time, the study of coarse-grain parallelization characteristics...
A two-layer cellular automata (CA) model of carbon monoxide (CO) oxidation reaction on platinum is developed and investigated. The reaction in non-equilibrium conditions can be accompanied by various spatio-temporal patterns such as surface waves, spirals and turbulences. A two-layer CA is a parallel composition of the two CA – the...
We consider the single-particle HPPrp Lattice Gas Cellular Automata for simulation of modeling wave processes. The HPPrp Cellular Automaton is defined on a two-dimensional square lattice. Each cell of the automaton contains particles of the two types: the moving particles and the rest particles. Inserting the rest particles leads to...
In this paper, we present a new network reliability measure that is useful to evaluate performance of ad hoc networks with imperfect nodes and perfectly reliable links. An ad hoc network is modeled as undirected probabilistic graph. A specific feature of our model is that a network contains initially excessive...
This paper selects constructions used in a group of algorithms for undirected graphs represented as a list of edges and their weights on a model of associative (content addressable) parallel systems with vertical processing (the STAR-machine). To this end, the paper first analyzes the implementation of the Prim-Dijkstra algorithm on...
Recently, hybrid (GPU-equipped) supercomputers have attained a very high performance level. The fact is, the solution of real physical problems with such supercomputers is restricted by the GPU programming complexity.
In order to simplify the development of high-performance plasma physics codes for hybrid supercomputers, a template implementation of Particle-in-Cell (PIC)...
We consider the application of wavelet transform and neural networks to solving the problem of defect detection (the lack of elements and the presence of adhesions elements) in multi-element photodetectors by processing their images. It is shown that both methods can be successfully applied to the detection of defects. Found...
An algorithm for counting the erythrocytes on low-contrast images of cytological preparations is proposed. The algorithm deals with low-contrast images: brightness histogram normalization, contrast stretching, and background alignment by the “top of hat” method. Erythrocytes are detected by the similarity criterion of reference samples and an area in the picture...
The MinCDE protein complex is present in Escherichia coli and some other bacteria. In vivo, the MinCDE prevents incorrect cell division. In vitro, the MinCDE forms the protein waves and some other patterns. Recently, a hypothesis has been proposed, which says that self-organization in the MinCDE system arises...
This work focuses on the analysis of online social networking services. We examine several formal definitions of various characteristics (numerical and structural) and introduce appropriate concepts, models and methods that could be useful for the analysis of information obtained from social networks. Preference analysis is proposed to be used to...
The paper describes a system of scientific research automation applied to the forecasting of the development of Russian core transport network. The process of formation, evaluation and analysis of forecasted variants is considered. The variants can be combined, which allows for the implementation of the concept of the situation room...
Abstract register machines are an important formal model of computation widely used for the modeling of many classes of computational algorithms and the analysis of their complexity. Despite the significance of this model, formal verification of general-purpose programs for abstract register machines has not been properly covered in the existing...
In this paper, we start with a motivation of the study of modal and/or description logics with values in concept lattices. Then we give a brief survey of approaches to lattice-valued modal and/or description logics. After that we study some methods of context symmetrization, because in our approach the description...
The paper selects constructions used to represent a group of algorithms for undirected graphs given as a list of edges and their weights on a model of associative (content addressable) parallel systems with vertical processing (the STAR–machine). To this end, the paper analyzes the implementation on the STAR–machine of classical...
Development of the C-light verification system is accompanied by various case studies. We have already demonstrated the applicability of our system to some examples from verification competitions. Those programs are connected to verification-difficult issues but, as a rule, they are represented by artificial or trivial pieces of code. Now we...
Sisal is a single-assignment language without side effects. Sisal supports error values and a flow data type and allows recursion. It has a verbose syntax, which reminds that of Pascal in some cases. Sisal is positioned as a language for scientific computations, implicitly parallel and effective. It can significantly simplify...
A new kind of labeled transition systems, program specific transition systems, is proposed. These systems are used to formalize and unify some aspects of program handling. Such aspects as the development of program operational semantics and proof of safety properties of programs are considered, and the appropriate classes of program...
In this paper, a formalization of the two-level mixed verification method of C-light programs, based on program specific transition systems, is suggested. Two kinds of such systems are used to formalize the method. The first kind, operational semantics specific transition systems, is used to specify the C-light mixed operational semantics...
This paper describes starting experiments on integration of semantic systems based on ontologies. The experiments are carried out with the help of a toolkit intended to simplify visual analysis and integration of data from different datasets. The toolkit comprises several tools for application-specific visualization as well. The Bone ontology and...
This work represents a survey of the social network analysis problem. There are four main approaches: structural, resource-based, regulatory, and dynamic. To solve the problems in social network analysis, the following methods are used: graph and stochastic models, models of network evolution, methods involving ontologies, structural and relational models, machine...
The paper discusses an experience of using the methodology for the development of knowledge portals which provide systematization and integration of scientific and engineering knowledge and information resources as well as the content-based access to them. To provide a sufficiently complete and consistent representation of knowledge and information resources, their...
This paper describes a new method of graph algorithm visualization based on a dynamic approach. Graph algorithms are algorithms processing graphs. The main advantages of this approach are the possibility to set an algorithm as an input parameter, to set the graph as an input parameter, and also to adjust...
In many tasks related to reasoning about consequences of a logical theory, it is desirable to decompose the theory into a number of weakly-related or independent components. However, a theory may represent knowledge that is subject to change due to execution of actions that have effects on some properties mentioned...
Design and Analysis of Computer Algorithms is a must of Computer Curricula. It covers many topics that group around several core themes including algorithmic design patterns (ADP) like the greedy method, divide-and-conquer, dynamic programming, backtracking and branch-and-bound. These design patterns are usually considered as Classics of the Past (going back...
The computational complexity of cellular automata (CA) is investigated. Using unified approach to the CA behavior, we define the notion of CA convergence and propose the measures of the time and space complexity. The approach to the complexity reduction for some classes of synchronous CA is discussed. Then we consider...
The cellular automata model of populations' dynamics of eight types of organisms is proposed and investigated. The results of two computational experiments of simulation of population density distribution over space are presented. The first experiment was carried out is for the case of the emergence fishes at outfall shoal of...
A concept of invariants in the cellular automata (CA) models is introduced, being defined as a dimensionless value that characterizes the process simulated by a CA evolution irrespective of the form of its mathematical representation. This paper is concerned with asynchronous CA-models (ACA-models), simulating reaction-diffusion processes, although it may be...
It is known that the Lattice Gas Automata (LGA) models simulate a sound wave process. Moreover, it is proved that the LGA model corresponds to the hyperbolic equation. The computer simulation show that a wave profile varies with time: the profile amplitude reduces, the profile width increases. This suggests that...
This paper proposes a technique to build the data structure for finding the second simple shortest paths on a model of associative parallel processors (the STAR-machine). It includes three associative parallel algorithms represented on the STAR-machine as the corresponding procedures. We prove the correctness of these procedures and evaluate their...
Petri nets are a research tool for systems consisting of interacting components. Petri nets are the most interesting in that they allow representation and studying the behavior of evolving parallel processes in a program or in a discrete device. Petri nets are used to describe an asynchronous composition of fine-grained...
Evolution of totalistic cellular automata (CA) with weighed templates are studied. As a result of simulation various stable patterns are obtained and investigated. Both synchronous and asynchronous modes of CA operation are tested. As a result of simulation by synchronous and asynchronous CA, different stable patterns emerging from one nucleation...
Analysis of a set of data space dimensionality reduction methods in image recognition problems is carried out. A problem of diagnosis of thyroid diseases with the use of images of cytological preparation is investigated. It is shown that the morphological image analysis combined with the method of diffusion maps makes...
Based on a scatterogram of projections onto a plane of states of the output and hidden layers of a sigmoid neural network, its behavior in solving the problem of image recognition of letters is studied. In particular, it was found that the method of conjugate gradients for the entire training...
This paper describes a new approach to the analysis and verification of imperative programs, which allows us to integrate, unify and combine the methods and techniques of analysis and verification of imperative programs, accumulate and use knowledge about them. A feature of the approach is to use the domain-specific language...
We examine a number of methods for probing and understanding a large-scale structure of networks that evolve over time. In particular, we focus on citation networks, networks of references between documents such as research papers. We describe three different methods of visualization: the first is based on a hierarchical edge...
We consider the well-known Sliding Window Protocol (SWP) which provides reliable and efficient transmission of data over unreliable channels. It seems quite important to give a formal proof of correctness for the SWP, especially because the high degree of parallelism in this protocol creates a significant potential for errors. However...
The paper describes an application of a variant of the Newton-Raphson method to solution of geometric constraint problems. Sparsity and rank deficiency of the corresponding nonlinear systems are emphasized and statistical data are presented. Several ways of handling underdeterminancy and overdeterminancy in solving the Newton linear systems are considered. The...
In this paper, a computer memory system intended for storing an arbitrary sequence of multidimensional arrays is described. This memory system permits parallel access to the cuts distinguished in a given array by fixing one of the coordinates and to a large set of parallelepipeds which are the same dimension...
The paper proposes an efficient associative algorithm for dynamic update of the shortest paths tree of a directed weighted graph after deletion of an edge. To this end, we use the STAR–machine that simulates the run of associative (content addressable) parallel systems of the SIMD type with bit–serial (vertical) processing...
We start with a “make easy” approach to popularize formal semantics for software engineers. It is based upon a toy language with “exoteric” operational, denotational and axiomatic semantics. Then we present a realistic and practical operational, denotational and axiomatic semantics for a simple programming language. We hope that our approach...
The algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC) enriched with iteration. In this paper, a method of modeling and performance evaluation of concurrent systems in dtsPBC is outlined based on the stationary behaviour analysis. The method is then applied to the generalized shared...
The Atoment language is a domain-specific language of development for program verification methods. It is used in the multilanguage software system Spectrum of rapid development and testing of verification methods. The easy-to-use specialized language allows a user of the system to describe verification methods in a natural notation, verify algorithms...
The process of development of an ontology-based knowledge portal and creation of its content is time-consuming and laborious. The lifetime of such portals is sufficiently long and they collect a great volume of valuable information. This information can be analyzed from various points of view. This paper describes an extension...
In the paper, we give an overview of several approaches that we use to analyze “spam” (undesired bulk advertising) and the credentials of senders of spam, for the purpose of automatic detection. We use some of these approaches for discrimination between stolen account credentials and “spam-bots” (accounts opened purely for...
In this paper we use compositional methods for construction of a characteristic formula for the timed testing preorder in a model of timed event structures with discrete internal actions.
Timed transition systems are a widely studied model for real-time systems. In this work we deal with an extension of this model, timed transition systems with invariants. The intention of the paper is to show applicability of the general categorical framework of open maps in order to treat the decidability...
This work is dedicated to an actual problem of efficient information search in the Internet. The work is based on the algorithms of sentences comparison taking into account the schemes of syntactic analysis generated by Link Grammar Parser software. The main idea is that syntactic diagrams give us a primitive...
In the last 5 years, multi-core processors become more and more available to the wide public. Support for multi-core processors becomes de facto a standard for computation-intensive applications. In this paper, we present a parallel implementation of the UniCalc solver for non-linear engineering problems. Unlike the existent solvers of non-linear...
The classical Hoare logic links separate verification conditions (VCs) to linear paths of a program. The real verification condition generators (VCG) link VCs to line numbers at best. It can be insufficient, since VCs contain information neither about the evaluation order nor about correspondence between their fragments and specific operations...
A verifying compiler is a system program that translates programs written by an user from a high-level language into equivalent executable programs, and besides, proves (verifies) mathematical statements specified by the human about the properties of the programs being translated. The purpose of the F@BOOL@ project is to develop a...
For a discrete time stochastic extension dtsPBC of finite Petri box calculus (PBC) enriched with iteration, we define a number of stochastic equivalences. They allow one to identify processes with similar behaviour which are differentiated by the too discriminate semantic equivalence of the calculus. We investigate which is the weakest...
Time Petri nets with priorities are a widely studied model for real-time systems. The intention of the paper is to develop an algorithm for parametric timing behaviour verification of real-time and concurrent systems represented by prioritized time Petri nets (PrTPNs). To achieve the purpose, we introduce a notion of the...
The paper presents an approach to development of a system that supports decision-making for tasks aimed to reduce power consumption and enhance the environmental safety of a large-scale enterprise with a complex technological infrastructure. The architecture and operating principles of this system are discussed. Adjustment of the system to the...
This paper concerns the development of techniques for the cellular automata simulation on triangulation grids on at and curved surfaces. The possibility of the proposed techniques are shown on examples of the cellular automata simulation of diffusion, front propagation and diffusion-limited aggregation.
An overview and experimental comparative study of parallel algorithms of asynchronous cellular automata simulation are presented. The algorithms are tested for physicochemical process model of the surface reaction CO + O2 over the supported Pd nanoparticles on different parallel computers. For the testing, we use shared memory computers, distributed...
For simulating CO catalytic oxidation on platinum-group metals, kinetic asynchronous cellular automata (CA) (asynchronous CA with probabilistic transition rules) are used being sometimes referred to as Monte Carlo methods. In this paper, the influence of the rate coefficients values of oxygen adsorption and carbon monoxide absorbtion on the reaction rate...
Two new cellular-automata models of the diffusion process are pro- posed. They are based on integer states of cells instead of Boolean ones in the known models: asynchronous naive diffusion by Toffolli and block-synchronous Margolus diffusion. Computing experiments have been carried out with these models; they demonstrate a good correlation...
The paper proposes an efficient implementation of the Ramalingam algorithm for dynamic updating the single-sink shortest-paths subgraph of a directed weighted graph after insertion of an edge using a model of associative (content addressable) parallel systems with vertical processing (the STAR-machine). An associative version of the Ramalingam incremental algorithm is...
The importance of a proper selection of data structures can hardly be overestimated. It is crucial for the overall performance in certain problem domains, such as file systems, task and memory managers in operating systems, indexing in the DBMS, dictionaries in compression utilities.
By now, supercomputers have become an efficient tool of mathematical simulation for both scientific and applied large-size problems. This makes it possible to thoroughly analyze such physical processes that otherwise could be too costly or even prohibitively expensive or time consuming to be analyzed in a usual way. This tool...
A parallel algorithm for solving the traveling salesman problem by the recurrent Wang neural network in conjunction with the WTA (“Winner Takes All”) principle is proposed. This algorithm is preferable when it is necessary to solve the problem with sufficient accuracy in a lesser time.
An analysis of a thermal image (thermogram) of a human body surface shows the availability of correlation between the body state and the thermogram heterogeneity (“motley”). A new method for the quantitative analysis of the thermogram heterogeneity based on the thermogram representation by a quadtree of reduced images is proposed...
An approach to the development of easy-to-use operational specifications of dynamic systems is presented. It is based on the formalism of context machines and the language of description of context machines CML. The main notions of the theory of context machines are defined. Classification of general-purpose contexts is suggested. The...
The process of development of an ontology-based knowledge portal and creation of its content is time-consuming and labor-intensive. It is very desirable to have special analysis facilities for maintenance and development of such a portal. The subject of our paper is a tool for visual analysis of content and ontology...
The behaviour of concurrent systems is often specified extensionally by describing their “state-transitions” and the observable behaviours that such transitions produce. The simplest formal model of computation able to express naturally this idea is that of labelled transition systems, where the labels on the transitions represent the observable part of...
An acute problem for archives and museums is providing high-quality digitized text from low-quality or damaged originals. The majority of companies working in the field of optical character recognition (OCR) focus on digitzed texts of high quality, which represent the majority of processed data and the market for these companies’...
In this paper, by means of an abstract model of the SIMD type with vertical data processing (the STAR{machine), we present basic associative parallel algorithms. These algorithms are represented as the corresponding procedures for the STAR{machine, whose correctness is justified and the time complexity is evaluated. We also propose a...
The paper describes a programming interface that we have developed to separate constraints, solvers, and cooperation strategies in a constraint programming toolkit UniCalc. The interface is simple but it allows us to express such constraint solving techniques as increasing the level of consistency, various strategies for exhaustive search, and cooperation...
The fully automatic verification of programs is a tempting and hardly accessible goal of modern programming. The low-level nature of the most popular programming languages, such as C and C+, has raised its difficulty to a new level. New formal methods and specification languages are required, because the classical Hoare...
Logical semantics is a new kind of formal semantics used to describe semantics of pure call-by-value functional languages. For the statement S, the logical semantics LS(S) is a predicate that is true for the variable values for which the execution of S is finished. Let a specification of the statement...
The purpose of the F@BOOL@ project is to develop a transparent for users, compact, portable and extensible verifying compiler F@BOOL@ for annotated computer programs, that uses effective and sound automatic programs for checking satisfiability of propositional Boolean formulas. The kernel programming language of the project interprets all variables by residuals...
In the paper, the algorithm of the hierarchical cluster analysis is considered and the method is proposed to transfer this algorithm onto the parallel multiprocessor system used on modern graphics processing units (GPUs). Within the frameworks of some natural assumptions, we have estimated the run time of the algorithm in...
A three-stage method of C program verification is presented. It is a further development of the two-stage method in the framework of the C-light project. An additional stage of normalization of C-light programs is introduced and optimization of the two-stage method caused by this introduction is considered.
During the semicentenial history of Computer Science and Information Technologies, several thousands of computer languages have been created. Computer language universe includes languages for different purposes: programming languages, specification languages, modeling languages, languages for knowledge representation, etc. In each of these branches of computer languages it is possible to track...
Nets of active resources (AR-nets) are presented. This formalism has the same expressive power as Petri nets but a different syntax: the model is not a bipartite oriented graph, but an oriented graph with two types of arcs (consumption and production). Direction of the arc denotes active and passive participants...
Formal models for real-time systems have been actively studied over the past several years. Much of the theory of untimed systems has been lifted to the real-time setting. An example is the notion of trace equivalence applied to timed transition systems with invariants which is studied here within the general...
Problems related to reflection of some algorithms of image processing onto multiprocessor systems are investigated. In particular, algorithms of allocation of contours, such as the gradient method and the combinatorial method (the method of the threshold gradient), are considered. In view of complexity of the algorithm of searching objects on...
Structures of data and ontology arising in information systems containing facto-graphical data are considered.
We propose an efficient parallel implementation of the Ramalingam algorithm for dynamic updating the single-sink shortest paths subgraph of a directed weighted graph after deletion of an edge on a model of associative (content addressable) parallel systems with vertical processing (the STAR-machine). The associative version of the Ramalingam decremental algorithm...
In the paper, a natural class of logical calculi is fixed for which we formulate the notion of a Δ -decomposable set of formulas. We demonstrate that the property of uniqueness of signature decompositions holds in those calculi of this class that have the Craig interpolation property. In conclusion, we...
Algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC) enriched with iteration. In this paper, we define a number of stochastic equivalences for dtsPBC which allow one to identify finite and infinite stochastic processes with similar behaviour. A problem of preservation of the...
A Cellular Automaton (CA) is nowadays an object of ever growing interest as a mathematical model for spatial dynamics simulation. Due to the CA ability to simulate nonlinear and discontinuous processes, it is expected to become a complement to partial differential equations. Particularly, the CA may be helpful when there...
We consider a market model, which has arised under conditions of the paid usage of CPU time. A new algorithm for calculating the price of the local (for one processor) equilibrium is offered under the assumption that the users' preferences are described by the Cobb-Douglas utility functions. An example shows...
For implementation of pseudo-random number generators (PRNG), a linear congruential generator (LCG) is the most frequently used algorithm. The techniques to increase the efficiency of the LCG based on 64-bit integers and bit-wise operations are studied. The efficiency of the LCG implementation with the techniques proposed is experimentally tested.
For simulating physical and chemical processes on molecular level, asynchronous cellular automata with probabilistic transition rules are widely used being sometimes referred to as Monte-Carlo methods. The simulation requires a huge cellular space and millions of iterative steps for obtaining the CA evolution representing a real scene of the process...
Two statistical lattice models of a 3D crystal are proposed, which allow us to take into account a change in the shape and in the surface morphology of a nanoparticle under the influence of the temperature. It has been shown that consecutive diffusion of atoms does not give reasonable simulation...
The Lattice Gas Automata (LGA) models are based on a microscopic model of physical process being simulated and can be considered as an adjunct to the traditional numerical methods to the spatial dynamics simulation. Here we consider two simple LGA models: HPP and HPPRP. They are based on a square...
An extension to the Lattice-Gas Boolean models up to integer values of the particle velocity vectors is proposed. A new FHP-MP model is featured. Experiments on simulation of a fluid using the new model were carried out. The comparison with the known results is made.
The problem of smoothness of adaptive meshes produced by the Self-Organizing Maps is considered. It is shown that to improve the mesh smoothness, it is necessary to increase the learning radius. This leads, in turn, to the border effect. The main goal of this paper is to develop a technique...
In this paper, we propose an extended version of the associative graph- machine. Then we offer efficient algorithms for implementing the second group of relational algebra operations that consists of operations Product, Join, and Union. The proposed algorithms are represented as the corresponding procedures for the AG-machine. We prove their...
A new method is proposed to reduce non-physical effects in the PIC method. The method is demonstrated on an example of simulation of recombination of positive and negative ions in the radio frequency (RF) discharge.
In discharges in electro-negative gases, the negative ions are generated by dissociative attachment and lost...
Algorithms for mapping a weight matrix of a neural layer onto distributed computer systems with a torus structure are proposed for parallel image processing. It is shown that the choice of the mapping technique depends upon the ratio between the number of neurons and the number of weight coefficients in...
A new class of transition systems, ontological transition systems is presented. They enrich transition systems with ontological entities. In the framework of development of a language of ontological transition systems OTSL, a sublanguage of formulas is defined. Formulas are used to specify ontological entities of ontological transition systems.
Ontological transition systems are a method of specification of computer systems which integrates operational and ontological approaches to specification of these systems. In the framework of development of a language of ontological transition systems OTSL, a sublanguage of actions is defined. Actions are used to specify transitions in ontological transition...
We address a problem of efficiency of verification condition generation for unstructured non-deterministic imperative programs. Importance of the study is based upon two arguments:
The paper describes an approach to visualization of solution spaces in computer modeling problems. The advantage of the approach is that it is applicable to visualization of solution spaces of arbitrary spatial structure (e.g. consisting of multiple components, containing cuts, accumulation points, etc.) An implementation of the approach is built...
It is well known that parameterization is a powerful tool for creation and reuse of models. It allows us to construct models with predefined features, as well as to form new models by modification of parameters of already existing models. These opportunities are crucial for engineers and other CAD users...
The transitive closure (or reachability) problem in a directed graph consists in finding whether there is a path between any two vertices. In this paper, we first study the problem of parallelization of Italiano's algorithm for dynamic updating the transitive closure after inserting a new arc into the graph represented...
This paper introduces the notion of decomposability in an extension and relative decomposability for first-order theories. We describe several basic facts connected with these notions and formulate a criterion of relative decomposability.
The evolution of formal methods allowed us to overcome many obstacles in verification of procedural programs. However, wide spreading of object-oriented languages has brought new challenges, even in the case of sequential programs. These problems were thoroughly examined by ESC/Java and Spec# teams in their papers [10, 12], though in...
The paper presents an approach to document analysis adaptable to a certain genre of the document and subject domain. The approach is intended for updating a database of an information system by means of information obtained by automated analysis of electronic documents. This approach implies using linguistic knowledge about the...
Methods for analysis of texts and separate sentences in a natural language are under discussion. Their main application is to study a written speech with the help of mathematical logic, syntactic rules and the morphology of the modern Russian literary language. Various algorithms for matching predicates and formulas of first...
A class of asynchronous cellular automata (ACA) whose evolution simulates physicochemical kinetics of nano-systems is defined. It is characterized by multicell probabilistic transition rules and stochastic character of their application. To simulate real processes in real time ACAs should have huge cellular arrays and a very long evolution. So, the...
In this paper, we consider Computational Grid as market of the two commodities: CPU time and disc storage. Market agents are suppliers and users (consumers). The suggested market model refines the model proposed by R. Wolski et al. For the refined model, we discuss the possible application of the priceadjustment...
The Lattice Gas Cellular Automata (LGCA) models can be considered as an alternative to the conventional approach to the spatial dynamics simulation. The LGCA is based on a microscopic model of a physical process being simulated. Here we consider two simple LGCA models: HPP and HPPRP. They are based on...
Associative (content addressable) parallel processors of the SIMD type are ideally suited for performing fast parallel search operations being used in different applications such as graph theory, computational geometry, relational database processing, image processing, and genome matching.
The Delaunay Tessellation is used to construct a cellular automata resembling model based on data obtained from molecular dynamics experiment. Particle coordinates at each time step of required length are tessellated to compose a system of vertices and edges, which are classified to produce states and transitions. These states and...
A neural network algorithm is proposed for automation of cytological diagnostics of follicular tumors of a thyroid gland by images of an intraoperative material. Experimental results show the algorithm efficiency for constructing a medical expert system.
In the simulation of a protoplanetary disc with a power law density profile, a disc instability is detected. The instability arises only with a power law profile and is affected by the power index. Thus, the impact of initial density profile is large within the employed numerical model.
An effective algorithm is proposed for a balancing computation load in a heterogeneous multicomputer system by the self-organizing neural Kohonen network. The algorithm takes into consideration different performances of the system processors.
The paper is contributed to study an operator for refinement of actions to be used in the design of concurrent real time systems. The refinement operator replaces actions on a given level of abstraction by more complicated processes on a lower level. We define this operator on a causality based...
In this article we consider requirements to visualization of semantic properties of programs appearing in the reengineering process when use of hierarchical ordering is an appropriate way to visualize the information of interest. We consider two algorithms of graph placement that implement geometrical inclusion of object hierarchy. They use (non)slicing...
In this paper we present a linear constraint solver for the UniCalc system, an environment for reliable solution of mathematical modeling problems.
The paper presents a model of adaptive behavior of an autonomous adaptive agent (an artificial organism) based on the semantic probabilistic inference and the functional system theory by P.K. Anokhin. The main distinction of this model is the possibility for automatic generation of new subgoals, which allows us to solve...
A timed extension of weak trace equivalence is developed for a model of timed event structures. Moreover, a category-theoretic characterization of this equivalence based on a span of open maps is specified. Finally, the problem of decidability of weak trace equivalence is solved in the setting of finite timed event...
Finding shortest paths in a weighted graph is a fundamental and well studied problem in computer science. Such a problem arises in practice in different application settings.
This paper considers theoretical background and experimental compar- ison of two approaches to automatic recognition of tabular property of superintu- itionistic logics. A principle opportunity for automatization is based on theoretical results of L.L. Maksimova that were obtained in 1973{2003 and their algorithmic interpretation that was developed recently by P.A...
The paper describes equivalent transformations of Sisal 3.1 language structures in detail. The programming language Sisal 3.1 is based on Sisal 90. Transformations are aimed to to decomposition of complex language structures into more simple ones that can be directly expressed by an internal representation IR1 based on an intermediate...
In the last decades, a number of stochastic enrichments of process algebras was constructed to specify stochastic processes within the well-developed framework of algebraic calculi. In [26], a continuous time stochastic extension of finite Petri box calculus (PBC) was proposed and called sPBC. The algebra sPBC has...
The paper presents an improvement over traditional SSA form, called partial SSA that features only partial translation of a program into the singleassignment state. Partial SSA is more compact than the traditionally used full SSA while it suits well most program optimization algorithms. The paper introduces formal quality criteria for...
This paper presents an approach to the development of specialized Internet portals providing content-based access to systematized knowledge and information resources, relating to a certain branch of science. The information basis of such portals is formed by ontologies, containing the description of scientific and research activity as a whole as...
Parallel programs often are non-deterministic in their nature, what greatly complicates testing, debugging, verifying and analyzing such programs. On a uniprocessor, interleaving actions of the system scheduler (thread switches) can be thought of as source of nondeterminism. The precise detection of these actions helps many tasks, especially the schedule-based execution...
In this paper, we propose an efficient associative parallel algorithm for updating tree paths after every change in the underlying graph. Such a problem arises when we perform dynamic graph algorithms. To speed up time complexity of the algorithm, we use a new associative model called associative graph machine (AG-machine)...
In order to extend the area of application of the symbolic verification method [19, 20, 21, 22, 23], definite iterations over tuples of altered data structures are introduced and reduced to the standard definite iterations. This reduction is extended to definite iterations including the exit statement. The generalization of the...
Cooperative constraint solving is an area of constraint programming that studies the interaction between constraint solvers with the aim of discovering the interaction patterns that amplify the positive qualities of individual solvers. Automatisation and formalisation of such studies is an important issue of cooperative constraint solving.
In this paper, we...
Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. The paper suggests a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the propositional μ-Calculus.
The history of development of the SSCC computer resources and the organization of solving large-scale modeling problems are considered. The results of the project for the development of a multicomputer system SIBIR in the 80-s, the current SSCC structure, the main results of its operation in 2004, and prospects for...
The architecture of an innovative portal based on a fine-grain modularity and an assembly technology is presented. The portal resources and services for the interaction between participants of the innovative activity within a common information space are realized. The investigation of the system and the creation of its prototype have...
The basic means and methods to increase the efficiency of the sequential numerical simulation programs are considered. The main components of the modern hardware and software which affect the programs efficiency are discussed. The most important guidelines and advices for application programmers are outlined.
With evolution of mathematical modeling and creation of high-performance computer systems, many scientific applications have appeared, demanding an increase in computational performance higher than any of available supercomputers can provide.
The new parallel algorithm has been developed and implemented for solving the axially symmetric problem of the interaction of a plane shock wave with a free bubble system (cluster) resulting in the formation of a stationary oscillating shock wave. The important characteristics of the problem in question, such as acceleration...
This paper considers aspects of parallelizing of the solution process of problems of the integer linear and quadratic programming as well as of problems of global optimization of the non-convex quadratic programming.
The experimental library PLVIP for parallel image processing, elaborated and implemented in the Image Processing Laboratory of the ICM&MG SB RAS is described. The library is built on the vertical processing principle and is installed on the multiprocessor computers of the Siberian Supercomputer Center, MVS-1000/M and RM600-E30. The basic characteristics...
By now a substantial body of literature has evolved which deals with the numerical simulation of the 3D convective currents in the Earth’s mantle (see, e.g., [1–4] and references therein). A crucial point is to estimate the reliability of numerical experimental results because the similarity principle fails when the dynamical...
With MVS-1000M the distribution of particle and gas density in the soliton were investigated, as well as their velocities, angular momentum, flow of gas and particles through soliton and vorticity of particle velocity. It is shown that in the soliton the high values of gas and dust densities and gas...
The Parallel Substitution Algorithm (PSA) is a spatial dynamical system used to represent processes in cellular space. The PSA is applied to designing programs of self-replication in cellular space. The programs become more laconic (by the number of transition rules or substitutions) in comparison with the ones based on the...
Methods of Cellular Automata (CA) composition are systematically considered and analyzed. To formally define them some basic mathematical operations on cellular arrays are introduced. Trivial sequential and parallel composition types with no shared variables in cell transition functions are given in brief. The main concern is with two basic methods...
This paper describes the experience gained in the development of PABX monitoring system using the Internet-technologies. The basic attention is being given to the formal representation of data accounting, storage subsystems and access to data. Information about the system realization is given, and the user interface is described.
This paper presents the review of the network monitoring technologies that now are widely used. The main attention is given to MRTG, NETMON and NFC&NDA systems. The paper describes their advantages, configuring parameters and a necessary programming base. The experience of using these systems for monitoring the NSCnet network is...
With evolution of mathematical modeling, and with creation of high-performance computing systems, many scientific applications have appeared, demanding ever increasing computer costs, which are higher than any of available supercomputers can provide.
This paper is oriented to the cellular pipelined algorithm architecture for the 1D diffusion simulation. The finite difference representation of 1D diffusion is written in terms of the residue number system. The cellular pipelined algorithm architectures for the main operations with a minimum period are developed. The parallel Substitution Algorithm...
In this paper we describe in detail a new technique for updating tree paths on a model of associative parallel systems with vertical data processing (the STAR-machine). It includes a new associative parallel algorithm for finding an MST along with the matrix of tree paths and a new associative parallel...
This paper presents a Dynamically Configurable Modular System (DCMS), which is a library for the development of applications with an open architecture. The DCMS is oriented to a wide set of applications, such as mathematical simulation, Web technologies, and so on. By now, the library has been used in the...
An algorithm for the real-time image rotation on the array microprocessor NM6403 is proposed. For implementation of this image transformation on the microprocessor NM6403, decomposition of a rotation matrix is used. This decomposition reduces any pixel rotation to a sequence of unidimensional translations which can be effectively vectorized.
A new language of finite state machines called USL is proposed. The language is intended for rapid development of formal verification-oriented operational semantics of modern programming languages. Formal operational semantics of the USL language is defined. The USL-based approach to programming language semantics design is illustrated by the example of...
In this paper, we try to decide a problem of recognising timed testing equivalences for timed event structures with dense internal actions. For this purpose, we construct a formula that characterizes a timed event structure up to the timed must-preorder. So, to understand if two timed event structures are...
We study the model checking problem for fixpoint logics in well- structured multiaction transition systems. P.A. Abdulla et al. (1996) and Finkel & Schnoebelen (2001) examined the decidability problem for liveness (reachability) and progress (eventuality) properties in well-structured single action transition systems. Our main result is as follows: the model...
A new three-level approach to sequential object-oriented program verification is presented. It is applied to a significant С# subset called C#-light that includes all principal sequential С# constructs. At the first stage, C#-light is translated into an intermediate language C#-kernel that allows us to simplify axiomatic semantics. At the second...
This work considers a model of a multilevel information system that integrates heterogeneous classes of objects of different configuration and complexity range. The architectural solution is suggested that allows dynamical extension of a working system by connecting objects both of existing classes and new classes as well. The use of...
Stochastic Petri nets (SPNs) is a well-known model for quantitative analysis. We consider the class called DTWSPNs that is a modification of discrete time SPNs (DTSPNs) by transition labeling and weights. Transitions of DTWSPNs are labeled by actions that represent elementary activities and can be visible or invisible for an...
It is shown in the paper that state-based algebraic semantics of an imperative program can be regarded as a compiler abstract model and can serve as a good assistant of the compiler designer.
Since Cellular Automata attract a growing interest as a model to be used in simulating spatial dynamics, the problem arises of Boolean data compatibility with continuous spatial functions widespread in physics. To solve this problem, a method to approximate real functions in discrete space by Boolean arrays and vice versa...
In this paper, we propose a novel associative parallel algorithm performing depth-first search on an abstract model of the SIMD type with vertical data processing (the STAR-machine). This algorithm is represented in two ways: as recursive and non-recursive STAR procedures, whose correctness is verified and time complexity is evaluated.
In this paper, computational potentialities of the residue number system for solution to the diffusion equation is investigated. The finite-difference diffusion scheme is modified in terms of the residue number system. Computer simulation has been performed. The computational characteristics (stability, accuracy) have been assessed and compared with similar ones obtained...
We have developed a hybrid procedure based on the Godunov algorithm for computing eigenvectors of tridiagonal symmetric matrices and inverse iteration, which we call the Godunov-Inverse Iteration algorithm. It employs the inverse iteration to improve the accuracy of eigenvectors computed according to the Godunov method with the embedded Modified Gram-Schmidt...
In this paper, the boundary conditions of 2D and 3D Cellular Automaton models (CA models) are considered and classified. It is shown that the simulation algorithm does not change at different boundary conditions, and the computing complexity of simulation is not increased with a large number of wall cells, even...
In this paper, we propose a new implementation of Dijkstra's shortest path algorithm on a model of associative parallel processors with the vertical data processing (the STAR-machine) to obtain for every vertex of a directed graph the distance along with the shortest path from the source vertex. We prove correctness...
A model of self-gravitating system is described. Present parallel programs implementation of such a model are reviewed in brief. Numerical algorithm is described. The parallelization technique and load balancing strategy are discussed in detail. The parameters of test computations that meet the requirements of the problem of protoplanetary disc simulation...
An approach to mapping structure of parallel program onto structure of distributed computer system by the Hopfield neural network is presented. For typical structures of parallel programs ("line", "ring", "mesh", "binary tree") and regular structures of distributed CS ("torus", "hypercube") it is shown that fuzzy control of derivative of neuron...
Technological aspects of parallelization of the computing system "Potok-3", intended for some numerical modeling of problems of aerodynamics and physical gas dynamics are considered. The methods and problems of global parallelization of a multi-program complex by major parameters, as well as C -, L- and V-types of the parallelization procedures...
The intention of the paper is to extend the testing methodology to true concurrent models with a dense time domain. In particular, we develop three different semantics, based on interleaving, steps, and partial orders of actions, for testing equivalence in the setting of timed event structures. We study the relationship...
We present a graph drawing algorithm that was developed for real-life call graphs, data flows and class hierarchies. The algorithm is an extension of the hierarchical layout method of Sugiyama. The main difference is that we achieved an orthogonal layout with the maximum number of edge bends equal to 2...
In the paper, we construct a formula that characterizes a timed event structure with discrete internal actions up to the timed must-preorder.
A complex programming system may have a large number of parameters controling its configuration and behavior. The editing, programmatic access, packaging and upgrade of these parameters may become a complicated and time-consuming task. We present a component called Dialogic, which stores options as a strictly typed XML structure and automatically...
Testing strategies based on finite states machines (FSMs) are widely used for protocol test derivation. Most FSM-based methods of test generation are based on the well-known W-method. In this paper, we determine the necessary conditions for a test suite to be complete under an assumption that only the number...
Maintenance and transformation of large program systems require means for com- prehension of their data dependences. We consider facilities for data flow visualization implemented in the RescueWare® system — a workbench for modernization of legacy systems. One of the key points in the process is the user-guided identification and extrac-...
In this paper, we present a study of the definability properties of fixed points of effective operators on abstract structures without the equality test. In particular, we prove that the Gandy theorem holds for the reals without the equality test. This provides a useful tool for dealing with recursive definitions...
The methods of compiler (and converter as a special case) development are sufficiently investigated and described. There are a number of converters from the standard Pascal language to C/C++ languages.
In this work, some translation schemes (that are of theoretical interest, in the authors’ opinion) elaborated for a converter from...
The Supercomputer Software Department (SSD) of the Computing Center SB RAS (at present Institute of Computational Mathematics and Mathematical Geophysics), Novosibirsk, was founded on April 1, 1987 on the base of System Software Laboratory and Research Group of Parallel Program Synthesis. The goal of this alliance was the actualization of...
The Parallel Substitution Algorithm -- a spatial model used to represent cellular computations -- is applied to designing self-replicating structures in cellular space. The implementation of the Parallel Substitution Algorithm enables one to develop more compact (according to the number of states and the number of transition rules or substitutions)...
Fine-grained parallel models of spatial dynamics are analyzed from the point of view of the relationship between their continuous and discrete constituents. The models are ranged from the absolutely continuous partial differential equations to the absolutely discrete cellular automata. In the interval between them, there are cellular neural networks, cellular...
In this paper, the functions, raising the level of communication operations and mapping operations of the solution space of applied tasks on the multicomputer memory in the MPI-programs, are offered.
The Graph Automaton intended for modeling parallel fine-grained transformations of graph structures is presented. It works in mode of simultaneous application of a set of substitution commands to a graph image. Substitution commands are presented in graph notation, too. The example of algorithm implementation on the Graph Automaton is given.
A new multilayer cellular pipelined algorithm architecture for the complex scalar product computation is presented. The time complexity is evaluated. The initial data and results are quaterimaginary numbers. The design is performed in terms of a model of distributed computation – Parallel Substitution Algorithm.
The Cellular Automata models were proposed for simulation not so long ago, but recently they are in importance. Amongst 2D models, which have been recently studied, two basic ones have been distinguished. All the other known models are modifications of the basic ones. One of such modifications is proposed, and...
In this paper, by means of an abstract model of the SIMD type with vertical data processing (the STAR-machine), we present a simple associative parallel algorithm for implementing the criterion of Chin and Houck to verify minimal spanning trees in undirected graphs. This algorithm is given as the corresponding STAR...
The WinALT system for imitational simulation of fine-grain structures and algorithms is presented in the paper. Its architecture is substantiated; user's interface is described, possible applications are outlined. It is demonstrated that open architecture of the system allows to construct different versions of system for sequential and parallel computers and...
In this paper, we propose a strategy language for designing constraint solvers and schemes of solver collaborations. Solvers are seen as bricks that can be integrated when creating more complex solvers that can become themselves new bricks to compose new solvers. These bricks are glued together using operators of our...
Various algorithms for achieving different levels of local consistency (i.e., constraint propagation algorithms), even diverse ones for the same kind of local consistency, are present in the literature and built into existing systems. Due to their variety and diversity, a natural quest is to search for a common framework. In...
In this paper we present a new stochastic search algorithm which is designed to solve finite binary constraint satisfaction problems, where constraints of the “not equal” type predominate. The experiments show that, in comparison with the backtrack-based algorithms, the presented algorithm is superior when it is used to solve problems...
In the present paper, we examine some issues related to the development of Time-EX (an intelligent scheduling and project management system) as an application of the method of subdefinite models (SD-models). Extension of SD-models with dynamic elements is briefly discussed, along with their implementation via the tools for knowledge representation...
At the beginning of each school year, universities everywhere must undertake boring and time-consuming process of slotting students, teachers and lessons into available classrooms. It is a natural scheduling problem and schedulemakers are looking for simple flexible and effective automatic systems.
Scheduling problems are often NP-complete. There are many approaches...
Logic programming is a rule-based formalism: a program consists of a set of rules activated by an initial query. In contrast, imperative programming is explained by means of a procedure-based view: a program consists of a set of procedure declarations and an initial statement.
We clarify here to what procedure-based...
We describe the use of array expressions as constraints, which represents a consequent generalisation of the element constraint. Constraint propagation for array constraints is studied theoretically, and for a set of domain reduction rules the local consistency they enforce, arc-consistency, is proved. An efficient algorithm is described that encapsulates the...
The paper presents a model for building cooperative solvers for computational problems. We suggest an architecture of an environment which allows us to implement the model. It consists of a kernel, a library of methods, a scenario language and a universal internal representation. Methods have a special structure that provides...
One of the most advanced and practically significant approaches in constraint programming is the method of subdefinite models.
This method is the basis for a multilevel constraint programming tech- nology that has been developed to solve various problems in economics, engineering, calendar planning, etc.
A subdefinite model is a pair...
Algorithm is one of the most fundamental concepts in information technology. Its absolutely dominant position reminds that of programming in machine codes during the era of the first computers: it appeared to be the only conceivable method to communicate with a machine, but its fate disproved this axiom. The same...
A knowledge representation language with subdefinite data types and constraints is considered. An important feature of this language is the possibility of operating with objects that may have slots (attributes) with imprecisely defined (subdefinite) values. Another important feature of the language is that it allows one to bind any object...
A new specification language, simple to master, is suggested. In spite of simplicity, this language is expressive enough. A decision method for its quantifier-free formulas is given. A program verification method based on this language is illustrated by an example of a program of bubble sorting.
In the paper, we construct a formula that characterizes a timed event structure up to the timed must-preorder.
This paper presents a class of Stochastic Petri Nets with concurrent transition firings. It is assumed that transitions occur in steps and for every step each enabled transition decides probabilistically whether it wants to participate in the step or not. Among the transitions which want to participate in a step...
A lot of work has been dedicated to the analysis of sequential imperative programs. However, existing tools of analysis seem to lack for clarity and extensibility. That is to say, although some of them perform powerful context-sensitive dataflow analysis, their efforts are chiefly directed to the analysis of a particular...
In this paper, the model-checking algorithm from [22] is adapted to coloured Petri nets (CPN) [9, 10]. The state-based semantics of LTL for CPN is given and the correctness of the obtained approach is proven. It is also shown how to apply this model checking technique to interval-timed CPN.
The symbolic method for verifying definite iterations over hierarchical data structures is extended to allow tuples of data structures and exit from the iteration body under a condition. Transformations of these generalized iterations to the standard ones are proposed and justified. Useful properties of the transformations are given. A technique...
There are lots of different approaches developed for global static program error analysis. Most of them are concentrated on sequential programs. Analysis of parallel programs is considered complicated. The overview contains brief information on obsolete and modern approaches to global static error analysis of parallel programs.
R.N. Taylor has proposed Call...
A formal model of the state of a dynamic system with updateable locations as values is presented. A mechanism of dynamic function declaration resembling that of variable declaration in programming languages is suggested.With each of these functions a dynamic access function is associated. An access function can be used either...
Two-tier procedure of constructing compound model of computing structure with fine-grain parallelism are discussed in this paper. The description of tools of construction is presented. It was shown that the visual programming technology was utilized for their creation, and the care was taken to give to the user intuitively understandable...
In this paper, we continue the study of a parallel FSM equation. We establish that the solution set has a lattice structure and consider two restricted solutions to the equation, namely, a supremal and a livelock-free solution.
The algorithms for minimization of large-dimension functions with linear constraints with allowance for sparseness of the limitation matrices are considered. A~special case of the quadratic programming is emphasized. The algorithms have been implemented as a package of software programs to be used in the operational environments DOS, UNIX.
In this paper, by means of a model of associative parallel systems with the vertical processing (the STAR-machine), we propose a natural straight forward representation of the Edmonds–Karp version of performing the Ford shortest path algorithm. We present the associative parallel algorithm as the corresponding STAR procedure and prove its...
The methods and tools of model construction with fine-grain algorithms and structures are considered and demonstrated by typical examples. The usage of the system for models with complicated structure and large amount of data is presented.
The Object Visualization Engine library developed by the authors is described in the paper and its architecture is substantiated. This library provides an easy way for a user to implement the modules for custom visualization of cellular objects. These modules are called Object Visualization Drivers (OVD). The algorithm of the...
In this paper, the first-order Cellular Neural Networks (CNN) with homogeneous weight structure are investigated and an approach to learn them is suggested. It is shown that all CNN weight templates are classified according to properties of possible stable states. As the result, the proposed learning method is based on...
A parallel algorithm is presented for the input of data arrays (partly, of images) into processors of a distributed computer system (CS). The algorithm minimizes the input time by means of effective routing of array fragments in the CS interconnection network. The algorithm modeling shows that it is optimum for...
A new notion of a multi-branch narrowing that allows case analysis to be built in is introduced. A narrowing strategy that preserves formula satisfiability is suggested. A formalism called formula rewriting systems specifying the strategy is defined. The termination of formula rewriting systems is considered.
A pair consisting of a place and a token in a coloured Petri net is considered as an elementary resource for this net, and a resource is a multiset of elementary resources. Two resources are bisimilar, if replacement of one by another in any marking doesn't change the net behaviour...
Based on notions of computability for operators and real-valued functionals, a background for formalisation of complex systems is introduced. We propose a recursion scheme which is a suitable tool for formalisation of complex systems, such as hybrid systems. In this framework the trajectories of continuous parts of hybrid systems can...
The symbolic method for verifying definite iterations over hierarchical data structures is extended to allow a restricted change of the structures by the iteration body and exit from the iteration body under a condition. A transformation of definite iterations which use exit from the iteration bodies to the standard definite...
The paper discusses some issues related to model checking utility and reliability: (1) utility of model checking and games for solving puzzles, and (2) importance of games and puzzles for validation of model checkers.
We consider the process algebra BPA* proposed by Bergstra, Bethke, and Ponse, since it nicely defines a class of infinite processes. Investigation of representation of event structures for this class of processes is presented in this article. We extend the algebra BPA* by a parallel composition and modify its sequential...
Dataflow networks are a well-known mathematical tool extensively used for representing, analyzing and modeling concurrent computing systems and their software. Formal dataflow models reported in the literature may be divided in two groups – static and dynamic. Static models admit at most one token on an arc. This assumption severely...
An important problem of the representation of a big dynamic system as a number of interrelating typed Gurevich Machines (Abstract State Machines or just ASMs in the sequel) and the subsequent combination of the specifications of individual ASMs into the specification of the whole system is investigated in the paper...
We describe a notion of formula rewriting systems (FRSs) and investigate a relation between FRSs and techniques of term rewriting systems (TRSs) and narrowing. We demonstrate the use of FRSs for finding errors in array and file operations.
The work is devoted to a tool for simulation of executional specifications of distributed systems, simulation and testing of the behaviour of these systems. The systems are described in terms of the REAL language developed in A.P. Ershov Institute of Informatics Systems, SD RAS .
Pattern matching is a component of many information retrieval problems. We deal with searching for a set of patterns. The following generalizations of the problem are considered on the same basis: 1) searching for the set of patterns by a partially-specified query of large cardinality; 2) revealing the coincidences...
The paper considers the problem of supercomputing support and Internet technologies. The PROGRESS project being developed at the A.P. Ershov Institute of Informatics Systems is discussed. The system is intended to support rapid prototyping of compilers for high-level languages (e.g., Fortran-77, Modula-2, Sisal-90) and for a family of architectures exploiting fine-grained...
The HIGRES system is considered as a support tool for visual processing of hierarchical graph models. HIGRES is implemented in C++, works under MS Windows 95/NT and is available on WWW at http://pco.iis.nsk.su/higres.
This paper presents a brief description of an expert system LMESOP, a tool for investigation of already known systems of optimizing transformations and for development of the new ones.
A technology for solving problems with large data sets in an object-oriented constraint programming environment NeMo+ is presented. We describe facilities for database access and interaction of data with NeMo+ objects.
Formal models of parallel computations are widely used in the design of parallel and distributed software (PDS) for multiprocessor computer systems (MCS). The choice of a model is decisive for efficiency of the solution of design problems. The necessity of such a choice is due to a splash of interest...
A hypertext system here presented supports some features essential for software and documents development environment; in particular, versioning (both logical and chronological), macro facilities, authoring facilities and interface with text representation systems HTML and TEX.
Hypertext is a natural environment for software project development. The hypertext of a...
In the paper we present a technology for development of dynamic multi-agent systems which is based on a combination of the object-oriented approach with constraint programming. We introduce the notion of an active object as a way of describing and implementing the intellectual, reactive and communicative properties of agents. We...
The paper is devoted to the investigation of behavioural equivalences for Petri nets with silent transitions (τ-equivalences). Basic τ-equivalences and back-forth τ-bisimulation equivalences are supplemented by new ones, giving rise to the complete set of equivalence notions in interleaving / true concurrency and linear / branching time semantics. Their interrelations...
In this paper we focus on new facilities of a logic programming system ECLiPSe and propose a way of using these facilities for implementation of a constraint programming method called Subdefinite Computations. We briefly describe the Interval Domain library which employs the proposed implementaion technique for solving...
An approach to integration of methods of constraint programming with various knowledge representation means, such as frames, semantic networks, and production rules, is considered. A knowledge representation language developed on the basis of this approach is presented. In contrast to other languages that also use the constraint programming technique, this...
This report presents an informal description of the GSTC language and some methods of recursive parallel programming language which enable us to organize parallelizing with the help of a set of basic structures (stencils). This makes it possible to design effective recursive parallel programs and to create, on their basis...
In this article, we discuss the analysis of equality relationships for program terms. We extend a description of the analysis presented in last articles of the author and give attention to some new aspects which are not widely considered yet. In particular, among other illustrating examples, a program is given...
The history of informatics in the leading countries as well as our twelve-year experience shows that the initial stage of the computerization era is practically connected with the level of the computer competence. Educational informatics provides elementary computer knowledge. This course should be based on a special concept (model) of...
In this paper we propose a novel associative parallel algorithm for selecting a directed cycle of the maximal weight on an abstract model of the SIMD type with vertical data processing (the STAE-machine). This algorithm is represented as the corresponding STAR procedure whose correctness is verified and time complexity is...
We introduce a new notion of parametric time Petri nets, an extension of time Petri nets whose transitions are labelled with parametric time restrictions. Further, a time behaviour analysis algorithm for the real time branching time temporal logic TCTL and a one-safe parametric time Petri net is proposed. The result...
We present an extension of the class of cause-effect structures by coloured tokens. As an example of coloured c-e structure we use the well-known problem of dining philosophers. Relationships between the classes of coloured c-e structures and coloured Petri Nets introduced by K. Jensen are investigated.
The notion of bisimulation equivalence has been introduced by D.M.R.Park. Informally, two processes are bisimilar if their possible behaviors have the same branching structure, i.e. any behavior of one system can be reproduced by the other system. In this paper, in order to get equivalence notions nicely adapted to peculiarities...
Parallel Substitution Algorithm (PSA) is a formal model of fine-grained parallel computation. It has been developed and used for design and investigation of highly parallel algorithms and digital systems architecture. Here it is shown, that its expressive capabilities allow also to use PSA formalisms for representing a wide range of...
The inverse problem of determination of coefficients of multidimensional heat equation is considered. The method of statistical modeling of trajectories of corresponding systems of stochastic differential equations is applied to the solution of the direct problem and sensitivity analysis. The application of parallel computers allows a significant increase of the...
In the present paper, one of the methods of parallel solution to the multidimensional parabolic equations on the multiprocessor computing systems of the MIMD type is proposed. Much attention is given to the domain decomposition method and to distribution of subdomains among computers. As a computing system, on which the...
The well-known “ob-shop” problem in the wider formulation (many machines of the same sort and many workers per one operation) is discussed in the paper. The graphic approach to the problem with two jobs and variable processing times of operations is proposed. It is shown that the more general problem...
The optimal circulant graphs have minimum diameter for the given order N and degree ν and, respectively, optimal features with respect to communication delays, reliability and connectivity under implementation as interconnection networks in multimodule supercomputer systems. The questions of existence of optimal (nearly optimal) circulants with the degree ν =...
A model of parallel program called program skeleton and a program system for manipulating and translating the program skeletons into parallel programs on various high-performance computing systems are considered. The main goal of this system is to make it easier to create and execute parallel programs on various parallel computing...
In this paper, we employ Dijkstra's algorithm for finding single-source shortest paths in directed graphs. We propose an efficient implementation of this algorithm on a model of associative parallel processors of the SIMD type with bit-serial (or vertical) processing (the STAR-machine). Moreover, we show how to extend this implementation for...
We intend to draw a comparison between the different most known data indexing structures so as to outline the bottlenecks and faults from the point of view of their utilization in the fine grained algorithms simulating system WinALT. Then we would like to propose some ways to eliminate these drawbacks...
In this work, a formal background for the choice of parameters of Cellular Neural Network generating basic types of autowaves, namely, a round traveling front, a round traveling pulse and a spiral wave, is presented. This background is based on investigation of phase plane properties of a CNN cell. The...
In this paper, a branch and bound algorithm with branching in depth for problems of the integer linear programming (ILP) is considered. The results of solution to large problems of integer and mixed-integer linear programming are presented. A brief information is given on the software for solution to large ILP...
Using the Parallel Substitution Algorithm, as a formal model of parallel computations, a distributed architecture is designed for implementation of the following two fast parallel algorithms: one for the maximal independent set problem and the other for the minimum weighted vertex cover problem. The former is a randomizing algorithm based...
A discrete time version of Cellular–Neural Network (DCNN) is a paradigm of neural networks that has the realistic perspective to be implemented in VLSI. An investigation of DCNN capabilities for image processing is attempted. It is done through detailed study of two typical concrete problems: 1) associative storing, retrieving and...
Several classes of objects for the object-oriented approach in programming the approximation stage of solving the boundary value problems are proposed. They are the classes for a computational cell, for boundary conditions and coefficients of the linear system of equations.
Technological aspects of the numerical solution to multi-dimensional boundary value problems (BVP) for partial differential equations (PDEs) using the finite difference, the finite element or the finite volume methods are described. Among them, the mathematical formulation of the problem, definitions of objects under consideration, algorithms of approximation with different accuracy...
A new cellular algorithm architecture for multiplication of two long binary integers in arrays of restricted size is presented. The new algorithm is based on “divide and conquer” technique and performed in terms of a model of fine-grained parallelism – Parallel Substitution Algorithm. Time complexity of the new algorithm for...
TOPAS (Test and Optimization of Parallel Algorithms and Structures), a programming tool for visualization, animation and investigation of sequential and parallel algorithms for mapping of parallel program graphs into graph structure of parallel computer systems is presented. The tool is implemented in Java and is accessed on http://rav.sscc.ru/~monakhov/topas.html.
A solution to combinatorial optimization problem of constructing optimal circulant networks with the minimum diameter under given degree and number of graph nodes is considered. The circulant networks and their different applications are the object of intense investigations. Under degree of a graph δ > 4 and large number of nodes...
In this paper we propose a representation of Edmonds' algorithm for finding optimum branchings on an abstract model of the SIMD type with vertical data processing (the STAR-machine). To this end for a directed graph given as a list of triples (edge vertices and the weight) we construct associative algorithms...
The necessity of the open architecture for fine-grained parallel model simulating system (WinALT) is discussed. The description of WinALT open architecture and external module interfaces is given. WinALT consists of the language and graphical user's interface subsystems and the kernel. The extensibility of WinALT is implemented in the kernel by...
The problem of achieving Cellular-Neural Associative Memory (CNAM) limiting capability is considered. At first a CNAM learning method based on the idea of Perceptron Learning Rule which provides maximal ability to restore distorted patterns is suggested. Next, expressions for determining self-connection weight values which increase attractivity and decrease the number...
Two-layer cellular network as a simulating model of wave processes is considered. The wave speed dependence from an intralayer connection weight is presented.
We generalize the notion of formula rewriting systems proposed in the prelim¬inary work, extend the class of such systems and expand our previous results for the new class. We demonstrate that the well-known techniques of formula simpli¬fication can be represented in terms of this formalism and investigate termination problem for...
Our aim is to validate distributed systems which are described by means of Estelle. This paper describes a procedure of translating the Estelle specifications into colored Petri nets extended by the priorities and Merlin’s time concepts. The considered specifications are based on standard Estelle which developed by ISO. The hierarchy...
The XDS-COM toolkit provides a language binding of the Microsoft COM to Oberon-2/Modula-2. It can be used to develop both COM clients and servers. Mul¬tiple interfaces of a single object are created in a natural way. The XDS-COM does not introduce any language extensions but extensively uses the rich run-time...
The paper is contributed to develop a family of equivalence notions for real¬time systems represented by labelled Merlin’s time Petri nets with zero length time intervals (i.e., with fixed time delays). We call them “timed Petri nets”. In particular, we introduce timed (time-sensitive), untimed (time-abstracting) and region (based on the...
A knowledge representation language based on integration of such means as frames, semantic networks, production rules, subdefinite computational models, and methods of constraint programming are considered. An important feature of this language is the possibility of operating with objects which can have slots with imprecisely defined (subdefinite) values. Another important...
An approach to the object-oriented specification by typed Gurevich machines is proposed in the paper. The approach is based on considering an object update as a transition from one algebra of a given signature to another of the same signature. Each object possesses a state and a unique identifier; the...
This paper describes a new group-oriented distributed shared memory (GDSM) computation model and its hardware support for improving performance in large-scale shared memory multiprocessors. The GDSM model is based on a concept of groups as basic computational units representing sets of parallel threads that cooperate and communicate by sharing an...
In this paper by means of an abstract model (the STAR-machine) we study a group of associative algorithms for unweighted graphs given as an adjacency matrix. These algorithms are written as the corresponding STAR procedures whose correctness is proved and time complexity is evaluated.
The specification language Basic-REAL consists of executional and logical specification sublanguages. The first one is based on SDL and differs from it by multiple clock concept, time intervals associated with actions, non-determinism, and rich collection of channel structures. The second one is based on temporal and dynamic logics extended by...
The paper is devoted to the investigation of behavioural equivalences of concurrent systems modelled by Petri nets. Back-forth and place bisimulation equivalences known from the literature are supplemented with new ones, and their relationships with basic behavioural equivalence relations are examined for the whole class of Petri nets as well...
The intention of the paper is to develop a model checking algorithm for real time systems represented by time Petri nets and a real time extension of the branching time temporal logic CTL, called TCTL. Since time Petri nets model real time systems over dense time domain, the number of...
An approach to combining type-structured algebraic specifications with Gurevich Machines (evolving algebras) is proposed. A type-structured algebraic specification, in its simplest form, consists of data type specifications and independent function (detached operation) specifications. Concrete and generic specification components (data types and functions) are distinguished in a more developed case. A...
Problems of modeling and calculations of dynamics of the price of options by Monte Carlo method on parallel processors are considered. Technique of calculation of some factors, enabling to investigate change of the price of options and to evaluate possible consequences of the made bargains is described. Numerical calculations show...
The basic principles and tools of the technology, intended for the development of the computerized training environments, in particular for computerization of university courses are presented. The proposed technology is based on the use of the processor Word for Windows and other environments, such as Turbo Pascal, Delphi, etc.
In the paper the construction of the so called iterative networks is studied. This class contains rearrangeable N-inputs M-outputs networks carrying m connections with roughly 2(N+M) log (NM/(N+M)) contacts, if m = min(N,M) and with roughly 2(N+M) log m contacts, if m < min(N,M); these results are the best obtainable by the methods used.
A class of two-dimensional regular graphs called circulants and its special case of the double-loop networks are considered. Such graphs provide a practical interest as reliable interconnection networks for the multimodule supercomputer systems. A solution to the problem of determining the best double-loop networks with the minimum of a diameter...
In this paper we consider the routing, broadcast and gossiping problems in circulant networks. The circulant graphs are studied extensively as reliable interconnection networks for the multiprocessor systems. The optimal circulants have the minimum diameter and the minimum average distance and, respectively, maximum of the reliability and connectivity. Review of...
For fine-grained associative parallel systems of the SIMD type with vertical data processing we analyze two models of associative processing: the STAR-machine and the orthogonal machine. We have obtained that the STAR-machine simulates the orthogonal machine run in constant time while the orthogonal machine simulates the STAR-machine run in time...
A description of user interface and language of a simulation system (WinALT) is given in the article. This system is based upon formal model called Parallel Substitution Algorithm (PSA). The system combines the best features of its ancestors. It has extensible functionality and is open for user modifications and extensions...
A cellular algorithm for extraction of isolines from 2D image of 3D surface is presented. The algorithm is divided into two stages: secondary quantization and extraction of isolines. Realization of each stage as one-time iteration on the base of the Parallel Substitution Algorithm is obtained. Results of the algorithm simulation...
A verification method is proposed for definite iteration over different data structures. The method is based on a replacement operation, which expresses the definite iteration effect in a symbolic form and belongs to a specification language. The method includes a proof rule for the iteration without invariants and inductive proof...
This paper discusses a subclass of Merlin’s time Petri nets called here time Petri nets without overlappings of firing intervals. In addition to the existing enumerative procedure for time nets, a new technique of reachability analysis for nets in the subclass is presented. Correctness of the presented method is proved...
In the paper two problems of semantic property analysis of recursion schemes are stated and a marking technique for solving these problems is described.
This paper describes a system of transformations that preserves the semantics of logic programs with respect to a fixed goal. We formalise some standard transformations and introduce two new transformation rules: Copying/Merge of Copies and Contextual Replacement by Equal Term. Correctness of all schemes of the transformation rules is...
In the paper a multi-agent technology based on integration of the object- oriented approach and constraint programming is proposed. The key notion of this technology is an ’’active object” that has three specific features. First, an active object has the ability to change its state based on the analysis of...
A new calculus of labelled nondeterministic processes AFLP2 is proposed which is an extension of the known calculus AFP2 by labelling function. The denotational and operational semantics and complete axiomatization of the semantic equivalence are presented. The interrelation of net equivalences from with equivalences of the algebra (semantic...
We consider different equivalence notions for prime event structures, which explicitly reflect causality, concurrency and conflict relations between occurrences of events in the structures. The intention of the paper is to establish whether or not these equivalences are preserved under refinement of actions. An operator of refinement replaces actions on...
Associative neural memory of the Hopfield type, where each element (neuron) has a restricted amount of connections is considered as a cellular-automaton-like network. The goal of the investigation is to determine the degradation of memory capacity and efficiency of pattern retrieval caused by the decrease of connection number. As a...
Solving of large-scale systems of linear algebraic equations, ill-conditioned and non-square systems requires special algorithms which should be suitable for effective implementation in modern multi-processor systems. One of such methods was proposed by A.A. Abramov. This approach is based on consequential projecting of solution to a system of ortogonal vectors...
Two new cellular pipelined algorithms (2D and 3D) for computing a sum of products with a very short multiplication time (six and three steps, respectively) are proposed. The initial data and results are binary signed-digit integers. The design and investigation tool is an experemental computer simulating system (Animating Language Tools)...
The history of the Siberian researches in parallel processing is surveyed and present project of the Siberian Network Supercomputing Center (SNSC) is considered.
In this paper by means of an abstract model (the STAR-machine) we describe an associative version of the Gabow algorithm for the degree-restricted problem. We have obtained that on an associative parallel processor this algorithm takes the same time as a minimal spanning tree algorithm. In Appendix the associative algorithm...
Finite element non-stationary electromagnetic fields modeling technique is proposed. It permits to decrease computing expenses of three-dimensional problem solving. This technique is implemented in program complex TELMA, its efficiency is confirmed by solving significant number of both modeling tasks, and complicated practical problems.
A formal model for the fine-grained parallel computations is presented, which combines the connectionist approach of Artificial Neuron Networks with the cellular -like communication structure. The model is based on the concepts and formalities of Parallel Substitution Algorithm, which is considered the most theoretically advanced generalization of Cellular Automaton. Principles...
This paper includes several results concerning with compositional model checking (CMC) for finite-state systems with multiple clocks. We describe a model of time [6], and a method of reducing a timed (infinite) model to a finite untimed model. We also present a new Finite Process Algebra (FPA) and its...
In this paper the possibilities of organizing heterogeneous computing in so-called Combined Architecture systems consisting of a basic host subsystem (a massively parallel computer), and a set of high-performance specialized parallel coprocessors (hardware modules) executing the main workload are discussed. To optimize the choice of hardware modules, a classification of...
An annotated program is a program written down in a programming language extended by the annotations which are formalized comments in the basic programs and relevant for the semantics of the program can be described. The paper focuses on the completeness property of the directive mechanism for different kinds of...
A problem of mapping of an information graph of a complex algorithm into the pyramidal interprocessor network of a parallel computer system is considered. The parallel recursive algorithm for optimal or suboptimal solution of the mapping problem, the objective functions for mapping and experimental results for the pyramidal multiprocessor system...
In this paper we analyze two procedures for finding a minimal spanning tree of a graph for an abstract associative STAR-machine with bit-serial processing. These procedures are based on the Prim-Dijkstra algorithm and use different graph representations. We prove their correctness, evaluate their complexity and compare them. In addition, we...
In this paper a variety of Petri net equivalences is examined. A correlation of all the considered equivalences is established, and a lattice of implications is obtained. In addition, the equivalences are treated for some subclasses of Petri nets: sequential nets, T-nets and nets with strict labelling.
Dataflow networks are a well-known mathematical tool extensively used for modelling and analyzing concurrent computing systems and their software. A few formal dataflow models reported in the literature may be amalgamated in two groups-static and dynamic. Static models allow at most one token on an arc. This assumption severely limits...
Operation of parallel substitutions over cellular arrays in mixed (synchronous-asynchronous) mode is studied. Correctness conditions for parallel substitution systems in this mode of execution are stated.
The aim of this paper is to introduce the new kind of decomposition for computer colour images based on the three-factors analysis of the palette and to demonstrate the improvement of the compression coefficients in the comparison with the well-known PAL television oriented decomposition standard.
Asynchronous versus synchronous cellular computations are investigated in terms of Parallel Substitution Algorithm (a formal model of fine-grained parallel data processing). A general method for constructing asynchronous cellular computation equivalent to a given cellular algorithm execution is presented. It is shown that more than a twofold increase in cell-complexity should...
This paper is devoted to the application of specialized processors for speeding-up the realization of relational algebra operations on fine-grain SIMD computers. A short description of two processors is presented. By means of a special high level language STAR, the algorithms of implementation of relational algebra operations in a STARAN-like...
Peculiarity of the most direct algorithms for solving system of linear equations is the use of divisions for the elimination of unknowns. Divisions require a great time for its execution, when the multiprecision arithmetic is used because in this case they are realized by special programs. The paper describes the...
Event structures have widely been proposed as a basis for constructing models of nondeterministic processes. However, not all event structures are turned out to be suitable for this purpose. One way to get around this problem is to adapt Petri's concurrency axioms (including K-density and related properties) to event structures...
Special colour roundoff problem arises in the visualization of the colour images in the •computer screen under restricted palette after real valued treatment of the initial image, connected for example with the compression of colour components, and also in the scanning of colour images, palette exchanges and so on. An...
Some results of investigation into the spectral properties of k-valued (k ≥ 2) logical functions are presented. The main goal of the investigation is to show the power of spectral methods in implicant extraction and recognition of some useful logical function properties. The relation between the sum-of-products form...
This paper describes implementation algorithms of relational algebra operations in associative parallel processors like Staran using the language STAR. For these operations we construct procedures which form a hierarchy.
This paper presents the S4CAD software tool which allows to synthesize and analyse a set of admissible systolic arrays for the given matrix algorithm. A systematic approach to the design is presented as a theoretical background of the S4CAD. The tool runs under graphical operating environment Microsoft Windows 3 placing...
An efficient way to achieve the high accuracy of the results of computations is to increase the operands capacity. The best results in terms of the problem solution rate and effectiveness of memory using can be reached in the case when a computer system provides the possibility of dynamic capacity...
The intention of the paper is to characterize and examine density and crossing properties of prime event structures. We show the coincidence of L-density and L-ciossing for this class of event structures. It has turned out that any configuration in an M-dense prime event structure is full (i.e., at least...
Mu-calculus is a polymodal logic with fixed points. A Decision Procedure (DP) checks the validity of a formula. A Model-Checking Procedure (MCP) constructs the validity set of a formula in a model. Since Mu-calculus is finitely approximatizible and it is applicable for verification of Finite-State Machines an effective MCPs are...