[{"month":"09","oa":1,"date_published":"2024-09-01T00:00:00Z","das_tickbox":"0","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2405.04015"}],"title":"Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties","_id":"18159","supplementarymaterial":"no","publisher":"International Joint Conferences on Artificial Intelligence","oa_version":"Preprint","publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"date_created":"2024-09-29T22:01:38Z","doi":"10.24963/ijcai.2024/1","article_processing_charge":"No","publication_status":"published","external_id":{"arxiv":["2405.04015"]},"author":[{"first_name":"S","full_name":"Akshay, S","last_name":"Akshay"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","first_name":"Tobias","full_name":"Meggendorfer, Tobias"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699"}],"abstract":[{"lang":"eng","text":"Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defned with respect to paths over MDP states. An increasingly\r\npopular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defned in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verifcation techniques. In this work, we consider the problems of certifed policy (i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance specifcations. By certifed we mean that, along with a policy, we also aim to synthesize a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certifcate for a given policy or synthesize a policy along with a certifcate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certifcates and present automated procedures for (1) synthesizing a certifcate for a given policy, and (2) synthesizing a policy together with the certifcate, both providing formal guarantees on certifcate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certifed policies and to certify existing policies. "}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","corr_author":"1","language":[{"iso":"eng"}],"publication":"Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence","citation":{"short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In: <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2024:3-12. doi:<a href=\"https://doi.org/10.24963/ijcai.2024/1\">10.24963/ijcai.2024/1</a>","chicago":"Akshay, S, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” In <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, 3–12. International Joint Conferences on Artificial Intelligence, 2024. <a href=\"https://doi.org/10.24963/ijcai.2024/1\">https://doi.org/10.24963/ijcai.2024/1</a>.","ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties,” in <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, Jeju, Korea, 2024, pp. 3–12.","ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 3–12.","mla":"Akshay, S., et al. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12, doi:<a href=\"https://doi.org/10.24963/ijcai.2024/1\">10.24963/ijcai.2024/1</a>.","apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., &#38; Zikelic, D. (2024). Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i> (pp. 3–12). Jeju, Korea: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2024/1\">https://doi.org/10.24963/ijcai.2024/1</a>"},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"page":"3-12","ec_funded":1,"type":"conference","status":"public","scopus_import":"1","date_updated":"2026-10-16T08:08:15Z","day":"01","fulldoi":"https://doi.org/10.24963/ijcai.2024/1","quality_controlled":"1","conference":{"end_date":"2024-08-09","location":"Jeju, Korea","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2024-08-03"},"researchdata_availability":"no","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt), the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant, Google Research Award 2023 and the SBI Foundation Hub for Data and Analytics.","year":"2024","department":[{"_id":"KrCh"}],"arxiv":1},{"arxiv":1,"year":"2024","department":[{"_id":"KrCh"}],"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Czech Science Foundation\r\ngrant no. GA23-06963S.","quality_controlled":"1","researchdata_availability":"no","conference":{"start_date":"2024-08-03","name":"IJCAI: International Joint Conference on Artificial Intelligence","end_date":"2024-08-09","location":"Jeju, South Korea"},"OA_type":"green","day":"01","date_updated":"2026-10-16T08:07:05Z","fulldoi":"https://doi.org/10.24963/ijcai.2024/741","scopus_import":"1","type":"conference","status":"public","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"page":"6707-6715","ec_funded":1,"publication":"33rd International Joint Conference on Artificial Intelligence","citation":{"apa":"Chatterjee, K., Goharshady, E., Karrabi, M., Novotný, P., &#38; Zikelic, D. (2024). Solving long-run average reward robust MDPs via stochastic games. In <i>33rd International Joint Conference on Artificial Intelligence</i> (pp. 6707–6715). Jeju, South Korea: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>","mla":"Chatterjee, Krishnendu, et al. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” <i>33rd International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–15, doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>.","short":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, D. Zikelic, in:, 33rd International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–6715.","ama":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. Solving long-run average reward robust MDPs via stochastic games. In: <i>33rd International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2024:6707-6715. doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic, “Solving long-run average reward robust MDPs via stochastic games,” in <i>33rd International Joint Conference on Artificial Intelligence</i>, Jeju, South Korea, 2024, pp. 6707–6715.","ista":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving long-run average reward robust MDPs via stochastic games. 33rd International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 6707–6715.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Petr Novotný, and Dorde Zikelic. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” In <i>33rd International Joint Conference on Artificial Intelligence</i>, 6707–15. International Joint Conferences on Artificial Intelligence, 2024. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>."},"corr_author":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"external_id":{"arxiv":["2312.13912"]},"abstract":[{"text":"Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in NP∩CONP and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration. ","lang":"eng"}],"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","first_name":"Ehsan","last_name":"Kafshdar Goharshadi"},{"last_name":"Karrabi","first_name":"Mehrdad","full_name":"Karrabi, Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757","orcid":"0009-0007-5253-9170"},{"last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","full_name":"Novotný, Petr"},{"last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde"}],"oa_version":"Preprint","publication_identifier":{"isbn":["9781956792041"],"issn":["1045-0823"]},"publication_status":"published","date_created":"2024-09-29T22:01:39Z","article_processing_charge":"No","doi":"10.24963/ijcai.2024/741","_id":"18160","supplementarymaterial":"no","publisher":"International Joint Conferences on Artificial Intelligence","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.13912"}],"title":"Solving long-run average reward robust MDPs via stochastic games","month":"09","oa":1,"date_published":"2024-09-01T00:00:00Z","OA_place":"repository","das_tickbox":"0"},{"conference":{"name":"IJCAI: International Joint Conferences on Artificial Intelligence","start_date":"2021-08-19","end_date":"2021-08-27","location":"Virtual, Online"},"quality_controlled":"1","acknowledgement":"This research was supported by the Czech Science Foundation (no. 19-24384Y), by the OP VVV MEYS funded project CZ.02.1.01/0.0/0.0/16 019/0000765 “Research Center for Informatics”, by the ERC CoG 863818 (ForM-SMArt), and by the Combat Capabilities Development Command Army Research Laboratory and was accomplished under Cooperative\r\nAgreement Number W911NF-13-2-0045 (ARL Cyber Security CRA). The views and conclusions contained in this document are those of the authors and should not be interpreted as\r\nrepresenting the official policies, either expressed or implied, of the Combat Capabilities Development Command Army Research Laboratory or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes not withstanding any copyright notation here on. ","department":[{"_id":"KrCh"}],"year":"2021","page":"4182-4189","ec_funded":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"status":"public","type":"conference","ddc":["000"],"scopus_import":"1","fulldoi":"https://doi.org/10.24963/ijcai.2021/575","day":"01","date_updated":"2026-06-18T10:41:02Z","publication_status":"published","article_processing_charge":"No","date_created":"2022-03-13T23:01:47Z","doi":"10.24963/ijcai.2021/575","oa_version":"Published Version","publication_identifier":{"issn":["1045-0823"],"isbn":["9780999241196"]},"author":[{"full_name":"Tomášek, Petr","first_name":"Petr","last_name":"Tomášek"},{"last_name":"Horák","full_name":"Horák, Karel","first_name":"Karel"},{"first_name":"Aditya","full_name":"Aradhye, Aditya","last_name":"Aradhye"},{"first_name":"Branislav","full_name":"Bošanský, Branislav","last_name":"Bošanský"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"}],"abstract":[{"text":"We study the two-player zero-sum extension of the partially observable stochastic shortest-path problem where one agent has only partial information about the environment. We formulate this problem as a partially observable stochastic game (POSG): given a set of target states and negative rewards for each transition, the player with imperfect information maximizes the expected undiscounted total reward until a target state is reached. The second player with the perfect information aims for the opposite. We base our formalism on POSGs with one-sided observability (OS-POSGs) and give the following contributions: (1) we introduce a novel heuristic search value iteration algorithm that iteratively solves depth-limited variants of the game, (2) we derive the bound on the depth guaranteeing an arbitrary precision, (3) we propose a novel upper-bound estimation that allows early terminations, and (4) we experimentally evaluate the algorithm on a pursuit-evasion game.","lang":"eng"}],"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"P. Tomášek, K. Horák, A. Aradhye, B. Bošanský, and K. Chatterjee, “Solving partially observable stochastic shortest-path games,” in <i>30th International Joint Conference on Artificial Intelligence</i>, Virtual, Online, 2021, pp. 4182–4189.","chicago":"Tomášek, Petr, Karel Horák, Aditya Aradhye, Branislav Bošanský, and Krishnendu Chatterjee. “Solving Partially Observable Stochastic Shortest-Path Games.” In <i>30th International Joint Conference on Artificial Intelligence</i>, 4182–89. International Joint Conferences on Artificial Intelligence, 2021. <a href=\"https://doi.org/10.24963/ijcai.2021/575\">https://doi.org/10.24963/ijcai.2021/575</a>.","ista":"Tomášek P, Horák K, Aradhye A, Bošanský B, Chatterjee K. 2021. Solving partially observable stochastic shortest-path games. 30th International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conferences on Artificial Intelligence, 4182–4189.","ama":"Tomášek P, Horák K, Aradhye A, Bošanský B, Chatterjee K. Solving partially observable stochastic shortest-path games. In: <i>30th International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2021:4182-4189. doi:<a href=\"https://doi.org/10.24963/ijcai.2021/575\">10.24963/ijcai.2021/575</a>","short":"P. Tomášek, K. Horák, A. Aradhye, B. Bošanský, K. Chatterjee, in:, 30th International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2021, pp. 4182–4189.","mla":"Tomášek, Petr, et al. “Solving Partially Observable Stochastic Shortest-Path Games.” <i>30th International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2021, pp. 4182–89, doi:<a href=\"https://doi.org/10.24963/ijcai.2021/575\">10.24963/ijcai.2021/575</a>.","apa":"Tomášek, P., Horák, K., Aradhye, A., Bošanský, B., &#38; Chatterjee, K. (2021). Solving partially observable stochastic shortest-path games. In <i>30th International Joint Conference on Artificial Intelligence</i> (pp. 4182–4189). Virtual, Online: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2021/575\">https://doi.org/10.24963/ijcai.2021/575</a>"},"publication":"30th International Joint Conference on Artificial Intelligence","date_published":"2021-09-01T00:00:00Z","oa":1,"month":"09","title":"Solving partially observable stochastic shortest-path games","main_file_link":[{"open_access":"1","url":"https://doi.org/10.24963/ijcai.2021/575"}],"publisher":"International Joint Conferences on Artificial Intelligence","_id":"10847"},{"quality_controlled":"1","conference":{"start_date":"2018-07-13","name":"IJCAI: International Joint Conference on Artificial Intelligence","location":"Stockholm, Sweden","end_date":"2018-07-19"},"year":"2018","department":[{"_id":"KrCh"}],"arxiv":1,"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"page":"4700-4707","type":"conference","status":"public","scopus_import":"1","day":"17","date_updated":"2026-10-16T22:30:59Z","fulldoi":"https://doi.org/10.24963/ijcai.2018/653","oa_version":"Preprint","publication_identifier":{"isbn":["9780999241127"],"issn":["1045-0823"]},"date_created":"2019-02-13T13:26:27Z","article_processing_charge":"No","publication_status":"published","doi":"10.24963/ijcai.2018/653","external_id":{"arxiv":["1804.08984"],"isi":["000764175404118"]},"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"first_name":"Amir","full_name":"Goharshady, Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","last_name":"Goharshady"},{"last_name":"Okati","full_name":"Okati, Nastaran","first_name":"Nastaran"}],"abstract":[{"text":"We consider the stochastic shortest path (SSP)problem for succinct Markov decision processes(MDPs), where the MDP consists of a set of vari-ables, and a set of nondeterministic rules that up-date the variables. First, we show that several ex-amples from the AI literature can be modeled assuccinct MDPs.  Then we present computationalapproaches for upper and lower bounds for theSSP problem: (a) for computing upper bounds, ourmethod is polynomial-time in the implicit descrip-tion of the MDP; (b) for lower bounds, we present apolynomial-time (in the size of the implicit descrip-tion) reduction to quadratic programming. Our ap-proach is applicable even to infinite-state MDPs.Finally, we present experimental results to demon-strate the effectiveness of our approach on severalclassical examples from the AI literature.","lang":"eng"}],"isi":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","citation":{"mla":"Chatterjee, Krishnendu, et al. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, vol. 2018, IJCAI, 2018, pp. 4700–07, doi:<a href=\"https://doi.org/10.24963/ijcai.2018/653\">10.24963/ijcai.2018/653</a>.","apa":"Chatterjee, K., Fu, H., Goharshady, A. K., &#38; Okati, N. (2018). Computational approaches for stochastic shortest path on succinct MDPs. In <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i> (Vol. 2018, pp. 4700–4707). Stockholm, Sweden: IJCAI. <a href=\"https://doi.org/10.24963/ijcai.2018/653\">https://doi.org/10.24963/ijcai.2018/653</a>","ista":"Chatterjee K, Fu H, Goharshady AK, Okati N. 2018. Computational approaches for stochastic shortest path on succinct MDPs. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4700–4707.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran Okati. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” In <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, 2018:4700–4707. IJCAI, 2018. <a href=\"https://doi.org/10.24963/ijcai.2018/653\">https://doi.org/10.24963/ijcai.2018/653</a>.","ieee":"K. Chatterjee, H. Fu, A. K. Goharshady, and N. Okati, “Computational approaches for stochastic shortest path on succinct MDPs,” in <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, Stockholm, Sweden, 2018, vol. 2018, pp. 4700–4707.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, N. Okati, in:, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4700–4707.","ama":"Chatterjee K, Fu H, Goharshady AK, Okati N. Computational approaches for stochastic shortest path on succinct MDPs. In: <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>. Vol 2018. IJCAI; 2018:4700-4707. doi:<a href=\"https://doi.org/10.24963/ijcai.2018/653\">10.24963/ijcai.2018/653</a>"},"intvolume":"      2018","month":"07","volume":2018,"oa":1,"date_published":"2018-07-17T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1804.08984","open_access":"1"}],"title":"Computational approaches for stochastic shortest path on succinct MDPs","_id":"5977","publisher":"IJCAI"},{"publist_id":"6395","department":[{"_id":"ToHe"}],"pubrep_id":"818","file":[{"file_name":"IST-2017-818-v1+1_allIJCAI_CR.pdf","relation":"main_file","content_type":"application/pdf","creator":"system","date_updated":"2018-12-12T10:16:58Z","file_size":365172,"access_level":"open_access","date_created":"2018-12-12T10:16:58Z","file_id":"5249"}],"year":"2017","conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence ","start_date":"2017-08-19","location":"Melbourne, Australia","end_date":"2017-08-25"},"quality_controlled":"1","fulldoi":"https://doi.org/10.24963/ijcai.2017/11","date_updated":"2025-07-10T11:49:38Z","day":"30","ddc":["004"],"scopus_import":"1","has_accepted_license":"1","status":"public","type":"conference","page":"70 - 76","project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"citation":{"apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2017). An abstraction-refinement methodology for reasoning about network games (pp. 70–76). Presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia: AAAI Press. <a href=\"https://doi.org/10.24963/ijcai.2017/11\">https://doi.org/10.24963/ijcai.2017/11</a>","mla":"Avni, Guy, et al. <i>An Abstraction-Refinement Methodology for Reasoning about Network Games</i>. AAAI Press, 2017, pp. 70–76, doi:<a href=\"https://doi.org/10.24963/ijcai.2017/11\">10.24963/ijcai.2017/11</a>.","ista":"Avni G, Guha S, Kupferman O. 2017. An abstraction-refinement methodology for reasoning about network games. IJCAI: International Joint Conference on Artificial Intelligence , 70–76.","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia, 2017, pp. 70–76.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games,” 70–76. AAAI Press, 2017. <a href=\"https://doi.org/10.24963/ijcai.2017/11\">https://doi.org/10.24963/ijcai.2017/11</a>.","ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. In: AAAI Press; 2017:70-76. doi:<a href=\"https://doi.org/10.24963/ijcai.2017/11\">10.24963/ijcai.2017/11</a>","short":"G. Avni, S. Guha, O. Kupferman, in:, AAAI Press, 2017, pp. 70–76."},"related_material":{"record":[{"relation":"later_version","status":"public","id":"6006"}]},"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","isi":1,"file_date_updated":"2018-12-12T10:16:58Z","abstract":[{"lang":"eng","text":"Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology."}],"author":[{"last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","full_name":"Avni, Guy"},{"first_name":"Shibashis","full_name":"Guha, Shibashis","last_name":"Guha"},{"first_name":"Orna","full_name":"Kupferman, Orna","last_name":"Kupferman"}],"external_id":{"isi":["000764137500011"]},"doi":"10.24963/ijcai.2017/11","publication_status":"published","date_created":"2018-12-11T11:49:38Z","article_processing_charge":"No","oa_version":"Submitted Version","publication_identifier":{"issn":["1045-0823"]},"publisher":"AAAI Press","_id":"1003","title":"An abstraction-refinement methodology for reasoning about network games","date_published":"2017-05-30T00:00:00Z","oa":1,"month":"05"},{"citation":{"short":"M. Henzinger, R. Motwani, C. Silverstein, in:, 18th International Joint Conference on Artificial Intelligence, Association for Computing Machinery, 2003, pp. 1573–1579.","ama":"Henzinger M, Motwani R, Silverstein C. Challenges in web search engines. In: <i>18th International Joint Conference on Artificial Intelligence</i>. Association for Computing Machinery; 2003:1573-1579.","ista":"Henzinger M, Motwani R, Silverstein C. 2003. Challenges in web search engines. 18th International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 1573–1579.","chicago":"Henzinger, Monika, Rajeev Motwani, and Craig Silverstein. “Challenges in Web Search Engines.” In <i>18th International Joint Conference on Artificial Intelligence</i>, 1573–79. Association for Computing Machinery, 2003.","ieee":"M. Henzinger, R. Motwani, and C. Silverstein, “Challenges in web search engines,” in <i>18th International Joint Conference on Artificial Intelligence</i>, Acapulco, Mexico, 2003, pp. 1573–1579.","mla":"Henzinger, Monika, et al. “Challenges in Web Search Engines.” <i>18th International Joint Conference on Artificial Intelligence</i>, Association for Computing Machinery, 2003, pp. 1573–79.","apa":"Henzinger, M., Motwani, R., &#38; Silverstein, C. (2003). Challenges in web search engines. In <i>18th International Joint Conference on Artificial Intelligence</i> (pp. 1573–1579). Acapulco, Mexico: Association for Computing Machinery."},"publication":"18th International Joint Conference on Artificial Intelligence","extern":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2003","language":[{"iso":"eng"}],"author":[{"last_name":"Henzinger","full_name":"Henzinger, Monika H","first_name":"Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Motwani","first_name":"Rajeev","full_name":"Motwani, Rajeev"},{"last_name":"Silverstein","first_name":"Craig","full_name":"Silverstein, Craig"}],"abstract":[{"text":"This article presents a high-level discussion of some problems that are unique to web search engines. The goal is to raise awareness and stimulate research in these areas.","lang":"eng"}],"oa_version":"Published Version","conference":{"end_date":"2003-08-15","location":"Acapulco, Mexico","start_date":"2003-08-09","name":"IJCAI: International Joint Conference on Artificial Intelligence"},"publication_identifier":{"issn":["1045-0823"]},"quality_controlled":"1","date_created":"2022-08-18T06:40:02Z","publication_status":"published","article_processing_charge":"No","date_updated":"2024-11-06T08:13:06Z","_id":"11909","day":"01","publisher":"Association for Computing Machinery","scopus_import":"1","main_file_link":[{"url":"https://www.ijcai.org/Proceedings/03/Papers/278.pdf","open_access":"1"}],"title":"Challenges in web search engines","type":"conference","status":"public","month":"08","date_published":"2003-08-01T00:00:00Z","page":"1573-1579","oa":1}]