Model Checking Polymorphic Systems with Arrays

Speaker: Ranko Lazic

27th October 2004 , 2pm , Room 519, Claremont Tower

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 a complete classification of parameterised reachability problems on subclasses of PSAs into decidable or undecidable.

-------
Ranko Lazic
Department of Computer Science
University of Warwick