{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T07:00:56Z","timestamp":1762326056155,"version":"build-2065373602"},"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":[[2025,11]]},"abstract":"<jats:p>Model checking for disjunctive logic programs is a\n\nco-NP-complete task for which two main state-of-the-art\n\napproaches exist: one based on the unsatisfiability of SAT\n\nformulas derived from program reducts, and another based on\n\nunfounded sets.\n\nAlthough both are effective and efficient, their original\n\nformulations do not support recursive aggregates.\n\nThis paper extends previous work by tackling the stability\n\ncheck problem in the presence of such aggregates. We\n\ngeneralize the reduct-based approach to operate over\n\npseudo-Boolean theories rather than SAT encodings, yielding\n\nmore compact and efficient formulations. In parallel, we\n\nextend the unfounded-set-based approach to incorporate\n\naggregates, integrating both strategies as propagators\n\nwithin the ASP solver clingo. Additionally, we introduce\n\npartial stability checks to enable incremental or\n\napproximate verification of model stability. Our empirical\n\nevaluation demonstrates that these novel strategies not\n\nonly preserve correctness but also substantially improve\n\nthe efficiency of model checking for disjunctive programs\n\nwith aggregates.<\/jats:p>","DOI":"10.24963\/kr.2025\/57","type":"proceedings-article","created":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:10:44Z","timestamp":1762323044000},"page":"588-598","source":"Crossref","is-referenced-by-count":0,"title":["Model Checker for Recursive Aggregates"],"prefix":"10.24963","author":[{"given":"Mario","family":"Alviano","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, University"},{"name":"of Calabria"}]},{"given":"Carmine","family":"Dodaro","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, University"},{"name":"of Calabria"}]},{"given":"Salvatore","family":"Fiorentino","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, University"},{"name":"of Calabria"}]}],"member":"10584","event":{"name":"22nd International Conference on Principles of Knowledge Representation and Reasoning {KR-2025}","theme":"Artificial Intelligence","location":"Melbourne, Australia","acronym":"KR-2025","number":"22","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Academic College of Tel-Aviv","European Association for Artificial Intelligence","National Science Foundation"],"start":{"date-parts":[[2025,11,11]]},"end":{"date-parts":[[2025,11,17]]}},"container-title":["Proceedings of the TwentySecond International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:11:15Z","timestamp":1762323075000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2025\/57"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2025,11]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2025\/57","relation":{},"subject":[],"published":{"date-parts":[[2025,11]]}}}