Dierl, S.S.DierlHowar, FalkFalkHowar2022-10-172022-10-172022https://publica.fraunhofer.de/handle/publica/42770210.1007/978-3-031-09827-7_22-s2.0-85134320132Register 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.enConformance checkingConstraint projectionHistory independenceModel checkingNon-emptinessReachabilityRegister automataconference paper