ﻻ يوجد ملخص باللغة العربية
Proposition algebra is based on Hoares conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so-called free valuation congruence: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Free valuation congruence is axiomatized by the four basic equational axioms of proposition algebra that define the conditional connective. Valuation congruences that identify more conditional statements than free valuation congruence are repetition-proof, contractive, memorizing, and static valuation congruence. Each of these valuation congruences is characterized using a transformation on evaluation trees: two conditional statements are C-valuation congruent if, and only if, their C-transformed evaluation trees are equal. These transformations are simple and natural, and only for static valuation congruence a slightly more complex transformation is used. Also, each of these valuation congruences is axiomatized in proposition algebra. A spin-off of our approach can be called normalization functions for proposition algebra: for each valuation congruence C considered, two conditional statements are C-valuation congruent if, and only if, the C-normalization function returns equal images.
We add probabilistic features to basic thread algebra and its extensions with thread-service interaction and strategic interleaving. Here, threads represent the behaviours produced by instruction sequences under execution and services represent the b
In this paper, we extend the theory CCS for trees (CCTS) to value-passing CCTS (VCCTS), of which symbols have the capacity for receiving and sending data values, and a nonsequential semantics is proposed in an operational approach. In this concurrent
This paper provides a fully abstract semantics for value-passing CCS for trees (VCCTS). The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. The labelled transition semantics is no
Terms are a concise representation of tree structures. Since they can be naturally defined by an inductive type, they offer data structures in functional programming and mechanised reasoning with useful principles such as structural induction and str
We present a process algebra based approach to formalize the interactions of computing devices such as the representation of policies and the resolution of conflicts. As an example we specify how promises may be used in coming to an agreement regardi