Abstract
Among formal models proposed to specify concurrent systems and processes, three main groups emerged. They can be referred to as net models, algebraic calculi and process logics. Each group supports specific abstraction methodology and possesses different descriptive and analytical power. These two abilities are, to some extent, contradictory and usually are exploited separately in theoretical studies. However, their combination is highly desirable in practical tools for the verification and synthesis of systems. This stimulates the comparative studies of different classes of models with cross-interpretation of their basic notions and primitives. Some efforts to combine their advantages in the framework of unified theories are now in progress. The models based on Petri nets seem to be the most close to the adequate description of “pure” concurrency. As a result, many net- -based models were proposed for the formal specification and validation of concurrent systems: control structures in parallel programs, circuitry design, net protocols, etc. However, these models, providing a good insight into structural properties of designed concurrent systems, do not contain sufficient support for the validation of behavioural properties and equivalencies. This forces to have recources to some “external” formalisms. For example, having a net description of a system, we use firing sequences, traces, net languages, etc. to define and analyze the net properties. It would be more convenient if both descriptive and analytical parts of a modelling theory were based on the same set of basic notions and constructors.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Petri C.A. Hon-sequential processes. — ISF-Report-77.05, St. Augustin: Gesellschaft für Mathematik und Datenverarbeitung, 1971, 31 p.
Kotov V.E., Cherkasova L.A. On structural properties of generalized processes. — Lecture Notes in Computer Science, 188, Springer-Verlag, Berlin, 1984, p. 288–306.
Harel D. first-order dynamic logic. — Lecture Notes in Computer Science, 68, Springer—Verlag, Berlin, 1979.
Fisher M.J., Ladner R.E. Propositional dynamic logic of regular programs. — J. Comput. on System Science, 18(2), 1979, p. 197–211.
Pratt V.R. Process logic. — Proc. ACM Symp. on Principles of Programming Languages, 1979, p. 93–100.
Manna Z., Pnueli A. Verification of concurrent programs: temporal proof principles. — Lecture Notes in Computer Science, Springer-Verlag, Berlin, v. 131, 1981, p. 200–252.
Best E. The relative strength of K-density. — Lecture Notes in Computer Science, Springer-Verlag, Berlin, v. 84, 1980, p.261–276.
Kotov V.E. An algebra for parallelism based on Petri nets. — Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1978, p. 39–55.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kotov, V.E., Cherkasova, L.A. (1987). From Nets to Logic and Back in the Specification of Processes. In: Voss, K., Genrich, H.J., Rozenberg, G. (eds) Concurrency and Nets. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-72822-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-72822-8_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-72824-2
Online ISBN: 978-3-642-72822-8
eBook Packages: Springer Book Archive