We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.

Register automata are one of the simplest classes of automata that operate on infinite input 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. One such use for this is representing processes in the π-calculus, where private names need to be fresh with respect to any process context. 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 define and implement a novel translation from π-calculus processes to fresh-register automata, and use the latter to obtain a (strong early) bisimilarity checking tool for finitary π-calculus processes. Using a series of benchmarks for this, we demonstrate an improvement in run-time compared to another equivalence checker.