On the Boundedness Problem for Higher-Order ...
Type de document :
Communication dans un congrès avec actes
Titre :
On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems
Auteur(s) :
Penelle, Vincent [Auteur]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
Salvati, Sylvain [Auteur]
Linking Dynamic Data [LINKS]
Sutre, Grégoire [Auteur]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
Salvati, Sylvain [Auteur]
Linking Dynamic Data [LINKS]
Sutre, Grégoire [Auteur]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
Titre de la manifestation scientifique :
FSTTCS 2018 - 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Ville :
Ahmedabad
Pays :
Inde
Date de début de la manifestation scientifique :
2018-12-10
Titre de la revue :
LIPIcs
Éditeur :
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
Mot(s)-clé(s) en anglais :
Higher-order pushdown automata
Vector addition systems
Boundedness problem
Termination problem
Coverability problem
Vector addition systems
Boundedness problem
Termination problem
Coverability problem
Discipline(s) HAL :
Informatique [cs]/Théorie et langage formel [cs.FL]
Informatique [cs]/Logique en informatique [cs.LO]
Informatique [cs]/Logique en informatique [cs.LO]
Résumé en anglais : [en]
Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later ...
Lire la suite >Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness.We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.Lire moins >
Lire la suite >Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness.We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.archives-ouvertes.fr/hal-01962407/document
- Accès libre
- Accéder au document
- https://hal.archives-ouvertes.fr/hal-01962407/document
- Accès libre
- Accéder au document
- LIPIcs-FSTTCS-2018-44.pdf
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document