论文标题
在商店语言和应用程序上
On Store Languages and Applications
论文作者
论文摘要
某种任意类型的机器的存储语言是所有商店配置的集合（State Plus商店内容，而不是输入），可以显示在接受计算中。获得了商店语言的新算法和表征，例如，任何不确定性的俯卧撑自动机都会随着相反的柜台增强的结果，在这些柜台上可以将其内容“翻转”到有限的次数，只有一台机器就可以接受逆转柜台的机器。然后，在商店语言和几种模型检查和可及性问题之间进行连接，例如从给定的一组配置中接受所有前身和后继配置的集合，并确定在接受两台计算机的计算之间是否至少有一个或无限的常见配置。这些经常包含多个并行数据存储的各种不同的机器模型进行了探索。所研究的许多机器模型都可以接受一组先前的配置（一组常规配置），一组后继配置以及两台机器之间的一组常见配置，具有比本身更简单的机器模型，具有可决定性的空虚，无限性和差异性属性。商店语言是显示这些属性的关键。
The store language of a machine of some arbitrary type is the set of all store configurations (state plus store contents but not the input) that can appear in an accepting computation. New algorithms and characterizations of store languages are obtained, such as the result that any nondeterministic pushdown automaton augmented with reversal-bounded counters, where the pushdown can "flip" its contents up to a bounded number of times, can be accepted by a machine with only reversal-bounded counters. Then, connections are made between store languages and several model checking and reachability problems, such as accepting the set of all predecessor and successor configurations from a given set of configurations, and determining whether there are at least one, or infinitely many, common configurations between accepting computations of two machines. These are explored for a variety of different machine models often containing multiple parallel data stores. Many of the machine models studied can accept the set of predecessor configurations (of a regular set of configurations), the set of successor configurations, and the set of common configurations between two machines, with a machine model that is simpler than itself, with a decidable emptiness, infiniteness, and disjointness property. Store languages are key to showing these properties.
