A calculus of quality for robustness against unreliable communication
We extend the Quality Calculus, introduced to reason about unreliable communication. We provide a new explicit substitution semantics for the calculus. Such semantics allows to formally prove the correctness of the robustness analysis. It also leads to a novel way of treating explicit substitutions with structural rules. We prove the equivalence of the two semantics up to moving recursion to the transition rules.
robustness availability denial-of-service process calculus sat-solving