---
_id: '4456'
abstract:
- lang: eng
  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.'
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
citation:
  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>'
  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>'
  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>.
  ieee: 'T. A. Henzinger, R. Jhala, and R. Majumdar, “Permissive interfaces,” presented
    at the FSE: Foundations of Software Engineering, 2005, pp. 31–40.'
  ista: 'Henzinger TA, Jhala R, Majumdar R. 2005. Permissive interfaces. FSE: Foundations
    of Software Engineering, 31–40.'
  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.
conference:
  name: 'FSE: Foundations of Software Engineering'
date_created: 2018-12-11T12:08:56Z
date_published: 2005-09-01T00:00:00Z
date_updated: 2021-01-12T07:57:06Z
day: '01'
doi: 10.1145/1081706.1081713
extern: 1
month: '09'
page: 31 - 40
publication_status: published
publisher: ACM
publist_id: '274'
quality_controlled: 0
status: public
title: Permissive interfaces
type: conference
year: '2005'
...
---
_id: '4457'
abstract:
- lang: eng
  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.
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Christoph
  full_name: Kirsch, Christoph M
  last_name: Kirsch
- first_name: Slobodan
  full_name: Matic, Slobodan
  last_name: Matic
citation:
  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>'
  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>'
  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>.
  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.'
  ista: 'Henzinger TA, Kirsch C, Matic S. 2005. Composable code generation for distributed
    Giotto. LCTES: Languages, Compilers, and Tools for Embedded Systems, 21–30.'
  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>.
  short: T.A. Henzinger, C. Kirsch, S. Matic, in:, ACM, 2005, pp. 21–30.
conference:
  name: 'LCTES: Languages, Compilers, and Tools for Embedded Systems'
date_created: 2018-12-11T12:08:57Z
date_published: 2005-06-01T00:00:00Z
date_updated: 2021-01-12T07:57:06Z
day: '01'
doi: 10.1145/1065910.1065914
extern: 1
month: '06'
page: 21 - 30
publication_status: published
publisher: ACM
publist_id: '275'
quality_controlled: 0
status: public
title: Composable code generation for distributed Giotto
type: conference
year: '2005'
...
---
_id: '4536'
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. '
acknowledgement: Supported in part by the AFOSR MURI grant F49620-00-1-0327 and the
  NSF grants CCR-0208875 and CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jean
  full_name: Raskin, Jean-François
  last_name: Raskin
citation:
  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>'
  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>'
  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.'
  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.'
  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>.'
  short: L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2005, pp. 144–161.
conference:
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2005-12-13T00:00:00Z
date_updated: 2021-01-12T07:59:31Z
day: '13'
doi: 'DOI: 10.1007/11603009_13'
extern: 1
intvolume: '      3829'
month: '12'
page: 144 - 161
publication_status: published
publisher: Springer
publist_id: '190'
quality_controlled: 0
status: public
title: Automatic rectangular refinement of affine hybrid systems
type: conference
volume: 3829
year: '2005'
...
---
_id: '4541'
abstract:
- lang: eng
  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.
    We 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.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  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>'
  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>'
  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.'
  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>.
  short: K. Chatterjee, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik, 2005, pp. 1–18.
conference:
  name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
date_created: 2018-12-11T12:09:23Z
date_published: 2005-12-07T00:00:00Z
date_updated: 2021-01-12T07:59:34Z
day: '07'
doi: 10.1007/11590156_1
extern: 1
intvolume: '      3821'
month: '12'
page: 1 - 18
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '182'
quality_controlled: 0
status: public
title: Semiperfect-information games
type: conference
volume: 3821
year: '2005'
...
---
_id: '4553'
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.'
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.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Luca
  full_name: de Alfaro, Luca
  last_name: De Alfaro
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  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>'
  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>'
  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.
conference:
  name: 'ICALP: Automata, Languages and Programming'
date_created: 2018-12-11T12:09:27Z
date_published: 2005-06-24T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '24'
doi: 10.1007/11523468_71
extern: 1
intvolume: '      3580'
month: '06'
page: 878 - 890
publication_status: published
publisher: Springer
publist_id: '158'
quality_controlled: 0
status: public
title: The complexity of stochastic Rabin and Streett games
type: conference
volume: 3580
year: '2005'
...
---
_id: '4554'
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.
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Thomas Henzinger
  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
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>'
  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>'
  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>.
  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.'
  ista: 'Chatterjee K, Henzinger TA, Jurdziński M. 2005. Mean-payoff parity games.
    LICS: Logic in Computer Science, 178–187.'
  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>.
  short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, in:, IEEE, 2005, pp. 178–187.
conference:
  name: 'LICS: Logic in Computer Science'
date_created: 2018-12-11T12:09:27Z
date_published: 2005-09-19T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '19'
doi: 10.1109/LICS.2005.26
extern: 1
month: '09'
page: 178 - 187
publication_status: published
publisher: IEEE
publist_id: '159'
quality_controlled: 0
status: public
title: Mean-payoff parity games
type: conference
year: '2005'
...
---
_id: '4557'
abstract:
- lang: eng
  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.'
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
citation:
  ama: 'Chatterjee K, Henzinger TA, Jhala R, Majumdar R. Counterexample-guided planning.
    In: AUAI Press; 2005: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.'
  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.'
  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.
  short: K. Chatterjee, T.A. Henzinger, R. Jhala, R. Majumdar, in:, AUAI Press, 2005,
    pp. 104–111.
conference:
  name: 'UAI: Uncertainty in Artificial Intelligence'
date_created: 2018-12-11T12:09:28Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:41Z
day: '01'
extern: 1
main_file_link:
- open_access: '0'
  url: http://uai.sis.pitt.edu/papers/05/p104-chatterjee.pdf
month: '01'
page: 104 - 111
publication_status: published
publisher: AUAI Press
publist_id: '157'
quality_controlled: 0
status: public
title: Counterexample-guided planning
type: conference
year: '2005'
...