An Epistemic Proof System for Parallel Processes**A full version appeared as Technical Report No. 93-17.

1994 ◽  
pp. 243-254 ◽  
Author(s):  
M. van Hulst ◽  
J.-J.Ch. Meyer
Keyword(s):  
Proof System ◽  
Full Version ◽  
Parallel Processes ◽  
Technical Report

scholarly journals A Cook's Tour of Countable Nondeterminism

1981 ◽  
Vol 10 (133) ◽  
Author(s):  
K. R. Apt ◽  
Gordon D. Plotkin
Keyword(s):  
Programming Language ◽  
Partial Orders ◽  
Proof System ◽  
Weakest Precondition ◽  
Full Version ◽  
Total Correctness ◽  
Soundness And Completeness

<p>We provide four semantics for a small programming language involving unbounded (but countable) nondeterminism. These comprise an operational one, two denotational ones based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. We also introduce a Hoare-like proof system for total correctness and show its soundness and completeness in an appropriate sense. Admission of countable nondeterminism results in a lack of continuity of various semantic functions; moreover some of the partial orders considered are in general not cpo's and in proofs of total correctness one has to resort to the use of (countable) ordinals. Proofs will appear in the full version of the paper.</p>

scholarly journals A Compositional Proof System on a Category of Labelled Transition Systems

1989 ◽  
Vol 18 (294) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Category Theory ◽  
Proof System ◽  
Parallel Composition ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Proof Systems ◽  
Categorical Logic ◽  
Parallel Processes ◽  
System A ◽  
Categorical Constructions

This paper presents an attempt to cast labelled transition systems, and other models of parallel computation, in a category-theoretic framework. One aim is to use category theory to provide abstract characterisations of constructions like parallel composition valid throughout a range of different models and to provide formal means for translating between different models. Another aim is to exploit the framework of categorical logic to systematise specification languages and the derivation of proof systems for parallel processes. After presenting a category of labelled transition systems, its categorical constructions are used to establish a compositional proof system. A category of properties of transition systems indexed by the category of labelled transition systems is used in forrning the proof system.

Sign in / Sign up

Export Citation Format

Share Document