Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as regular nondeterministic nominal automata (RNNAs) have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-muTL for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-muTL allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-muTL over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.

翻译：用于无限字母语言的逻辑和自动数学模型,例如冻结 LTL 和注册自动地图,用于核查带有数据的流程或文件。它们与标称组的正规主义关系密切,例如非确定性轨道-无限自动地图(NOFAs),名称在其中起着数据的作用。在这种形式化中引起问题的原因往往在计算上是硬的。在常规非确定性名义自动地图(RNNAs)中,带有名称约束性的名义自动模型(Automatas)被证明更便于计算。在本文中,我们为无限字母的限定词引入线性固定点逻辑 Bar-muTL,其特征是完全否定和通过名称绑定冻结量化。我们通过非边际缩减来扩展非确定性名义自动模型,即使Bar-muTL允许不受限制的非确定性和非约束性名义自动自动登记册(RNNNAs),模型检查 Bar-muTL 相对于RNNNAs和对等兼容性核对都具有基本的复杂性。例如,模型检查是在空间空间数据库中以2Explasmissional Stormationslationsormationslateslationslationslations。