[{"abstract":[{"text":"A modular program analysis considers components independently and provides a succinct summary for each component, which is used when checking the rest of the system. Consider a system consisting of a library and a client. A temporal summary, or interface, of the library specifies legal sequences of library calls. The interface is safe if no call sequence violates the library's internal invariants; the interface is permissive if it contains every such sequence. Modular program analysis requires full interfaces, which are both safe and permissive: the client does not cause errors in the library if and only if it makes only sequences of library calls that are allowed by the full interface of the library.Previous interface-based methods have focused on safe interfaces, which may be too restrictive and thus reject good clients. We present an algorithm for automatically synthesizing software interfaces that are both safe and permissive. The algorithm generates interfaces as graphs whose vertices are labeled with predicates over the library's internal state, and whose edges are labeled with library calls. The interface state is refined incrementally until the full interface is constructed. In other words, the algorithm automatically synthesizes a typestate system for the library, against which any client can be checked for compatibility. We present an implementation of the algorithm which is based on the BLAST model checker, and we evaluate some case studies.","lang":"eng"}],"day":"01","page":"31 - 40","date_published":"2005-09-01T00:00:00Z","publication_status":"published","_id":"4456","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","first_name":"Thomas A"},{"last_name":"Jhala","first_name":"Ranjit","full_name":"Jhala, Ranjit"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar S","last_name":"Majumdar"}],"type":"conference","status":"public","year":"2005","date_updated":"2021-01-12T07:57:06Z","publisher":"ACM","doi":"10.1145/1081706.1081713","title":"Permissive interfaces","publist_id":"274","quality_controlled":0,"month":"09","conference":{"name":"FSE: Foundations of Software Engineering"},"extern":1,"citation":{"ieee":"T. A. Henzinger, R. Jhala, and R. Majumdar, “Permissive interfaces,” presented at the FSE: Foundations of Software Engineering, 2005, pp. 31–40.","chicago":"Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Permissive Interfaces,” 31–40. ACM, 2005. <a href=\"https://doi.org/10.1145/1081706.1081713\">https://doi.org/10.1145/1081706.1081713</a>.","ama":"Henzinger TA, Jhala R, Majumdar R. Permissive interfaces. In: ACM; 2005:31-40. doi:<a href=\"https://doi.org/10.1145/1081706.1081713\">10.1145/1081706.1081713</a>","ista":"Henzinger TA, Jhala R, Majumdar R. 2005. Permissive interfaces. FSE: Foundations of Software Engineering, 31–40.","apa":"Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2005). Permissive interfaces (pp. 31–40). Presented at the FSE: Foundations of Software Engineering, ACM. <a href=\"https://doi.org/10.1145/1081706.1081713\">https://doi.org/10.1145/1081706.1081713</a>","mla":"Henzinger, Thomas A., et al. <i>Permissive Interfaces</i>. ACM, 2005, pp. 31–40, doi:<a href=\"https://doi.org/10.1145/1081706.1081713\">10.1145/1081706.1081713</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2005, pp. 31–40."},"date_created":"2018-12-11T12:08:56Z"},{"type":"conference","status":"public","publisher":"ACM","date_updated":"2021-01-12T07:57:06Z","year":"2005","doi":"10.1145/1065910.1065914","abstract":[{"text":"We present a compositional approach to the implementation of hard real-time software running on a distributed platform. We explain how several code suppliers, coordinated by a system integrator, can independently generate different parts of the distributed software. The task structure, interaction, and timing is specified as a Giotto program. Each supplier is given a part of the Giotto program and a timing interface, from which the supplier generates task and scheduling code. The integrator then checks, individually for each supplier, in pseudo-polynomial time, if the supplied code meets its timing specification. If all checks succeed, then the supplied software parts are guaranteed to work together and implement the original Giotto program. The feasibility of the approach is demonstrated by a prototype implementation.","lang":"eng"}],"date_published":"2005-06-01T00:00:00Z","page":"21 - 30","publication_status":"published","day":"01","_id":"4457","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","first_name":"Thomas A"},{"first_name":"Christoph","full_name":"Kirsch, Christoph M","last_name":"Kirsch"},{"first_name":"Slobodan","full_name":"Matic, Slobodan","last_name":"Matic"}],"extern":1,"conference":{"name":"LCTES: Languages, Compilers, and Tools for Embedded Systems"},"citation":{"ieee":"T. A. Henzinger, C. Kirsch, and S. Matic, “Composable code generation for distributed Giotto,” presented at the LCTES: Languages, Compilers, and Tools for Embedded Systems, 2005, pp. 21–30.","chicago":"Henzinger, Thomas A, Christoph Kirsch, and Slobodan Matic. “Composable Code Generation for Distributed Giotto,” 21–30. ACM, 2005. <a href=\"https://doi.org/10.1145/1065910.1065914\">https://doi.org/10.1145/1065910.1065914</a>.","ama":"Henzinger TA, Kirsch C, Matic S. Composable code generation for distributed Giotto. In: ACM; 2005:21-30. doi:<a href=\"https://doi.org/10.1145/1065910.1065914\">10.1145/1065910.1065914</a>","mla":"Henzinger, Thomas A., et al. <i>Composable Code Generation for Distributed Giotto</i>. ACM, 2005, pp. 21–30, doi:<a href=\"https://doi.org/10.1145/1065910.1065914\">10.1145/1065910.1065914</a>.","ista":"Henzinger TA, Kirsch C, Matic S. 2005. Composable code generation for distributed Giotto. LCTES: Languages, Compilers, and Tools for Embedded Systems, 21–30.","short":"T.A. Henzinger, C. Kirsch, S. Matic, in:, ACM, 2005, pp. 21–30.","apa":"Henzinger, T. A., Kirsch, C., &#38; Matic, S. (2005). Composable code generation for distributed Giotto (pp. 21–30). Presented at the LCTES: Languages, Compilers, and Tools for Embedded Systems, ACM. <a href=\"https://doi.org/10.1145/1065910.1065914\">https://doi.org/10.1145/1065910.1065914</a>"},"date_created":"2018-12-11T12:08:57Z","title":"Composable code generation for distributed Giotto","quality_controlled":0,"publist_id":"275","month":"06"},{"type":"conference","status":"public","year":"2005","publisher":"Springer","date_updated":"2021-01-12T07:59:31Z","doi":"DOI: 10.1007/11603009_13","abstract":[{"lang":"eng","text":"We show how to automatically construct and refine rectangular abstractions of systems of linear differential equations. From a hybrid automaton whose dynamics are given by a system of linear differential equations, our method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton. We prove an optimality criterion for successive refinements. We also show that this method can take into account a safety property to be verified, refining only relevant parts of the state space. The practicability of the method is illustrated on a benchmark case study. "}],"day":"13","page":"144 - 161","date_published":"2005-12-13T00:00:00Z","publication_status":"published","_id":"4536","author":[{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A"},{"last_name":"Raskin","full_name":"Raskin, Jean-François","first_name":"Jean"}],"intvolume":"      3829","alternative_title":["LNCS"],"conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"extern":1,"acknowledgement":"Supported in part by the AFOSR MURI grant F49620-00-1-0327 and the NSF grants CCR-0208875 and CCR-0225610.","citation":{"chicago":"Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Automatic Rectangular Refinement of Affine Hybrid Systems,” 3829:144–61. Springer, 2005. <a href=\"https://doi.org/DOI: 10.1007/11603009_13\">https://doi.org/DOI: 10.1007/11603009_13</a>.","ieee":"L. Doyen, T. A. Henzinger, and J. Raskin, “Automatic rectangular refinement of affine hybrid systems,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2005, vol. 3829, pp. 144–161.","mla":"Doyen, Laurent, et al. <i>Automatic Rectangular Refinement of Affine Hybrid Systems</i>. Vol. 3829, Springer, 2005, pp. 144–61, doi:<a href=\"https://doi.org/DOI: 10.1007/11603009_13\">DOI: 10.1007/11603009_13</a>.","apa":"Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2005). Automatic rectangular refinement of affine hybrid systems (Vol. 3829, pp. 144–161). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. <a href=\"https://doi.org/DOI: 10.1007/11603009_13\">https://doi.org/DOI: 10.1007/11603009_13</a>","ista":"Doyen L, Henzinger TA, Raskin J. 2005. Automatic rectangular refinement of affine hybrid systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 3829, 144–161.","short":"L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2005, pp. 144–161.","ama":"Doyen L, Henzinger TA, Raskin J. Automatic rectangular refinement of affine hybrid systems. In: Vol 3829. Springer; 2005:144-161. doi:<a href=\"https://doi.org/DOI: 10.1007/11603009_13\">DOI: 10.1007/11603009_13</a>"},"date_created":"2018-12-11T12:09:22Z","title":"Automatic rectangular refinement of affine hybrid systems","volume":3829,"publist_id":"190","quality_controlled":0,"month":"12"},{"day":"07","page":"1 - 18","date_published":"2005-12-07T00:00:00Z","publication_status":"published","abstract":[{"text":"Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete.\nWe study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives.\n","lang":"eng"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Krishnendu Chatterjee"},{"first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"_id":"4541","status":"public","type":"conference","doi":"10.1007/11590156_1","year":"2005","date_updated":"2021-01-12T07:59:34Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","title":"Semiperfect-information games","volume":3821,"month":"12","publist_id":"182","quality_controlled":0,"conference":{"name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science"},"extern":1,"intvolume":"      3821","alternative_title":["LNCS"],"date_created":"2018-12-11T12:09:23Z","citation":{"chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Semiperfect-Information Games,” 3821:1–18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2005. <a href=\"https://doi.org/10.1007/11590156_1\">https://doi.org/10.1007/11590156_1</a>.","ieee":"K. Chatterjee and T. A. Henzinger, “Semiperfect-information games,” presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, 2005, vol. 3821, pp. 1–18.","short":"K. Chatterjee, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2005, pp. 1–18.","ista":"Chatterjee K, Henzinger TA. 2005. Semiperfect-information games. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LNCS, vol. 3821, 1–18.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Semiperfect-Information Games</i>. Vol. 3821, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2005, pp. 1–18, doi:<a href=\"https://doi.org/10.1007/11590156_1\">10.1007/11590156_1</a>.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2005). Semiperfect-information games (Vol. 3821, pp. 1–18). Presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/11590156_1\">https://doi.org/10.1007/11590156_1</a>","ama":"Chatterjee K, Henzinger TA. Semiperfect-information games. In: Vol 3821. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2005:1-18. doi:<a href=\"https://doi.org/10.1007/11590156_1\">10.1007/11590156_1</a>"}},{"publist_id":"158","quality_controlled":0,"month":"06","title":"The complexity of stochastic Rabin and Streett games","volume":3580,"citation":{"chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “The Complexity of Stochastic Rabin and Streett Games,” 3580:878–90. Springer, 2005. <a href=\"https://doi.org/10.1007/11523468_71\">https://doi.org/10.1007/11523468_71</a>.","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “The complexity of stochastic Rabin and Streett games,” presented at the ICALP: Automata, Languages and Programming, 2005, vol. 3580, pp. 878–890.","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2005. The complexity of stochastic Rabin and Streett games. ICALP: Automata, Languages and Programming, LNCS, vol. 3580, 878–890.","mla":"Chatterjee, Krishnendu, et al. <i>The Complexity of Stochastic Rabin and Streett Games</i>. Vol. 3580, Springer, 2005, pp. 878–90, doi:<a href=\"https://doi.org/10.1007/11523468_71\">10.1007/11523468_71</a>.","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, Springer, 2005, pp. 878–890.","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2005). The complexity of stochastic Rabin and Streett games (Vol. 3580, pp. 878–890). Presented at the ICALP: Automata, Languages and Programming, Springer. <a href=\"https://doi.org/10.1007/11523468_71\">https://doi.org/10.1007/11523468_71</a>","ama":"Chatterjee K, De Alfaro L, Henzinger TA. The complexity of stochastic Rabin and Streett games. In: Vol 3580. Springer; 2005:878-890. doi:<a href=\"https://doi.org/10.1007/11523468_71\">10.1007/11523468_71</a>"},"acknowledgement":"This research was supported in part by the ONR grant N00014-02-1-0671, the AFOSR MURI grant F49620-00-1-0327, and the NSF grant CCR-0225610.","date_created":"2018-12-11T12:09:27Z","intvolume":"      3580","alternative_title":["LNCS"],"conference":{"name":"ICALP: Automata, Languages and Programming"},"extern":1,"_id":"4553","author":[{"first_name":"Krishnendu","full_name":"Krishnendu Chatterjee","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"de Alfaro, Luca"},{"full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"lang":"eng","text":"The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We show that for Rabin winning conditions, both problems are in NP. As these problems were known to be NP-hard, it follows that they are NP-complete for Rabin conditions, and dually, coNP-complete for Streett conditions. The proof proceeds by showing that pure memoryless strategies suffice for qualitatively and quantitatively winning stochastic graph games with Rabin conditions. This insight is of interest in its own right, as it implies that controllers for Rabin objectives have simple implementations. We also prove that for every ω-regular condition, optimal winning strategies are no more complex than almost-sure winning strategies."}],"day":"24","publication_status":"published","page":"878 - 890","date_published":"2005-06-24T00:00:00Z","year":"2005","date_updated":"2021-01-12T07:59:39Z","publisher":"Springer","doi":"10.1007/11523468_71","type":"conference","status":"public"},{"abstract":[{"lang":"eng","text":"Games played on graphs may have qualitative objectives, such as the satisfaction of an ω-regular property, or quantitative objectives, such as the optimization of a real-valued reward. When games are used to model reactive systems with both fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding objective combines both a qualitative and a quantitative component. In a general case of interest, the qualitative component is a parity condition and the quantitative component is a mean-payoff reward. We study and solve such mean-payoff parity games. We also prove some interesting facts about mean-payoff parity games which distinguish them both from mean-payoff and from parity games. In particular, we show that optimal strategies exist in mean-payoff parity games, but they may require infinite memory."}],"page":"178 - 187","date_published":"2005-09-19T00:00:00Z","publication_status":"published","day":"19","_id":"4554","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Krishnendu Chatterjee"},{"full_name":"Thomas Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"first_name":"Marcin","full_name":"Jurdziński, Marcin","last_name":"Jurdziński"}],"type":"conference","status":"public","date_updated":"2021-01-12T07:59:39Z","publisher":"IEEE","year":"2005","doi":"10.1109/LICS.2005.26","title":"Mean-payoff parity games","quality_controlled":0,"publist_id":"159","month":"09","extern":1,"conference":{"name":"LICS: Logic in Computer Science"},"citation":{"ama":"Chatterjee K, Henzinger TA, Jurdziński M. Mean-payoff parity games. In: IEEE; 2005:178-187. doi:<a href=\"https://doi.org/10.1109/LICS.2005.26\">10.1109/LICS.2005.26</a>","mla":"Chatterjee, Krishnendu, et al. <i>Mean-Payoff Parity Games</i>. IEEE, 2005, pp. 178–87, doi:<a href=\"https://doi.org/10.1109/LICS.2005.26\">10.1109/LICS.2005.26</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Jurdziński, M. (2005). Mean-payoff parity games (pp. 178–187). Presented at the LICS: Logic in Computer Science, IEEE. <a href=\"https://doi.org/10.1109/LICS.2005.26\">https://doi.org/10.1109/LICS.2005.26</a>","ista":"Chatterjee K, Henzinger TA, Jurdziński M. 2005. Mean-payoff parity games. LICS: Logic in Computer Science, 178–187.","short":"K. Chatterjee, T.A. Henzinger, M. Jurdziński, in:, IEEE, 2005, pp. 178–187.","ieee":"K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Mean-payoff parity games,” presented at the LICS: Logic in Computer Science, 2005, pp. 178–187.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Mean-Payoff Parity Games,” 178–87. IEEE, 2005. <a href=\"https://doi.org/10.1109/LICS.2005.26\">https://doi.org/10.1109/LICS.2005.26</a>."},"date_created":"2018-12-11T12:09:27Z"},{"month":"01","publist_id":"157","main_file_link":[{"url":"http://uai.sis.pitt.edu/papers/05/p104-chatterjee.pdf","open_access":"0"}],"quality_controlled":0,"title":"Counterexample-guided planning","date_created":"2018-12-11T12:09:28Z","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Counterexample-Guided Planning,” 104–11. AUAI Press, 2005.","ieee":"K. Chatterjee, T. A. Henzinger, R. Jhala, and R. Majumdar, “Counterexample-guided planning,” presented at the UAI: Uncertainty in Artificial Intelligence, 2005, pp. 104–111.","apa":"Chatterjee, K., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2005). Counterexample-guided planning (pp. 104–111). Presented at the UAI: Uncertainty in Artificial Intelligence, AUAI Press.","short":"K. Chatterjee, T.A. Henzinger, R. Jhala, R. Majumdar, in:, AUAI Press, 2005, pp. 104–111.","ista":"Chatterjee K, Henzinger TA, Jhala R, Majumdar R. 2005. Counterexample-guided planning. UAI: Uncertainty in Artificial Intelligence, 104–111.","mla":"Chatterjee, Krishnendu, et al. <i>Counterexample-Guided Planning</i>. AUAI Press, 2005, pp. 104–11.","ama":"Chatterjee K, Henzinger TA, Jhala R, Majumdar R. Counterexample-guided planning. In: AUAI Press; 2005:104-111."},"conference":{"name":"UAI: Uncertainty in Artificial Intelligence"},"extern":1,"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Krishnendu Chatterjee"},{"full_name":"Thomas Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar S"}],"_id":"4557","day":"01","page":"104 - 111","publication_status":"published","date_published":"2005-01-01T00:00:00Z","abstract":[{"text":"Planning in adversarial and uncertain environments can be modeled as the problem of devising strategies in stochastic perfect information games. These games are generalizations of Markov decision processes (MDPs): there are two (adversarial) players, and a source of randomness. The main practical obstacle to computing winning strategies in such games is the size of the state space. In practice therefore, one typically works with abstractions of the model. The diffculty is to come up with an abstraction that is neither too coarse to remove all winning strategies (plans), nor too fine to be intractable. In verification, the paradigm of counterexample-guided abstraction refinement has been successful to construct useful but parsimonious abstractions automatically. We extend this paradigm to probabilistic models (namely, perfect information games and, as a special case, MDPs). This allows us to apply the counterexample-guided abstraction paradigm to the AI planning problem. As special cases, we get planning algorithms for MDPs and deterministic systems that automatically construct system abstractions.","lang":"eng"}],"year":"2005","publisher":"AUAI Press","date_updated":"2021-01-12T07:59:41Z","status":"public","type":"conference"}]