The reachability problem for ground TRS and some extensions
Identifieur interne : 001381 ( Istex/Curation ); précédent : 001380; suivant : 001382The reachability problem for ground TRS and some extensions
Auteurs : A. Deruyver [France] ; R. Gilleron [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The reachability problem for term rewriting systems (TRS) is the problem of deciding, for a given TRS S and two terms M and N, whether M can reduce to N by applying the rules of S. We show in this paper by some new methods based on algebraical tools of tree automata, the decidability of this problem for ground TRS's and, for every ground TRS S, we built a decision algorithm. In the order to obtain it, we compile the system S and the compiled algorithm works in a real time (as a fonction of the size of M and N). We establish too some new results for ground TRS modulo different sets of equations : modulo commutativity of an operator σ, the reachability problem is shown decidable with technics of finite tree automata; modulo associativity, the problem is undecidable; modulo commutativity and associativity, it is decidable with complexity of reachability problem for vector addition systems.
Url:
DOI: 10.1007/3-540-50939-9_135
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001398
Links to Exploration step
ISTEX:5555FA46CA0AFEA78DEA1606327828BC26173885Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">The reachability problem for ground TRS and some extensions</title><author><name sortKey="Deruyver, A" sort="Deruyver, A" uniqKey="Deruyver A" first="A." last="Deruyver">A. Deruyver</name><affiliation wicri:level="1"><mods:affiliation>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex</wicri:regionArea></affiliation></author><author><name sortKey="Gilleron, R" sort="Gilleron, R" uniqKey="Gilleron R" first="R." last="Gilleron">R. Gilleron</name><affiliation wicri:level="1"><mods:affiliation>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex</wicri:regionArea></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5555FA46CA0AFEA78DEA1606327828BC26173885</idno><date when="1989" year="1989">1989</date><idno type="doi">10.1007/3-540-50939-9_135</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-9QR95X94-W/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001398</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001398</idno><idno type="wicri:Area/Istex/Curation">001381</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">The reachability problem for ground TRS and some extensions</title><author><name sortKey="Deruyver, A" sort="Deruyver, A" uniqKey="Deruyver A" first="A." last="Deruyver">A. Deruyver</name><affiliation wicri:level="1"><mods:affiliation>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex</wicri:regionArea></affiliation></author><author><name sortKey="Gilleron, R" sort="Gilleron, R" uniqKey="Gilleron R" first="R." last="Gilleron">R. Gilleron</name><affiliation wicri:level="1"><mods:affiliation>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LIFL UA 369 CNRS Universite des sciences et techniques de LILLE FLANDRES ARTOIS U.F.R. d'I.E.E.A., Bat. M3, 59655, Villeneuve D'ascq Cedex</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The reachability problem for term rewriting systems (TRS) is the problem of deciding, for a given TRS S and two terms M and N, whether M can reduce to N by applying the rules of S. We show in this paper by some new methods based on algebraical tools of tree automata, the decidability of this problem for ground TRS's and, for every ground TRS S, we built a decision algorithm. In the order to obtain it, we compile the system S and the compiled algorithm works in a real time (as a fonction of the size of M and N). We establish too some new results for ground TRS modulo different sets of equations : modulo commutativity of an operator σ, the reachability problem is shown decidable with technics of finite tree automata; modulo associativity, the problem is undecidable; modulo commutativity and associativity, it is decidable with complexity of reachability problem for vector addition systems.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001381 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001381 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:5555FA46CA0AFEA78DEA1606327828BC26173885
|texte= The reachability problem for ground TRS and some extensions
}}
| This area was generated with Dilib version V0.6.33. |  |