Preprints of IIS SB RAS, 2000

Preprint 82
V. E. Kozura
Unfoldings of timed coloured petri nets

In the paper [10] the unfolding technique was applied to coloured Petri nets (CPN) [8,9]. It was also shown in [10] how to use the unfolding technique taking into consideration symmetry or equivalence specifications. In [1] unfolding technique was applied to interval-timed Petri nets. This paper transfers this technique to interval-timed CPN and also considers the unfolding technique for timed CPN (TCPN) [8,9]. We require CPN to be finite, n-safe and containing only finite sets of colours.

Preprint 80
V. E. Kozura
Unfoldings of coloured petri nets

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.

Preprint 79
M. Yu. Loenko
Improving of an external estimation of the solution set to constraint satisfaction problems

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.

Preprint 78
E. V. Okunishnikova
Coloured petri nets approach to the validation of dynamic estelle-specifications

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.

Preprint 77
M. V. Andreeva
Concurrent variants of may-testing equivalences for timed event structures

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

Preprint 76
Ivan A. Lisitsyn
Graph visualization and editing systems

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.

Preprint 75
Elena N. Bozhenkova
The investigation of the equivalences of the event stuctures with descrete time

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.

Preprint 73
V.F. Murzina
The polymodal logic based on a-spaces

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.

Preprint 72
Yulia V. Biryukova
Sisal 90 user tutorial

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.

Preprint 71
T. G. Churina
Coloured petri nets approach to the validation of dynamic sdl-specifications

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




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.