{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:25Z","timestamp":1776316885795,"version":"3.50.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,4,26]],"date-time":"2016-04-26T00:00:00Z","timestamp":1461628800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A data tree is an unranked ordered tree where each node carries a label from\na finite alphabet and a datum from some infinite domain. We consider the two\nvariable first order logic FO2(&lt;,+1,~) over data trees. Here +1 refers to the\nchild and the next sibling relations while &lt; refers to the descendant and\nfollowing sibling relations. Moreover, ~ is a binary predicate testing data\nequality. We exhibit an automata model, denoted DAD# that is more expressive\nthan FO2(&lt;,+1,~) but such that emptiness of DAD# and satisfiability of\nFO2(&lt;,+1,~) are inter-reducible. This is proved via a model of counter tree\nautomata, denoted EBVASS, that extends Branching Vector Addition Systems with\nStates (BVASS) with extra features for merging counters. We show that, as\ndecision problems, reachability for EBVASS, satisfiability of FO2(&lt;,+1,~) and\nemptiness of DAD# are equivalent.<\/jats:p>","DOI":"10.2168\/lmcs-12(2:3)2016","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T13:47:33Z","timestamp":1479736053000},"source":"Crossref","is-referenced-by-count":5,"title":["FO2(&lt;,+1,~) on data trees, data tree automata and branching vector addition systems"],"prefix":"10.46298","volume":"Volume 12, Issue 2","author":[{"given":"Florent","family":"Jacquemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luc","family":"Segoufin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jer\u00e9mie","family":"Dimino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2016,4,26]]},"reference":[{"key":"1122:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1635\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1635\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:08:39Z","timestamp":1681243719000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1635"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,26]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-12(2:3)2016","relation":{"is-same-as":[{"id-type":"arxiv","id":"1601.01579","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1601.01579","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,26]]},"article-number":"1635"}}