{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:39:32Z","timestamp":1753889972600,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,9,17]],"date-time":"2015-09-17T00:00:00Z","timestamp":1442448000000},"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":["288175"],"award-info":[{"award-number":["288175"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["257414"],"award-info":[{"award-number":["257414"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We propose a method for compositional verification to address the state space\nexplosion problem inherent to model-checking timed systems with a large number\nof components. The main challenge is to obtain pertinent global timing\nconstraints from the timings in the components alone. To this end, we make use\nof auxiliary clocks to automatically generate new invariants which capture the\nconstraints induced by the synchronisations between components. The method has\nbeen implemented in the RTD-Finder tool and successfully experimented on\nseveral benchmarks.<\/jats:p>","DOI":"10.2168\/lmcs-11(3:15)2015","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T13:46:02Z","timestamp":1479735962000},"source":"Crossref","is-referenced-by-count":4,"title":["Compositional Verification for Timed Systems Based on Automatic Invariant Generation"],"prefix":"10.46298","volume":"Volume 11, Issue 3","author":[{"given":"Lacramioara","family":"Astefanoaei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Souha Ben","family":"Rayana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Combaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2015,9,17]]},"reference":[{"key":"1084:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1591\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1591\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:07:23Z","timestamp":1681243643000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1591"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,17]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(3:15)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1506.04879","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1506.04879","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2015,9,17]]},"article-number":"1591"}}