Quantifying the Similarity of Non-bisimilar Labelled Transition Systems

Organisation:	Univ. Grenoble Alpes, LIG, and Inria Grenoble - Rhône-Alpes (FRANCE)
Functionality:	System Design
Tools used:	Python CADP (Construction and Analysis of Distributed Processes)
Period:	2021
Description:	Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Model-based verification methods, which work on LTS (Labelled Transition System) models of distributed systems, enable to automatically chase and find bugs that would be very difficult, if not impossible, to detect manually. Equivalence checking determines whether two LTSs (typically modelling the requirements and the implementation) are equivalent modulo a bisimulation relation. When the LTSs are not equivalent, the checker returns a Boolean verdict accompanied by a counterexample, which is typically a sequence of actions that, when executed in the two LTSs, leads to a couple of non-equivalent states. However, this counterexample does not give any indication of how far the two LTSs are one from another. One can wonder whether they are almost identical or totally different, which is not the same situation from a design or debugging point of view. This work proposes a set of metrics for quantifying the similarity of two behavioural models described using LTSs. The approach starts by computing the classes of bisimilar and non-bisimilar states using partition refinement. Then, a set of global and local metrics for each couple of non-bisimilar states is computed, which enables to build a matrix with a measure between 0 (totally different states) and 1 (bisimilar states) for each couple of states. This is done by combining several criteria, such as the matching of incoming/outgoing transitions, the similarity of neighbour states, the shortest distance from the initial state, and the distance to the closest bisimilar state. Finally, a global measure of similarity of both LTSs is computed based on this matrix. The computation of partition refinement, matrix, and similarity measures was implemented in the DLTS tool, which takes as inputs two LTSs in the textual AUT format (obtained by compiling LNT formal descriptions using the CADP compilers). DLTS was applied on about 200 LTSs, and its usage is illustrated on two case-studies in different areas: Internet of Things (conformance between a candidate composition of devices and a goal composition) and BPMN business process engineering (detection of similarities between a process and its evolved version).
Conclusions:	Better understanding and measuring the difference between two behavioural models can be of interest in many different contexts and application areas. For instance, it can be used for debugging purposes when the equivalence checking counterexample is not sufficient for detecting the source of the bug, for measuring the distance between two versions of a software, and for process model matching in the context of business process management.
Publications:	[Salaun-21] Gwen Salaün. "Quantifying the Similarity of Non-bisimilar Labelled Transition Systems". Science of Computer Programming 202, 2021. Available on-line at: http://hal.inria.fr/hal-03017666/en or from the CADP Web site in PDF or PostScript
Contact:	Gwen Salaün Inria Grenoble - Rhône-Alpes 655, avenue de l'Europe 38330 Montbonnot Saint Martin FRANCE Email: gwen.salaun@inria.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page