发表机构
Uppsala University; The Institute of Mathematical Sciences, Homi Bhabha National Institute; Chennai Mathematical Institute（乌普萨拉大学; 霍米·巴哈国家研究所数学科学研究所; 金奈数学研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文研究无限数据域上并发寄存器机的参数化可达性问题，证明一般情况为Pspace-完全，在新鲜性假设下不可判定，并给出两种受限设置的最优可判定性结果。
AI 中文摘要
我们研究了无限数据域上并发寄存器机的参数化可达性问题。在此框架中，每台机器是一个配备一组本地寄存器的程序，机器间的通信通过一组共享寄存器进行中介。本地寄存器和共享寄存器都可以从无限数据域中取值。程序的基本操作包括在寄存器之间复制值、赋值常量、比较寄存器是否（不）相等，以及将任意域值存储到本地寄存器中的非确定性赋值。参数化可达性问题考虑一个程序和一个目标位置，询问是否存在某个自然数 n，使得 n 个相同机器（称为实例）的执行导致至少一个实例到达指定位置。我们证明该问题在一般情况下是 Pspace-完全的，并且如果对非确定性赋值应用新鲜性假设（即每次赋值必须产生一个与所有常量不同的唯一值），则该问题变得不可判定。即使系统限制为两个共享寄存器和两个本地寄存器，这种不可判定性仍然存在。最后，我们为两种受限设置建立了最优可判定性结果：当每个线程仅限于一个本地寄存器时，或者当系统仅使用一个共享寄存器时。
英文摘要
We investigate the parameterized reachability problem for concurrent register machines over infinite data domains. In this framework, each machine is a program equipped with a set of local registers, the communication across machines is mediated through a set of shared registers. Both local and shared registers can take values from an infinite data domain. The program's primitive operations include copying values between registers, assigning constants, comparing registers for (dis-)equality, and nondeterministic assignments that store an arbitrary domain value into a local register. The parameterized reachability problem considers a program and a target location, asking whether there exists some n in Naturals such that an execution of n identical machines (referred to as instances) results in at least one instance reaching the specified location. We show that this problem is Pspace-complete in the general case and it becomes undecidable if a freshness assumption (i.e., each assignment must produce a unique value distinct from all constants) is applied to nondeterministic assignments. This undecidability persists even for systems restricted to two shared and two local registers. Finally, we establish optimal decidability results for two restricted settings: when each thread is limited to a single local register, or when the system utilizes only one shared register.
