Preprints of IIS SB RAS, 2000

In this paper the unfolding technique is applied to coloured Petri nets (CPN) [8,9]. The technique is formally described, two algorithms and three finitization criteria are considered. It is also shown how to use the unfolding technique taking into consideration symmetry or equivalence specifications presented in [9]. We require CPN to be finite, n-safe and containing only finite sets of colours.

At present, there are effective algorithms for solving non-linear univariate equations, for example, the interval Newton method. These methods are either ineffective or unapplicable to systems of multi-variable equations. The paper presents the NC algorithm for improving an external estimation of the solution set to a constraint satisfaction problem. To solve multi-variable systems, it uses existing methods for solving univariate equations.

This work is concerned to research dealing with automated constructing net models of dynamic Estelle specifications. Coloured Petri nets introduced by Jensen are used as the net models. Describes a method of translating the dynamic construction of Estelle specification into the net models.

Different concurrent (interliving, step and partial order) semantics of may-testing equivalences in the setting of timed event structures are developed. As a main result a trace characterization and comparison of all the equivalences are provided. This work is supported in part by Russian Fund of Basic Research (Grant N 00-01-00898).

This review is devoted to description and comparison of currently available tools for visualization and construction of graph objects. The entire spectrum of system characteristics is considered, from graphic possibilities and quality of the user interface to additional means intended to perform and visualize graph algorithms. In conclusion, the state-of-the-art of software design related to graph visualization is assessed and the trends of its further development are outlined. This work is partially supported by Russian Foundation for Basic Research under grant N 00-07-90296.

The intention of the paper is to extend the testing methodology to a model of event structures with a discrete time domain. Alternative characterizations of time testing relations are provided. To achieve their decidability we have reduced timed testing relations to appropriate bisimulation one.

The polymodal logic based on A-spaces is considered.Modalities connected with A-spaces are interpreted as tense ones. The nearest and detached future or past are considered, i.e. four modalities are used. The tense modalities are especially important for studying the parallel computations and for a verification of programs. A set of axioms is described and a theorem of correctness is formulated for these axioms relative to frames based on A - spaces. Logic calculus L' is introduced, for that some theorem about a canonical model is formulated. A connection between fragments of L' and the well known logic S4 is established. The proofs are omitted in view of their cumbersomity.

In this writing the Sisal 90 language definition is presented. Sisal 90 supports modern functional and imperative language features. It increases the language's utility for scientific programming by adding features from Fortran 90 and support for mixed language programming.