gLTSdiff: Generalized LTS differencing

gLTSdiff is a library for comparing the structures of two or more Generalized Labeled Transition Systems (GLTSs), and merging them into a single combined GLTS. gLTSdiff can be used and customized to compare and merge various types of directed graphs, labeled transition systems (LTSs), state machines, automata, and so on.

Out of the box, GLTs, LTSs, automata and difference automata can be compared. Their comparison can be configured to use different comparison algorithms that allow for a trade-off between performance and the number of differences in the result. The result may be post-processed to get rid of undesired patterns in the comparison result. Furthermore, gLTSdiff is designed with extensibility in mind. You may add your own representations, and customize the comparison, merging, output, and so on.

gLTSdiff is a generalization of the LTSdiff algorithm proposed by Neil Walkinshaw and Kirill Bogdanov, and implemented in the StateChum library. gLTSdiff is however more than only a generalization. It also offers significant performance improvements over LTSdiff, and adds additional features like post-processing to improve comparison results. gLTSdiff was first introduced, and formally defined, in the following article: Dennis Hendriks and Wytse Oortwijn, "gLTSdiff: A Generalized Framework for Structural Comparison of Software Behavior", 26th International Conference on Model Driven Engineering Languages and Systems (MODELS), 2023, to appear.

Examples

To get a feel of what is possible with gLTSdiff, here are a few simple examples.

Comparison of difference automata

Two difference automata (in red and green) may be compared and combined. Their common parts are shown in black, while their differences remain in red and green: