REACH on Register Automata via History Independence

Register automata are an expressive model of computation using finite memory. Conformance checking of their properties can be reduced to NONEMPTINESS tests, however, this problem is PSPACE -complete. Existing approaches usually employ symbolic state exploration. This results in state explosion for most complex register automata. We propose a semantics-preserving transformation of register automata into a representation in which reachability of states is equivalent to reachability of locations, i.e., is in NL. We evaluate the algorithm on random-generated and real-world automata and show that it avoids state explosion and performs better on most instances than a comparable existing approach. This yields a practical approach to conformance checking of register automata.