Milan Hutten: Sound and Complete Axiomatizations for the rooted variants of Divergence-Preserving, Weak Divergence-Preserving and Stability-Respecting Branching Bisimilarity


Event Details


This thesis studies divergence and the extra complexity it adds to branching bisimilarity and axiomatizations with respect to branching bisimilarity. Aceto et al. provided sound and complete axiomatization with respect to rooted branching bisimilarity over basic CCS with the prefix iteration operator. Additionally, Spaninks, and Liu and Yu proposed sound and complete axiomatizations with respect to rooted divergence-preserving branching bisimilarity over basic CCS with the recursion construct. We contribute by providing a sound and complete axiomatization with respect to rooted divergence-preserving branching bisimilarity over basic CCS with the prefix iteration operator. Additionally, we provide sound and complete axiomatizations with respect to rooted weakly divergence-preserving branching bisimilarity and rooted stability-respecting branching bisimilarity over the same algebra and show that completeness of these axiomatizations and the axiomatization with respect to rooted branching bisimilarity provided by Aceto et al. can be derived from the completeness of the axiomatization with respect to rooted divergence-preserving branching bisimilarity. Lastly, we discuss how the prefix iteration operator can be expressed through the recursion construct and partially show how our proposed axiomatization is represented in the axiomatizations of Spaninks, and Liu and Yu.