串并行图上逆转有界自动机的可达性分析

对字符串上有限状态自动机的扩展，如多磁头自动机或多计数器自动机，已成功用于编码许多无限状态非正则验证问题。本文将自动机理论的无限状态验证从字符串推广到带标签的串并行图。我们定义了一种在非确定性、双向、并发自动机模型，其在串并行图上工作并通过图上节点的共享寄存器进行通信。我们考虑如下验证问题：给定一个由上下文无关图变换系统（GTS）描述的串并行图族，以及一个关于串并行图的并发自动机，是否存在由 GTS 生成的图被该自动机接受？该一般问题即使对于字符串上的（单向）多磁头自动机也是不可判定的。我们证明了一个有界版本是可判定的，其中自动机沿图进行固定次数的逆转并使用固定数量的共享寄存器，即使 GTS 生成的串并行图的大小无界。我们的可判定性结果基于确立上下文切换次数有界，以及对有界并发自动机计算进行编码，从而将空性问题归约到下推自动机的空性问题。