{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:37Z","timestamp":1759638937595,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2013,12,17]],"date-time":"2013-12-17T00:00:00Z","timestamp":1387238400000},"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>We consider formal verification of recursive programs with resource\nconsumption. We introduce prefix replacement systems with non-negative integer\ncounters which can be incremented and reset to zero as a formal model for such\nprograms. In these systems, we investigate bounds on the resource consumption\nfor reachability questions. Motivated by this question, we introduce relational\nstructures with resources and a quantitative first-order logic over these\nstructures. We define resource automatic structures as a subclass of these\nstructures and provide an effective method to compute the semantics of the\nlogic on this subclass. Subsequently, we use this framework to solve the\nbounded reachability problem for resource prefix replacement systems. We\nachieve this result by extending the well-known saturation method to annotated\nprefix replacement systems. Finally, we provide a connection to the study of\nthe logic cost-WMSO.<\/jats:p>","DOI":"10.2168\/lmcs-9(4:22)2013","type":"journal-article","created":{"date-parts":[[2014,7,15]],"date-time":"2014-07-15T09:37:51Z","timestamp":1405417071000},"source":"Crossref","is-referenced-by-count":1,"title":["Modeling and Verification of Infinite Systems with Resources"],"prefix":"10.46298","volume":"Volume 9, Issue 4","author":[{"given":"Martin","family":"Lang","sequence":"first","affiliation":[]},{"given":"Christof","family":"L\u00f6ding","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2013,12,17]]},"reference":[{"key":"782:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1162\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1162\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:05:13Z","timestamp":1681243513000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1162"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,17]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-9(4:22)2013","relation":{"is-same-as":[{"id-type":"arxiv","id":"1311.1043","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1311.1043","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"arxiv","id":"1405.5593","asserted-by":"subject"},{"id-type":"doi","id":"10.4204\/eptcs.151.1","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arxiv.1405.5593","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2013,12,17]]},"article-number":"1162"}}