On-The-Fly Bisimilarity Checking for Fresh-Register Automata.

Register automata are one of the simplest classes of automata that operate on infinite alphabets. Each automaton comes equipped with a finite set of registers where it can store data values and compare them with others from the input. Fresh-register automata are additionally able to accept a given data value just if it is fresh in the computation history. The bisimilarity problem for fresh-register automata is known to be in NP, when empty registers and duplicate register content are forbidden. In this paper, we investigate on-the-fly algorithms for solving bisimilarity, which attempt to build a bisimulation relation starting from a given input configuration pair. We propose an algorithm that uses concise representations of candidate bisimulation relations based on generating systems. While the algorithm runs in exponential time in the worst case, we demonstrate through a series of benchmarks its efficiency compared to existing algorithms and tools. We moreover implement a translation from pi-calculus processes to fresh-register automata, and use the latter to obtain a prototype (strong early) bisimilarity checking tool for finitary pi-calculus processes.