On Store Languages and Applications

TL;DR

This paper introduces new algorithms and characterizations for store languages in various machine models, linking them to model checking and reachability problems, and demonstrating decidability of key properties.

Contribution

It provides novel characterizations of store languages and connects them to model checking, showing how complex machine behaviors can be simplified and analyzed.

Findings

Any nondeterministic pushdown automaton with reversal-bounded counters can be accepted by a machine with only reversal-bounded counters.

Many machine models can accept predecessor, successor, and common configurations with simpler models.

Decidability of emptiness, infiniteness, and disjointness properties is established for various machine models.

Abstract

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.