Constructing Specific SOS Semantics for Concurrency via Abstract Interpretation

摘要

Most of the SOS semantics for concurrent systems can be derived by abstracting on the inference rules of a concrete transition system, namely the proved transition system. Besides the standard interleaving semantics we mechanically derive the causal transition system for CCS, whose definition is particularly difficult and paradigmatic. Its rules are shown to coincide with those presented in the literature. Also, the tree of its computations coincide with that obtained by abstracting the computations of the proved transition system.