Harnessing LTL With Freeze Quantification
share
Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, respectively, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, where names play the role of data. For example, regular nondeterministic nominal automata (RNNA) are equivalent to a subclass of the standard register automata model, characterized by a lossiness condition referred to as name dropping. This subclass generally enjoys better computational properties than the full class of register automata, for which, e.g., inclusion checking is undecidable. Similarly, satisfiability in full freeze LTL is undecidable, and decidable but not primitive recursive if the number of registers is limited to at most one. In the present paper, we introduce a name-dropping variant bar-muTL of Freeze LTL for finite words over an infinite alphabet. We show by reduction to extended regular nondeterministic nominal automata (ERNNA) that even with unboundedly many registers, model checking for bar-muTL over RNNA is elementary, in fact in ExpSpace, more precisely in parametrized PSpace, effectively with the number of registers as the parameter.
READ FULL TEXT