Fault-tolerant bisimulation and process transformations

Abstract

We provide three methods of verifying concurrent systems which are tolerant of faults in their operating environment - algebraic, logical and transformational. The first is an extension of the bisimulation equivalence, the second is rooted in the Hennessy-Milner logic, and the third involves transformations of CCS processes. Based on the common semantic model of labelled transition systems, which is also used to model faults, all three methods are proved equivalent for certain classes of faults.