A Logic For Fresh Labelled Transition Systems

TL;DR

This paper introduces a logic for Fresh Labelled Transition Systems that can express properties involving fresh data generation and history, with analysis of model checking complexity.

Contribution

It develops a Hennessy-Milner logic with recursion for FLTSs, generalizing Fresh-Register Automata, and analyzes the model checking complexity using nominal sets.

Findings

Logic can express properties like infinite paths of distinct data.

Model checking reduces to parity games with exponential complexity.

Provides a formal framework for history-dependent automata on infinite alphabets.

Abstract

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 capture fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn are one of the simplest classes of history-dependent automata operating 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. In addition, the automaton can accept an input just if it be fresh: not seen in the computation before. The logic we introduce can express a variety of properties, such as the existence of an infinite path of distinct data values or the existence of a finite path where some taint property is violated. We study the model checking problem and its complexity via reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.