3:30 pm, Seminar Hall Data Multipushdown automata C. Aiswarya Chennai Mathematical Institute. 280817 Abstract We extend the classical model of multipushdown systems by considering systems that operate on a finite set of variables ranging over natural numbers. The conditions on variables are defined via gaporder constraints that allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. Furthermore, each message inside a stack is equipped with a data item representing its value. When a message is pushed to the stack, its value may be defined by a variable. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in multiple dimensions, namely we have a number of stacks that may contain an unbounded number of messages each of which is equipped with a natural number. It is wellknown that the verification of any non trivial property of multipushdown systems is undecidable, even for two stacks and for a finite datadomain. In this paper, we show the decidability of the reachability problem for the classes of data multipushdown system that admit a bounded splitwidth (or equivalently a bounded treewidth). As an immediate consequence, we obtain decidability for several subclasses of data multipushdown systems. These include systems with single stacks, restricted ordering policies on stack operations, bounded scope, bounded phase, and bounded context switches. This is a joint work with Parosh Aziz Abdulla and Mohamed Faouzi Atig (CONCUR 17).
