{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T23:15:34Z","timestamp":1789082134595,"version":"build-2803163510"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,7]]},"abstract":"<jats:p>Automated logic circuit design enhances chip performance, energy efficiency, and reliability, with applications in model-checking, reactive synthesis, and hyperproperty verification. AIGER circuits are a standard format for these domains, used in hardware model-checking, synthesis competitions such as Syntcomp, symbolic synthesis algorithms, and the verification of security properties in neural networks and safety-critical systems.\n\nTraditionally, AIGER circuits are generated from Linear Temporal Logic (LTL) specifications through complex pipelines, such as translating LTL to SMV or to automata and then to AIGER. These pipelines guarantee functional equivalence but produce large circuits with auto-generated labels that obscure the specification\u2019s meaning. In applications like symbolic reactive synthesis, model-checking, and neural network verification, understanding latches and outputs is critical for debugging and tool improvement.\n\nIn this tool paper, we introduce AIGLE, a novel tool that generates compact AIGER circuits directly from LTL[X] or Past-LTL specifications. Our approach uses linear-size translation from LTL[X] to Past-LTL, which produces highly legible circuits. Compared to tools like py-aiger, our tool reduces gate counts-\u2014often by thousands-\u2014 improving readability and synthesis speed. Our empirical evaluation demonstrates smaller, more understandable circuits and faster synthesis, offering a scalable, engineer-friendly solution for formal methods applications.<\/jats:p>","DOI":"10.24963\/kr.2026\/67","type":"proceedings-article","created":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:15:53Z","timestamp":1784200553000},"page":"711-722","source":"Crossref","is-referenced-by-count":1,"title":["AIGLE: A Tool for Compact, Legible AIGER Circuits from Safety Specifications"],"prefix":"10.24963","author":[{"given":"Mat\u00edas","family":"Brizzio","sequence":"first","affiliation":[{"name":"IMDEA Software Institute"},{"name":"Universidad Polit\u00e9cnica de Madrid"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andoni","family":"Rodr\u00edguez","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"},{"name":"Universidad Polit\u00e9cnica de Madrid"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Renzo","family":"Degiovanni","sequence":"additional","affiliation":[{"name":"Luxembourg Institute of Science and Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"10584","event":{"name":"23nd International Conference on Principles of Knowledge Representation and Reasoning {KR-2026}","theme":"Artificial Intelligence","location":"Lisbon, Portuagal","acronym":"KR-2026","number":"23","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","European Association for Artificial Intelligence"],"start":{"date-parts":[[2026,7,20]]},"end":{"date-parts":[[2026,7,18]]}},"container-title":["Proceedings of the TwentyThird International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:16:12Z","timestamp":1784200572000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2026\/67"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2026\/67","relation":{},"subject":[],"published":{"date-parts":[[2026,7]]}}}