Polymorphic systems with arrays : decidability and undecidability
Ranko Lazić, Tom Newcomb, Andrew William Roscoe · Warwick Research Archive Portal (University of Warwick) · 2004
Abstract. Polymorphic systems with arrays (PSAs) is a general class of nondeterministic reactive systems. A PSA is polymorphic in the sense that it depends on a signature, which consists of a number of type variables, and a number of symbols whose types can be built from the type variables. Some of the state variables of a PSA can be arrays, which are functions from one type to another. We present several new decidability and undecidability results for the parameterised control-state reachability problem on subclasses of PSAs. 1