论文标题
线性时间名义$μ$ $ - 级别的名称分配
A Linear-Time Nominal $μ$-Calculus with Name Allocation
论文作者
论文摘要
无限字母的语言的逻辑和自动机模型，例如冻结LTL和注册自动机，可验证流程或文档的数据。它们与名义集的形式主义紧密相关，例如非确定性的轨道轨道自动机（NOFAS），其中名称起着数据的作用。这种形式主义中的推理问题在计算上往往很难。名称结合标称自动机模型，例如常规的非确定性标称自动机（RNNA），已显示出更容易拖动的计算。在本文中，我们在无限字母上引入了一个线性时间fixpoint逻辑棒，用于有限单词，该字母具有完整的否定和通过名称绑定的冻结定量。我们通过非平凡的减少来表明扩展常规的非确定性名义自动机，即使BAR-MUTL允许不受限制的非确定性和无限的寄存器，模型对RNNA的模型进行了检查，并且对RNNAS进行了检查，并且可满足性检查都具有基本的复杂性。例如，模型检查位于2expspace中，更精确地在参数化的expspace中，有效地将寄存器数量作为参数。
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.
