{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:23Z","timestamp":1780994363701,"version":"3.54.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,11,26]],"date-time":"2012-11-26T00:00:00Z","timestamp":1353888000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["1035800"],"award-info":[{"award-number":["1035800"]}]},{"name":"National Science Foundation","award":["0931985"],"award-info":[{"award-number":["0931985"]}]},{"name":"National Science Foundation","award":["1054246"],"award-info":[{"award-number":["1054246"]}]},{"name":"National Science Foundation","award":["0926181"],"award-info":[{"award-number":["0926181"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We address a fundamental mismatch between the combinations of dynamics that\noccur in cyber-physical systems and the limited kinds of dynamics supported in\nanalysis. Modern applications combine communication, computation, and control.\nThey may even form dynamic distributed networks, where neither structure nor\ndimension stay the same while the system follows hybrid dynamics, i.e., mixed\ndiscrete and continuous dynamics. We provide the logical foundations for\nclosing this analytic gap. We develop a formal model for distributed hybrid\nsystems. It combines quantified differential equations with quantified\nassignments and dynamic dimensionality-changes. We introduce a dynamic logic\nfor verifying distributed hybrid systems and present a proof calculus for this\nlogic. This is the first formal verification approach for distributed hybrid\nsystems. We prove that our calculus is a sound and complete axiomatization of\nthe behavior of distributed hybrid systems relative to quantified differential\nequations. In our calculus we have proven collision freedom in distributed car\ncontrol even when an unbounded number of new cars may appear dynamically on the\nroad.<\/jats:p>","DOI":"10.2168\/lmcs-8(4:17)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:21:33Z","timestamp":1385731293000},"source":"Crossref","is-referenced-by-count":23,"title":["A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems"],"prefix":"10.46298","volume":"Volume 8, Issue 4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andre","family":"Platzer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2012,11,26]]},"reference":[{"key":"569:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/720\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/720\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:38Z","timestamp":1681242878000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/720"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,26]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(4:17)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1206.3357","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1206.3357","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"arxiv","id":"1408.1980","asserted-by":"subject"},{"id-type":"doi","id":"10.1145\/2817824","asserted-by":"subject"},{"id-type":"doi","id":"10.1184\/r1\/6604844","asserted-by":"subject"},{"id-type":"doi","id":"10.1184\/r1\/6604844.v1","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arxiv.1408.1980","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,26]]},"article-number":"720"}}