Tree Automata with Equality Constraints Modulo Equational Theories
Identifieur interne : 005355 ( Main/Exploration ); précédent : 005354; suivant : 005356Tree Automata with Equality Constraints Modulo Equational Theories
Auteurs : Florent Jacquemard [France] ; Michael Rusinowitch [France] ; Laurent Vigneron [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.
Url:
DOI: 10.1007/11814771_45
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001900
- to stream Istex, to step Curation: 001881
- to stream Istex, to step Checkpoint: 001208
- to stream Hal, to step Corpus: 004F72
- to stream Hal, to step Curation: 004F72
- to stream Hal, to step Checkpoint: 003F65
- to stream Main, to step Merge: 005501
- to stream Main, to step Curation: 005355
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Tree Automata with Equality Constraints Modulo Equational Theories</title><author><name sortKey="Jacquemard, Florent" sort="Jacquemard, Florent" uniqKey="Jacquemard F" first="Florent" last="Jacquemard">Florent Jacquemard</name></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name></author><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:6B5D7A874A050E8BCB345D15C19CDBF128CDD14F</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/11814771_45</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-S63RQ5TQ-K/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001900</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001900</idno><idno type="wicri:Area/Istex/Curation">001881</idno><idno type="wicri:Area/Istex/Checkpoint">001208</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001208</idno><idno type="wicri:doubleKey">0302-9743:2006:Jacquemard F:tree:automata:with</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00579011</idno><idno type="url">https://hal.inria.fr/inria-00579011</idno><idno type="wicri:Area/Hal/Corpus">004F72</idno><idno type="wicri:Area/Hal/Curation">004F72</idno><idno type="wicri:Area/Hal/Checkpoint">003F65</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003F65</idno><idno type="wicri:Area/Main/Merge">005501</idno><idno type="wicri:Area/Main/Curation">005355</idno><idno type="wicri:Area/Main/Exploration">005355</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Tree Automata with Equality Constraints Modulo Equational Theories</title><author><name sortKey="Jacquemard, Florent" sort="Jacquemard, Florent" uniqKey="Jacquemard F" first="Florent" last="Jacquemard">Florent Jacquemard</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</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: This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Jacquemard, Florent" sort="Jacquemard, Florent" uniqKey="Jacquemard F" first="Florent" last="Jacquemard">Florent Jacquemard</name></noRegion><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005355 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005355 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:6B5D7A874A050E8BCB345D15C19CDBF128CDD14F
|texte= Tree Automata with Equality Constraints Modulo Equational Theories
}}
| This area was generated with Dilib version V0.6.33. |  |