A logical view of composition

DOI10.1016/0304-3975(93)90151-IMaRDI QIDQ685416zbMATH OpenOpenAlexFDO

Authors Martín Abadi, Gordon D. Plotkin

Publication date 13 January 1994

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(93)90151-i

zbMATH Keywords

compositionalityconcurrent programmingintuitionistic logiclinear logicmodular specificationsafety properties

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification approaches; one of the logics is intuitionistic, while the other one is linear.

Recommendations

• An abstract account of composition
• scientific article; zbMATH DE number 2087508
• Logical specification of reactive and real-time systems
• Safe Reasoning with Logic LTS
• Composing and refining dense temporal logic specifications

Cites work

• Domain theory in logical form
• From Petri nets to linear logic
• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 3930354 (Why is no real title available?)
• scientific article; zbMATH DE number 3938541 (Why is no real title available?)
• scientific article; zbMATH DE number 4059362 (Why is no real title available?)
• scientific article; zbMATH DE number 3716749 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 46487 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 3624763 (Why is no real title available?)
• scientific article; zbMATH DE number 1028818 (Why is no real title available?)
• scientific article; zbMATH DE number 194916 (Why is no real title available?)
• Linear logic
• Proofs of Networks of Processes
• Quantales and (noncommutative) linear logic
• Quantales, observational logic and process semantics
• Specifying Concurrent Program Modules
• Testing equivalences for processes

Cited in

(22)

• An explanatory presentation of composition rules for assumption- commitment specifications
• Theory and methodology of assumption/commitment based system interface specification and architectural contracts
• Aspects of compositionality
• Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
• On hierarchically developing reactive systems
• AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES
• An abstract account of composition
• Safe Reasoning with Logic LTS
• Automated Compositional Reasoning of Intuitionistically Closed Regular Properties
• Autonomous posets and quantales
• scientific article; zbMATH DE number 2087508 (Why is no real title available?)
• Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
• Safe reasoning with logic LTS
• Retracing some paths in process algebra
• Assumption/guarantee specifications in linear-time temporal logic
• On using temporal logic for refinement and compositional verification of concurrent systems
• Lazy compositional verication
• The need for compositional proof systems: a survey
• Concurrent IMP
• ConcurrentHOL
• Conjunction on processes: Full abstraction via ready-tree semantics
• Ready simulation for concurrency: it's logical!

This page was built for publication: A logical view of composition

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