Process Equivalence Problems as Energy Games

TL;DR

This paper introduces a 6-dimensional energy game framework to characterize behavioral equivalences and preorders in process theory, providing an exponential-time decision method that matches the complexity of trace equivalence.

Contribution

It presents a novel energy game approach that unifies various behavioral equivalences and preorders, improving decision complexity over previous methods.

Findings

Algorithm performs comparably to the best similarity algorithms on VLTS benchmarks.

Decides all common behavioral equivalences within exponential time.

Unifies multiple behavioral equivalences through a single energy game model.

Abstract

We characterize all common notions of behavioral equivalence by one 6-dimensional energy game, where energies bound capabilities of an attacker trying to tell processes apart. The defender-winning initial credits exhaustively determine which preorders and equivalences from the (strong) linear-time--branching-time spectrum relate processes. The time complexity is exponential, which is optimal due to trace equivalence being covered. This complexity improves drastically on our recent approach for deciding groups of equivalences where exponential sets of distinguishing HML formulas are constructed on top of a super-exponential reachability game. In experiments using the VLTS benchmarks, the algorithm performs on par with the best similarity algorithm.