k-bisimulation: a new bisimulation for defining the dissimilarity between processes.

We propose the use of a bisimulation to quantify dissimilarity between processes: we call it k-bisimulation. Two processes p and q, whose semantics is given through transition systems, are k-bisimilar if they di↵er from at most k moves, where k is a natural number. Roughly speaking, the k-bisimulation captures the extension of the dissimilarity between p and q when they are neither strong nor weak equivalent. The importance of a formal concept of the k-bisimulation can be seen in several application fields, such as clone detection, process mining, business- IT alignment. We propose several heuristics in order to efficiently check such a bisimulation. The approach can be applied to di↵erent specification languages (CCS, LOTOS, CSP) provided that the language semantics is based on the notion of transition system. We have implemented a prototype tool and have conducted experiments on well-known systems for a proof of concept of our methodology.