{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T03:43:45Z","timestamp":1777434225612,"version":"3.51.4"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,9,5]],"date-time":"2015-09-05T00:00:00Z","timestamp":1441411200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Ripartizione Diritto allo Studio, Universit\u00e0 e Ricerca Scientifica of Provincia Autonoma di Bolzano-Alto Adige","award":["VeryiSyncopated"],"award-info":[{"award-number":["VeryiSyncopated"]}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["FP7-318338"],"award-info":[{"award-number":["FP7-318338"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Universit\u00e0 La Sapienza di Roma","award":["Spiritlets"],"award-info":[{"award-number":["Spiritlets"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2016,8]]},"DOI":"10.1007\/s11225-015-9626-z","type":"journal-article","created":{"date-parts":[[2015,9,5]],"date-time":"2015-09-05T14:27:26Z","timestamp":1441463246000},"page":"705-739","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Progression and Verification of Situation Calculus Agents with Bounded Beliefs"],"prefix":"10.1007","volume":"104","author":[{"given":"Giuseppe","family":"De Giacomo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yves","family":"Lesp\u00e9rance","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Patrizi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Vassos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,5]]},"reference":[{"key":"9626_CR1","doi-asserted-by":"crossref","unstructured":"Bagheri Hariri, B., D. Calvanese, G. De Giacomo, R. De Masellis, and P. Felli, Foundations of relational artifacts verification, in Proceedings of BPM, 2011.","DOI":"10.1007\/978-3-642-23059-2_28"},{"key":"9626_CR2","doi-asserted-by":"crossref","unstructured":"Bagheri Hariri, B., D. Calvanese, G. De Giacomo, A. Deutsch, and M. Montali, Verification of relational data-centric dynamic systems with external services, in Proceedings of PODS, 2013.","DOI":"10.1145\/2463664.2465221"},{"key":"9626_CR3","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier C., Katoen J.-P., Guldstrand Larsen K.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9626_CR4","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1613\/jair.4424","volume":"51","author":"F. Belardinelli","year":"2014","unstructured":"Belardinelli F., Lomuscio A., Patrizi F.: Verification of agent-based artifact systems. Journal of Artificial Intelligence Research 51, 333\u2013376 (2014)","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"3\u20134","key":"9626_CR5","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/j.artint.2009.11.001","volume":"174","author":"B. Bonet","year":"2010","unstructured":"Bonet B.: Conformant plans and beyond: Principles and complexity. Artificial Intelligence Research 174(3\u20134), 245\u2013269 (2010)","journal-title":"Artificial Intelligence Research"},{"key":"9626_CR6","doi-asserted-by":"crossref","unstructured":"Bordini, R. H., M. Fisher, C. Pardavila, and M. Wooldridge, Model checking agentspeak, in Proceedings of AAMAS, 2003.","DOI":"10.1145\/860575.860641"},{"key":"9626_CR7","doi-asserted-by":"crossref","unstructured":"Burkart, O., D. Caucal, F. Moller, and B. Steffen, Verification of infinite structures, in Handbook of Process Algebra, Elsevier Science, Amsterdam, 2001.","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"9626_CR8","unstructured":"Classen, J., and G. Lakemeyer, A logic for non-terminating Golog programs, in Proceedings of KR, 2008."},{"key":"9626_CR9","doi-asserted-by":"crossref","unstructured":"Classen, J., M. Liebenberg, G. Lakemeyer, and B. Zarriess, Exploring the boundaries of decidable verification of non-terminating Golog programs, in Proceedings of AAAI, 2014.","DOI":"10.1609\/aaai.v28i1.8875"},{"key":"9626_CR10","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Y. Lesp\u00e9rance, H. J. Levesque, and S. Sardina, IndiGolog: A high-level programming language for embedded reasoning agents, in Multi-Agent Programming: Languages, Tools and Applications, Springer, Berlin, 2009.","DOI":"10.1007\/978-0-387-89299-3_2"},{"key":"9626_CR11","unstructured":"De Giacomo, G., Y. Lesp\u00e9rance, and F. Patrizi, Bounded situation calculus action theories and decidable verification, in Proceedings of KR, 2012."},{"key":"9626_CR12","unstructured":"De Giacomo, G., Y. Lesp\u00e9rance, and F. Patrizi, Bounded epistemic situation calculus theories, in Proceedings of IJCAI, 2013."},{"key":"9626_CR13","unstructured":"De Giacomo, G., Y. Lesp\u00e9rance, F. Patrizi, and S. Vassos, LTL verification of online executions with sensing in bounded situation calculus, in Proceedings of ECAI, 2014."},{"key":"9626_CR14","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Y. Lesp\u00e9rance, F. Patrizi, and S. Vassos, Progression and verification of situation calculus agents with bounded beliefs, in Proceedings of AAMAS, 2014.","DOI":"10.1007\/s11225-015-9626-z"},{"key":"9626_CR15","unstructured":"De Giacomo, G., Y. Lesp\u00e9rance, and A. R. Pearce, Situation calculus based programs for representing and reasoning about game structures, in Proceedings of KR, 2010."},{"key":"9626_CR16","doi-asserted-by":"crossref","unstructured":"De Giacomo G., and H. J. Levesque, An incremental interpreter for high-level programs with sensing, in Logical Foundations for Cognitive Agents: Contributions in Honor of Ray Reiter, Springer, Berlin, 1999.","DOI":"10.1007\/978-3-642-60211-5_8"},{"key":"9626_CR17","unstructured":"De Giacomo, G., and H. J. Levesque, Projection using regression and sensors, in Proceedings of IJCAI, 1999."},{"issue":"1","key":"9626_CR18","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"L. A. Dennis","year":"2012","unstructured":"Dennis L. A., Fisher M., Webster M. P., Bordini R. H.: Model checking agent programming languages. Automated Software Engineering 19(1), 5\u201363 (2012)","journal-title":"Automated Software Engineering"},{"key":"9626_CR19","doi-asserted-by":"crossref","unstructured":"Deutsch, A., R. Hull, F. Patrizi, and V. Vianu, Automatic verification of data-centric business processes, in Proceedings of ICDT, 2009.","DOI":"10.1145\/1514894.1514924"},{"key":"9626_CR20","doi-asserted-by":"crossref","unstructured":"Dumas, M., W. M. P. van der Aalst, and A. H. M. ter Hofstede, Process-Aware Information Systems: Bridging People and Software Through Process Technology. Wiley, Hoboken, 2005.","DOI":"10.1002\/0471741442"},{"key":"9626_CR21","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., Model checking and the Mu-calculus, in Descriptive Complexity and Finite Models. Proceedings of a DIMACS Workshop, 1996.","DOI":"10.1090\/dimacs\/031\/06"},{"key":"9626_CR22","doi-asserted-by":"crossref","unstructured":"Gerede, C. E., and J. Su, Specification and verification of artifact behaviors in business process models, in Proceedings of ICSOC, 2007.","DOI":"10.1007\/978-3-540-74974-5_15"},{"key":"9626_CR23","unstructured":"Gu, Y., and M. Soutchanski, Decidable reasoning in a modified situation calculus, in Proceedings of IJCAI 2007."},{"key":"9626_CR24","doi-asserted-by":"crossref","unstructured":"Hull, R., Artifact-centric business process models: Brief survey of research results and challenges, in Proceedings of OTM 2008 Confederated International Conferences, 2008.","DOI":"10.1007\/978-3-540-88873-4_17"},{"key":"9626_CR25","unstructured":"Lakemeyer, G., and H. J. Levesque, Situations, si! situation terms, no!, in Proceedings of KR, 2004."},{"key":"9626_CR26","unstructured":"Lakemeyer, G., and H. J. Levesque, Semantics for a useful fragment of the situation calculus, in Proceedings of IJCAI, 2005."},{"key":"9626_CR27","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S0743-1066(96)00121-5","volume":"31","author":"H. J. Levesque","year":"1997","unstructured":"Levesque H. J., Reiter R., Lesp\u00e9rance Y., Lin F., Scherl R. B.: GOLOG: A Logic Programming Language for Dynamic Domains. Journal of Logic Programming 31, 59\u201384 (1997)","journal-title":"Journal of Logic Programming"},{"key":"9626_CR28","doi-asserted-by":"crossref","unstructured":"Libkin, L., Embedded finite models and constraint databases, in Finite Model Theory and Its Applications, Springer, Heidelberg, 2007.","DOI":"10.1007\/3-540-68804-8_5"},{"issue":"1\u20132","key":"9626_CR29","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/S0004-3702(96)00044-6","volume":"92","author":"F. Lin","year":"1997","unstructured":"Lin F., Reiter R.: How to progress a database. Artificial Intelligence 92(1\u20132), 131\u2013167 (1997)","journal-title":"Artificial Intelligence"},{"key":"9626_CR30","unstructured":"Liu, Y., and G. Lakemeyer, On first-order definability and computability of progression for local-effect actions and beyond, in Proceedings of IJCAI, 2009."},{"key":"9626_CR31","unstructured":"Liu, Y., and H. J. Levesque, Tractable reasoning with incomplete first-order knowledge in dynamic systems with context-dependent actions, in Proceedings of IJCAI, 2005."},{"key":"9626_CR32","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., H. Qu, and F. Raimondi, MCMAS: A model checker for the verification of multi-agent systems, in Proceedings of CAV, 2009.","DOI":"10.1007\/978-3-642-02658-4_55"},{"key":"9626_CR33","first-page":"463","volume":"4","author":"J. McCarthy","year":"1969","unstructured":"McCarthy J., Hayes P. J.: Some philosophical problems from the standpoint of artificial intelligence. Machine Intelligence 4, 463\u2013502 (1969)","journal-title":"Machine Intelligence"},{"key":"9626_CR34","unstructured":"Moore, R. C., A formal theory of knowledge and action, in J. R. Hobbs and R. C. Moore (eds.), Formal Theories of the Common Sense World, Ablex Publishing, Norwood, NJ, 1985, pp. 319\u2013358."},{"issue":"3","key":"9626_CR35","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1145\/316542.316545","volume":"46","author":"F. Pirri","year":"1999","unstructured":"Pirri F., Reiter R.: Some contributions to the metatheory of the situation calculus. Journal of ACM 46(3), 261\u2013325 (1999)","journal-title":"Journal of ACM"},{"key":"9626_CR36","doi-asserted-by":"crossref","unstructured":"Reiter, R., Knowledge in Action. Logical Foundations for Specifying and Implementing Dynamical Systems, MIT Press, Cambridge, 2001.","DOI":"10.7551\/mitpress\/4074.001.0001"},{"key":"9626_CR37","unstructured":"Sardina, S., and G. De Giacomo, Composition of ConGolog programs, in Proceedings of IJCAI, 2009."},{"key":"9626_CR38","doi-asserted-by":"crossref","unstructured":"Sardina, S., G. De Giacomo, Y. Lesp\u00e9rance, and H. J. Levesque, On the semantics of deliberation in IndiGolog\u2014from theory to implementation. Annals of Mathematics and Artificial Intelligence 41(2\u20134):259\u2013299, 2004.","DOI":"10.1023\/B:AMAI.0000031197.13122.aa"},{"key":"9626_CR39","unstructured":"Sardina, S., G. D. Giacomo, Y. Lesp\u00e9rance, and H. J. Levesque, On ability to autonomously execute agent programs with sensing, in Proceedings of AAMAS, 2004."},{"key":"9626_CR40","unstructured":"Sardina, S., G. D. Giacomo, Y. Lesp\u00e9rance, and H. J. Levesque, On the limits of planning over belief states under strict uncertainty, in Proceedings of KR, 2006."},{"key":"9626_CR41","unstructured":"Scherl, R. B., and H. J. Levesque, The frame problem and knowledge-producing actions, in Proceedings of AAAI, 1993."},{"issue":"1\u20132","key":"9626_CR42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0004-3702(02)00365-X","volume":"144","author":"R. B. Scherl","year":"2003","unstructured":"Scherl R. B., Levesque H. J.: Knowledge, action, and the frame problem. Artificial Intelligence 144(1\u20132), 1\u201339 (2003)","journal-title":"Artificial Intelligence"},{"key":"9626_CR43","doi-asserted-by":"crossref","unstructured":"Shapiro, S., Y. Lesp\u00e9rance, and H. J. Levesque, The cognitive agents specification language and verification environment for multiagent systems, in Proceedings of AAMAS, 2002.","DOI":"10.1145\/544741.544746"},{"key":"9626_CR44","doi-asserted-by":"crossref","unstructured":"Shapiro, S., Y. Lesp\u00e9rance, and H. J. Levesque, The cognitive agent specification language and verification environment, in M. Dastani, K. Hindriks, and J.-J. C. Meyer (eds.), Specification and Verification of Multi-agent Systems\/Programs, Springer, Berlin, 2010, pp. 289\u2013316.","DOI":"10.1007\/978-1-4419-6984-2_10"},{"key":"9626_CR45","doi-asserted-by":"crossref","unstructured":"Stirling, C., Modal and Temporal Properties of Processes, Springer, Heidelberg, 2001.","DOI":"10.1007\/978-1-4757-3550-5"},{"key":"9626_CR46","unstructured":"Ternovskaia, E., Automata theory for reasoning about actions, In Proceedings of IJCAI, 1999."},{"key":"9626_CR47","doi-asserted-by":"crossref","unstructured":"van Riemsdijk, M., L. Atefnoaei, and F. de Boer, Using the Maude term rewriting language for agent development with formal foundations, in M. Dastani, K. V. Hindriks, and J.-J. C. Meyer (eds.), Specification and Verification of Multi-agent Systems. Springer, Berlin, 2010, pp. 255\u2013287.","DOI":"10.1007\/978-1-4419-6984-2_9"},{"key":"9626_CR48","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y., An automata-theoretic approach to linear temporal logic, in Proceedings of Banff Higher Order Workshop, 1995.","DOI":"10.1007\/3-540-60915-6_6"},{"key":"9626_CR49","unstructured":"Vassos, S., G. Lakemeyer, and H. J. Levesque, First-order strong progression for local-effect basic action theories, in Proceedings of KR, 2008."},{"key":"9626_CR50","doi-asserted-by":"crossref","unstructured":"Vassos, S., and H. J. Levesque, How to progress a database III, Artificial Intelligence 195:203\u2013221, 2013.","DOI":"10.1016\/j.artint.2012.10.005"},{"key":"9626_CR51","unstructured":"Vassos, S., and F. Patrizi, A classification of first-order progressable action theories in situation calculus, in In Proceedings of IJCAI, 2013."},{"key":"9626_CR52","doi-asserted-by":"crossref","unstructured":"Wooldridge, M., Lomuscio A.:A computationally grounded logic of visibility, perception, and knowledge. Logic Journal of the IGPL 9(2):257\u2013272 (2001)","DOI":"10.1093\/jigpal\/9.2.257"},{"key":"9626_CR53","doi-asserted-by":"crossref","unstructured":"Yadav, N., and S. Sardina, Reasoning about BDI agent programs using ATL-like logics, in Proceedings of JELIA, 2012.","DOI":"10.1007\/978-3-642-33353-8_34"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9626-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-015-9626-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9626-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,13]],"date-time":"2023-08-13T20:19:48Z","timestamp":1691957988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-015-9626-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,5]]},"references-count":53,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,8]]}},"alternative-id":["9626"],"URL":"https:\/\/doi.org\/10.1007\/s11225-015-9626-z","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,5]]}}}