Push-Down Automata with Gap-Order Constraints

Abstract : 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.
Type de document :
Communication dans un congrès
Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.199-216, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_13〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01514667
Contributeur : Hal Ifip <>
Soumis le : mercredi 26 avril 2017 - 15:22:10
Dernière modification le : mercredi 26 avril 2017 - 15:26:38
Document(s) archivé(s) le : jeudi 27 juillet 2017 - 12:50:16

Fichier

978-3-642-40213-5_13_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Parosh Abdulla, Mohamed Atig, Giorgio Delzanno, Andreas Podelski. Push-Down Automata with Gap-Order Constraints. Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.199-216, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_13〉. 〈hal-01514667〉

Partager

Métriques

Consultations de la notice

135

Téléchargements de fichiers

90