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…
distributed systems verification, distributed systems analysis, translation, SDL, SPIN, Dynamic-REAL, GolangThe paper presents the history of START, an ad-hoc team created in 1985 to develop fifth-generation computers in response to the "Japanese challenge". As a new form of the organization and implementation of scientific and technical projects during the perestroika, START contributed to the…
perestroika, history of informatics, START, fifth generation computers, Japanese challenge, post-industrial societyNowadays, 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…
IoT, Electronics, Microcontrollers, Development platform, Web, Arduino, ESPThis 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…
neural network architectures, distributional semantic models, ELMO, SRU, GRU, named entity recognition taskThis 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…
natural language processing, information extraction, terminology extraction, definition extraction, entity recognitionThe 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…
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…
cellular automata, pattern formation, domino patternThe 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…
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…
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é…
elastostatics Lamé equation, matrix iterations, linear algebraic system, Monte Carlo method, red-black orderingThis 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 relations. The…
natural language processing, information extraction, language models, SpERT model, entity recognition, relation classification, machine learningThe 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…
transportation problem, modeling, research automation systemThe 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…
functional programming, parallel computing, programming languages, programming system, programming paradigm, multi-paradigmEntity 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…
entity alignment, knowledge graphs, vector representation, matrix ordering, language models, multilingual knowledge basesOne 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…
PCISPH, SPH, parallel computingWhen 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…
cassette, factographic systems, distributed systems, non-specific ontologyAt INP SB RAS, various mechanisms for the erosion of tungsten samples
during the pulsed heating were studied. Data were obtained that made it
possible to analyze the experimental results of the surface temperature dynamics
taking into account the cooling due to the vaporation in vacuum. A numerical…
A two-dimensional case of the process of laminar flow passing through
a pipe constriction is investigated. The two-dimensional statement corresponds
to the case with a three-dimensional flow between two parallel planes. A cellular
automaton model of a flow is used, which has an integer alphabet of…
The problem of the network reliability calculation is studied. As the
network reliability we mean the classical reliability measure, i.e. the network probabilistic connectivity. It is assumed that the network has unreliable communication
links and perfectly reliable nodes. The problem of computing…
Computational plasma physics problems are a wide field with its own
hardware, software and scheduling strategies. There is a set of physical phenonena,
mathematical equations, numerical approaches, programming strategies and architecture concepts directly followed by each other. This means that an…
The influence of the weight quantization levels number on a capsule
neural network functioning quality is studied. The network is tested on the MNIST
dataset recognition. It is shown that to achieve the performance of the network
with continuous weights it is enough to have 16 levels of uniform…
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…
multilingual knowledge bases, integration, cross-lingual entity resolution, clustering, interactive visualization, matrix orderingIn 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…
ksmt-solver, non-linear constraint, CDCL-style reasoning, bound propagation, conflict resolution, implementationIn 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…
Flow event structures, interleaving and step semantics, behaviour, transition systemsWe 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…
State space reduction, weak time Petri net, intermediate memory policy, atomic memory policyThe 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…
RC4 encryption algorithm, cryptograph, privacy, security, information security, encryption algorithmWhen 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…
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…
ontology, user interface, software portabilityThis 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…
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…
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…
directed weighted graph, adjacency matrix, decremental algorithm, associative parallel processor, access data by contents, the time complexityPresented 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…
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…
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…
multilayer network, utility network, deployment area, track, graph, hypergraph, hypernet, connectivity, network reliabilityThe 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.
Relational structure, N-density, K-density, concurrencyThe 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…
text processing, part-of-speech homonymy, combined approach, machine learning, homonymy resolutionWe 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…
research automation system, what-if, statistical analysis, development of the transport systemIn 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…
signal processing, orthogonal transformation, strip-method, Hadamard matrix, impulse hindrance, error estimationThis paper develops general concepts useful for extracting knowledge embedded in large graphs or datasets that have pair-wise relationships, such as relations of cause-effect type. Almost no underlying assumptions are made, other than that the data can be presented in terms of pair-wise…
knowledge extraction, graph structure, type theory, natural language processing, link grammar, sheaf theoryThe 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…
image processing, textural features, orthogonal transformations, analysis of micro-photos, electronic microscopy, plant raw materialsThe 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…
operational semantics, ontological operational semantics, information transition system, conceptual transition system, abstract state machinesThe 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…
link grammar, agglutinative language, semantic analyzer, rhetorical structure theory, discourse markers, rhetorical relationsWe 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…
ambiguity resolution, lexical ambiguity, syntactic ambiguity, ontology population, information retrieval, Scott information systems, formal concept analysis, multiagent systemsThe 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…
directed weighted graph, incremental algorithm, associative parallel processor, access data by contents, the time complexityDue 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 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…
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…
Impact structures catalog, morphostructural elements, geophysical anomalies, impact-magnetic genesisThis 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…
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…
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…
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…
operational semantics, conceptual transition systems, procedural programming languages, operational ontological approach, conceptuals, CTSL, MPLBodin 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…
SPIN, model checking, Promela editor, dsl, XtextThe 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…
natural language processing, syntactic analysis, Link Grammar Parser, summarization, relevanceThe 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…
scientific research automation, situation room, development of the transport system, macroeconomic modeling, what-if simulationThe 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…
programming languages, programming paradigms, programmers’ training, educational programming languages, language concepts, implementation structures, parallel programming, very high-level languagesCausal 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…
timed causal trees, category theory, syntax and semanticsThe 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…
mathematical functions, standard libraries, formal specification, formal program verificationWe 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…
labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid model, fluid density and distribution, performance analysis, Markovian bisimulation, fluid bisimulationThe 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…
science in Siberia, Novosibirsk programming school, software development, Alpha-compiler, Institute of Informatics Systems, A.P. ErshovThe 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.
state transition systems, domain-specific transition systems, operational semanticsThis 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…
Linked Open Data, SPARQL, ontology alignment, cross-language identity resolution, self-citation network, tf-idf, LDAThe 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…
natural language processing, syntactic analysis, Link Grammar Parser, relevance, Turkic languagesThe 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…
abstract register machines, random-access machines, search programs, formal specification, interactive theorem proving, verification system PVSSuccessful 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…
verification, specification, C-light, ACSL, MetaVCGThe 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 linguistics, text classi cation and categorization, text annota- tion, morphological tagging, social network data analysisThe 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…
ontology, Wiki, semantic technology, information system construction, data and knowledge extractionAlias 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…
aliasing problem, alias calculus, logic of partial correctnessRecognition 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…
GPU computing, parallel genetic algorithm, protein-RNA interaction, RNA motif recognitionThe 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.
attributed hierarchical graphs, graph visualization, graph navigation, search algorithm of maximum common subgraph of two graphsTwo 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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
social network analysis, data mining, Latané’s social impact theory, psychological operationsThe 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…
scientific research automation, situation room, development of the transport systemAbstract 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…
abstract register machines, random-access machines, formal specification, automated verification, interactive theorem proving, verification system PVSIn 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…
description logic, lattice-valued modal logics, modal logic, distributive lattice, concept latticeThe 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…
undirected graph, spanning tree, chord, minimum spanning tree, connected component, fundamental set of circuits, vertical processing systemDevelopment 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…
C-light, ACSL, Simplify, standard library, axiomatic theory, specification, verificationSisal 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…
functional programming, compilers, program optimizationA 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…
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…
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…
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…
social network analysis, network model, graph of a network, data mining, centralityThe 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…
scientific information resources, knowledge portal, ontology, content-based access, knowledge-driven navigation, semantic searchThis 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…
graph, hierarchical graphs, algorithm, visualization, visual effectIn 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…
decomposition, inseparability, forgetting, progression, basic action theory, situation calculus, reasoning about actionsDesign 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…
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…
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…
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)…
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…
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…
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…
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…
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…
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…
program analysis, program verification, program model, domain specific language, verification system, C-light, C-kernelWe 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…
hierarchical edge bundles, science portal, content, information visualization, layered drawing, ontology, citation networks, Open Linked DataWe 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…
computer networks, communication protocols, Sliding Window Protocol, formal specification, automated verification, interactive theorem proving, verification system PVSThe 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…
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…
Memory organization, parallel access to information, image processing, objects trackingThe 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…
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…
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…
stochastic process algebra, Petri box calculus, discrete time, iteration, stationary behaviour, performance evaluation, shared memory system, variable probabilityThe 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…
program specification, program verification, domain specific language, pattern matching, program model, information systemThe 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…
hierarchical edge bundles, knowledge portal, modularity, ontologyIn 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”…
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…
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…
Information Retrieval System, Link Grammar Parser, information search, semantic tree, relevanceIn 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…
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…
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…
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…
stochastic process algebra, Petri box calculus, iteration, discrete time, stochastic equivalence, stationary behaviour, performance evaluationTime 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…
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…
decision support system, task ontology, subject domain ontology, solver, decision support module, monitoring, analysis, optimizationThis 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…
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…
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…
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…
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…
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…
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…
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…
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…
knowledge portal, ontology, content, information visualization, force-directed methods, tree drawing algorithmsThe 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…
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…
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…
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…
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…
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…
functional language, Hoare's triple, operational semantics, logical semantics, total correctness of a programThe 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…
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…
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…
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…
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…
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…
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…
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)…
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…
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…
stochastic process algebras, Petri box calculus, discrete time, operational semantics, denotational semantics, empty loops, stochastic equivalences, congruenceA 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…
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…
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…
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…
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 allowing…
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…
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…
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…
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 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…
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:
- industrial programming is very often unstructural (e.g., extensive use of “go to” in C-programs);
- program analysis…
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…
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…
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…
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.
decomposable theories, modular terminological systemsThe 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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
stochastic Petri nets, stochastic process algebras, Petri box calculus, iteration, discrete time, transition systems, operational semantics, dts-boxes, denotational semanticsThe 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…
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…
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…
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…
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…
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…
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…
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…
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 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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
model checking, μ-Calculus, intuitionistic modal logicA 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…
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…
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…
stochastic Petri nets, invisible transitions, interleaving and step semantics, equivalences, bisimulation, modal logicsIt 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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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)…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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.
…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…
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…
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…
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…
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…
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…
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…
stochastic Petri nets, Step Semantics, Equivalence Relations, bisimulation, Stationary Behavior, stochastic process algebraA 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…
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…
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…
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…
dynamic systems, formal methods, implicit state, updateable locationsTwo-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…
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.
finite state machine, composition, equation solvingThe 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 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…
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…
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…
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…
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…
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. Due to this fact…
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…
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…
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…
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…
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…
abstract state machines, specification-in-the-large, modular design, dynamic systemWe 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 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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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)…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
timed and untimed Petri nets, timed, untimed and region equivalences, trace and bisimulation semanticsA 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…
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…
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…
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…
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…
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 states of any…
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…
evolving algebras, Gurevich Machines, abstract state machines, algebraic specifications, implicit stateProblems 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…
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…
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…
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…
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…
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…
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…
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…
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…
123
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…
In the paper two problems of semantic property analysis of recursion schemes are stated and a marking technique for solving these problems is described.
program flow analysis, abstract interpretation, approximation, recursion scheme, strictness analysis, parameter dependenceThis 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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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)…
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…
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…
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…
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…
associative parallel processor, bit-serial processing, parallel algorithm, complexity of algorithms, undirected weighted graph, minimal spanning tree of a graphIn 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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…