Push-Down Automata with Gap-Order Constraints - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Push-Down Automata with Gap-Order Constraints

Parosh Aziz Abdulla
  • Fonction : Auteur
  • PersonId : 1007031
Mohamed Faouzi Atig
  • Fonction : Auteur
  • PersonId : 998103
Andreas Podelski
  • Fonction : Auteur
  • PersonId : 1007032

Résumé

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.
Fichier principal
Vignette du fichier
978-3-642-40213-5_13_Chapter.pdf (158.32 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01514667 , version 1 (26-04-2017)

Licence

Paternité

Identifiants

Citer

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Giorgio Delzanno, Andreas Podelski. Push-Down Automata with Gap-Order Constraints. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.199-216, ⟨10.1007/978-3-642-40213-5_13⟩. ⟨hal-01514667⟩
174 Consultations
128 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More