%0 Conference Proceedings
%T Push-Down Automata with Gap-Order Constraints
%+ Uppsala University
%+ Università degli studi di Genova = University of Genoa (UniGe)
%+ University of Freiburg
%A Abdulla, Parosh, Aziz
%A Atig, Mohamed, Faouzi
%A Delzanno, Giorgio
%A Podelski, Andreas
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 5th International Conference on Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Farhad Arbab
%Y Marjan Sirjani
%I Springer Berlin Heidelberg
%3 Fundamentals of Software Engineering
%V LNCS-8161
%P 199-216
%8 2013-04-24
%D 2013
%R 10.1007/978-3-642-40213-5_13
%Z Computer Science [cs]Conference papers
%X We consider push-down automata with data (Pdad) that operate on variables ranging over the set of natural numbers. The conditions on variables are defined via gap-order constraint. Gap-order constraints allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. The messages inside the stack are equipped with values that are natural numbers reflecting their “values”. When a message is pushed to the stack, its value may be defined by a variable in the program. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in two dimensions, namely we have a stack that may contain an unbounded number of messages each of which is equipped with a natural number. We present an algorithm for solving the control state reachability problem for Pdad based on two steps. We first provide a translation to the corresponding problem for context-free grammars with data (Cfgd). Then, we use ideas from the framework of well quasi-orderings in order to obtain an algorithm for solving the reachability problem for Cfgds.
%G English
%2 https://inria.hal.science/hal-01514667/document
%2 https://inria.hal.science/hal-01514667/file/978-3-642-40213-5_13_Chapter.pdf
%L hal-01514667
%U https://inria.hal.science/hal-01514667
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ IFIP-LNCS-8161