{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:40Z","timestamp":1760202700879,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,8,4]],"date-time":"2016-08-04T00:00:00Z","timestamp":1470268800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["233599"],"award-info":[{"award-number":["233599"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We study linear-time temporal logics interpreted over data words with\nmultiple attributes. We restrict the atomic formulas to equalities of attribute\nvalues in successive positions and to repetitions of attribute values in the\nfuture or past. We demonstrate correspondences between satisfiability problems\nfor logics and reachability-like decision problems for counter systems. We show\nthat allowing\/disallowing atomic formulas expressing repetitions of values in\nthe past corresponds to the reachability\/coverability problem in Petri nets.\nThis gives us 2EXPSPACE upper bounds for several satisfiability problems. We\nprove matching lower bounds by reduction from a reachability problem for a\nnewly introduced class of counter systems. This new class is a succinct version\nof vector addition systems with states in which counters are accessed via\npointers, a potentially useful feature in other contexts. We strengthen further\nthe correspondences between data logics and counter systems by characterizing\nthe complexity of fragments, extensions and variants of the logic. For\ninstance, we precisely characterize the relationship between the number of\nattributes allowed in the logic and the number of counters needed in the\ncounter system.<\/jats:p>","DOI":"10.2168\/lmcs-12(3:1)2016","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T14:12:04Z","timestamp":1479737524000},"source":"Crossref","is-referenced-by-count":9,"title":["Reasoning about Data Repetitions with Counter Systems"],"prefix":"10.46298","volume":"Volume 12, Issue 3","author":[{"given":"Stephane","family":"Demri","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0114-2257","authenticated-orcid":false,"given":"Diego","family":"Figueira","sequence":"additional","affiliation":[]},{"given":"M","family":"Praveen","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2016,8,4]]},"reference":[{"key":"1144:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1645\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1645\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:08:53Z","timestamp":1681243733000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1645"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,4]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-12(3:1)2016","relation":{"is-same-as":[{"id-type":"arxiv","id":"1604.02887","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1604.02887","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2016,8,4]]},"article-number":"1645"}}