Representing CCS programs by finite predicate-transition nets

DOI10.1007/BF00277389MaRDI QIDQ1122360zbMATH OpenOpenAlexFDO

Authors Dirk Taubner

Publication date 1990

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00277389

zbMATH Keywords

CCS programsconcurrencydistributed semanticshidinginterleaving semanticsparallel synchronizationpredicate-transition netrenamingrestriction

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

A construction is given which for every CCS program (in which every choice and recursion starts sequentially) yields a finite and strict predicate/transition net. The main idea is to put the dynamically growing information about action manipulation (i.e. renaming, hiding, restriction) and parallel synchronization into the tokens of the net. All other information is static and can be encoded in the structure of the net. Consistency of this construction is proved not only with respect to the standard interleaving semantics but with respect to the distributed semantics of Degano, De Nicola and Montanari which additionally models the concurrency explicitly.

Recommendations

• scientific article; zbMATH DE number 4060688
• scientific article; zbMATH DE number 3896316
• Finite representations of CCS and TCSP programs by automata and Petri nets
• scientific article; zbMATH DE number 3911719
• Language representability of finite P/T nets

Cited in

(11)

• Finite representations of CCS and TCSP programs by automata and Petri nets
• Presheaf models for CCS-like languages
• Nested-unit Petri nets
• Nested-unit Petri nets: a structural means to increase efficiency and scalability of verification on elementary nets
• The Decidability of the Reachability Problem for CCS!
• Language representability of finite P/T nets
• scientific article; zbMATH DE number 3896316 (Why is no real title available?)
• scientific article; zbMATH DE number 3911719 (Why is no real title available?)
• scientific article; zbMATH DE number 4060688 (Why is no real title available?)
• scientific article; zbMATH DE number 1231669 (Why is no real title available?)
• scientific article; zbMATH DE number 4001493 (Why is no real title available?)

This page was built for publication: Representing CCS programs by finite predicate-transition nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1122360)