Preprints of IIS SB RAS, 1999

Preprint 70
E. V. Okunishnikova
Presentation of the estelle time constructions using different models of timed petri nets

This work is devoted to modeling Estelle timers in terms of time mechanism presented by Jensen for coloured Petri nets. In the paper two methods are considered to represent Estelle transitions with delay-clauses. One of them uses the time inscriptions on the input arcs of the transitions, and the second does not. Moreover, the method of organization of the management phase is presented which allows us not to use the priorities when Estelle transitions with delay-clauses are modeled.

Preprint 69
V.L.Selivanov, A.G.Schukin
On hierarchies of regular star-free languages

Here we study hierarchies of regular star-free languages induced by hierarchies of sentences of appropriate signature on the number of quantifier alternations in the prenex normal form. It has been proved that all levels of these hierarchies do not have the reduction property, but the first two of them have the separability property. We have found inclusions between the levels of these hierarchies, as well as between some of their refinements. Key words: regular star-free languages, hierarchy, reduction, separability, refinement.

Preprint 68
V. L. Selivanov
A logical approach to decidability of hierarchies of regular star-free languages

We propose a new, logical, approach to the decidability problem for the Straubing and Brzozowski hierarchies based on the preservation theorems from model theory, on a theorem of Higman, and on the Rabin tree theorem. In this way, we get purely logical, short proofs for some known facts on decidability, which may be of methodological interest. Our approach is also applicable to some other similar situations, say to "words" over dense orderings which is relevant to the continuous time and hybrid systems. Keywords: star-free regular languages, hierarchies, definability, decidability.

Preprint 67
Natalia V. Sosedkina
Elements of informatics: on some problems of informatics (not for little ones and not for grown-ups)

This article is addressed to the first and the second form pupils. Two chapters of informatics ("Internal structure of computer" and "Computer and health") are represented using microdiscoveries approach.

Preprint 65
V. A. Nepomniaschy, N. V. Shilov, E. V. Bodin
A new language basic-real for specification and verification of distributed system models

To design distributed systems the standard formal description techniques (FDT), such as Specification and Description Language (SDL), Extended State Transition Language (ESTELLE), Language of Temporal Ordering Specification (LOTOS) are used. The verification of FDT specifications (proving their safety, progress, and other properties) is still an open problem. The logical approach to the problem consists in the development of mathematical semantics for FDT, in a choice of a logical language for property presentation, and in the development of a corresponding proving methodology. Our approach to verification of SDL specifications uses two-level scheme which combines the translation of SDL to a model high-level language with a verification method for the models. We use especially designed Basic-REAL (bREAL) specification language. This language with rigorous mathematical semantics is a version of the specification language REAL based on SDL and CTL. The paper presents syntax and semantics of bREAL in both formal and informal levels. Some semantical properties of bREAL specifications (including invariance under stuttering and the interleaving property of concurrency) are proved. A specification and verification example ("Good Passenger and Slot-Machine") is also given.

Preprint 63
Denis Perchine
The review of some types of neural networks

Some major type of neural networks, learning and net creation algorithms are reviewed in the article.

Preprint 61
E. A. Pokozy
Toward verification of concurrent properties of time petri nets

The intention of the paper is to develop an algorithm for verification of quantitative concurrent properties of real-time systems. For this purpose we introduce a new real-time temporal logic TCCTL which is similar extension of TCTL as CCTL is an extension of CTL. The proposed logic allows to distinguish concurrency from non-determinism. On the other hand, it is able to express quantitative aspects of the system behaviour using explicit time restrictions as a subscripts in temporal operators. So, TCCTL is a natural formalism for specification of concurrent real-time systems. In this paper we use time Petri nets for modelling of real-time systems. Note, that concurrency can be expressed in this model in a natural way. The TCCTLbased verification algorithm for time Petri nets is proposed. The algorithm of checking if the given time Petri net satisfies to the given TCCTL-formula is linear in the size of the formula and exponential in the size of the time Petri net.

Preprint 60
A. V. Zamulin
Adding genericity to object-oriented asms

Facilities for the definition of generic object types, generic type categories, generic functions and generic procedures in an object-oriented ASM are described in the paper. These facilities permit one to specify algorithms over complex data structures abstracting both from the type of the structure components and the structure itself. The use of the facilities is demonstrated by the specifications of some important parts of Standard Template Library for C++.

Preprint 59
A. V. Monastyrnyi
Using spread spectrum signals with inverse spatial link for data transmition

The first part of the article briefly describes existing methods of spread spectrum signals usage in data transmission. The second part describes the new approach in spread spectrum signals usage for data transmission based on the inverse spatial link building in data transmission channel. The description of the method is presented and some numeric estimations are made.

Preprint 58
V. A. Evstigneev, I. L. Mirzuitova
Loop analysis: a selection of candidates for paralization

The problem of selection of loops for their parallization or vectorization by compilator is considered. At first some known vectorizing compilators and suitable tools are described. For each compilator and tools are pointed how analysis and selection of loops is happened.

Preprint 57
Natalia V. Sosedkina
Exercizes in informatics for primary school students

This work includes the exercises for children of 6-10 years old which can be used at the computing lessons on the topics `Information` and `Algorithm`.




You are reporting a typo in the following text:
Simply click the "Send typo report" button to complete the report. You can also include a comment.