Catálogo de publicaciones - libros

Design of modern discrete devices and systems often deals with parallel processes and structures. For that reason practically all modern hardware design languages and formalisms used for system specification (such as VHDL, Verilog) allow describing concurrency. Design of complex, VLSI-based electronic devices is possible only with the help of CAD systems, so the design and verification methods have to be (and mostly are) formalized. Formalization and automatization of system design requires developing of formal models for parallel discrete systems and low-level description languages based on these models.

This section contains definitions of main models used in the book and their properties. Other necessary definitions will appear in the text when correspondent notions will be introduced; they, unlike the definitions in this section, will be numbered.

Content of this section relates to the parallel discrete systems in general sense, unless otherwise stated.

A perspective approach to analysis of Petri nets and, generally, of parallel discrete systems, is based on the idea of decomposition. The task of net analysis is reduced to the task of analysis of the blocks of its decomposition, which may be considerably smaller than the net itself. That procedure can simplify analysis of large nets. Decomposition turns to be useful also for the synthesis purposes. More about theory and applications of net decomposition can be found in [15, 19, 36, 102, 169, 249, 251].

This chapter is dedicated to one of the important Petri net analysis tasks - calculation of siphons and traps. For some classes of Petri nets (and their extensions) properties like liveness and reversibility can be decided by analysis of siphons and traps [21, 28, 155, 176, 194, 228, 241, 249] - for example, there is a known result that a free choice net is live, if and only if every siphon contains a marked trap [140, 183]. Finding siphons and traps has a variety of applications to verification and design of parallel systems, such as detection and prevention of deadlocks (usually in a correct system no siphon can be emptied) [65, 81, 92]; one application of this kind will be presented below in Subsection 6.1.3.

Reachability graph of an interpreted Petri net is a subgraph of the reachability graph of the underlying net , because an interpretation can reduce possibilities of the net evolution and never can expand them. RRG , constructed for , is a subgraph of , but not necessarily of ; so can miss some information, important for analysis of .

Programming and hardware design languages, allowing to describe parallel processes, are widely used nowadays. Also, parallel formal models are widely used in the systems of computer-aided design of discrete devices. This is natural for the current level of development of system engineering and logical design, because practically every non-primitive software or hardware system, from logical control devices to multithread software applications, consists of concurrently acting objects.