Preprints of IIS SB RAS, 1999

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.

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.

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.

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.

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

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.

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++.

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.

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.