Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification
Ranko Lazić · Electronic Notes in Theoretical Computer Science · 2005
Many interesting systems can be seen as having two kinds of state variables: array variables, which are mappings from one data type into another; and basic variables, which are used to control the system, to perform basic computations, and for operations involving arrays. We investigate such systems where: • the type of each basic variable is built from type variables using product and sum constructs; • the type of each array variable is B → B ′ , where B and B ′ are types as for basic variables; • on any type variable, either no operations are available, or only the equality predicate, or only a linear-order predicate; • type variables denote arbitrary non-empty finite sets. We present a complete classification of reachability decision problems for these systems into decid- able or undecidable.