Novosibirsk, 2007
In the monograph, a wide range of behavioral equivalences has been proposed and investigated on the well-known models for concurrent systems specification and analysis such as Petri nets and process algebras. The equivalence relations have been explored on subclasses and extensions of the models: time and stochastic Petri nets and stochastic process algebras. On Petri nets both with and without silent transitions and their subclasses a wide set of basic, back-forth and place behavioural equivalences were proposed and investigated in the semantics ranged from interleaving to true concurrent as well as from linear to branching time ones. On time Petri nets both with and without silent transitions and their subclasses a number of time, untime and regional equivalences were proposed and investigated in interleaving and step semantics as well as in trace and bisimulation ones. Semantic equivalences of standard and stochastic process algebras are investigated, and a coherence between them and the net equivalence relations is clarified. An algorithm of automatic formula comparison for the semantic equivalence is designed and implemented. For graduate and post-graduate students and researchers interested in theoretical computer science, in particular, formal modeling and analysis of behavioural properties of concurrent systems and processes.
Keywords: standard, time and stochastic Petri nets, subclasses, standard and stochastic process algebras, invisible transitions and actions, behavioural and semantic equivalences, bisimulation, temporal and probabilistic logics, reduction, refinement and composition, congruence, axiomatization, term rewrite systems, implementation.
The book can be purchased in the internet shop of SB RAS Publisher or in the Akademkniga bookshop (22, Morskoj pr., 630090 Novosibirsk, Russia. Phone: +7 383 330 09 22).