---
_id: '4477'
abstract:
- lang: eng
  text: The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for
    decomposing a verification task about a system into subtasks about the individual
    components of the system. The key to assume-guarantee reasoning is to consider
    each component not in isolation, but in conjunction with assumptions about the
    context of the component. Assume-guarantee principles are known for purely concurrent
    contexts, which constrain the input data of a component, as well as for purely
    sequential contexts, which constrain the entry configurations of a component.
    We present a model for hierarchical system design which permits the arbitrary
    nesting of parallel as well as serial composition, and which supports an assume-guarantee
    principle for mixed parallel-serial contexts. Our model also supports both discrete
    and continuous processes, and is therefore well-suited for the modeling and analysis
    of embedded software systems which interact with real-world environments. Using
    an example of two cooperating robots, we show refinement between a high-level
    model which specifies continuous timing constraints and an implementation which
    relies on discrete sampling.
acknowledgement: Support for this research was provided in part by the AFOSR MURI
  grant F49620- 00-1-0327, and the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC
  grant 98-DT-660, the NSF ITR grant CCR-0085949.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Marius
  full_name: Minea, Marius
  last_name: Minea
- first_name: Vinayak
  full_name: Prabhu, Vinayak
  last_name: Prabhu
citation:
  ama: 'Henzinger TA, Minea M, Prabhu V. Assume-guarantee reasoning for hierarchical
    hybrid systems. In: <i>Proceedings of the 4th International Workshop on Hybrid
    Systems</i>. Vol 2034. Springer; 2001:275-290. doi:<a href="https://doi.org/10.1007/3-540-45351-2_24">10.1007/3-540-45351-2_24</a>'
  apa: 'Henzinger, T. A., Minea, M., &#38; Prabhu, V. (2001). Assume-guarantee reasoning
    for hierarchical hybrid systems. In <i>Proceedings of the 4th International Workshop
    on Hybrid Systems</i> (Vol. 2034, pp. 275–290). Rome, Italy: Springer. <a href="https://doi.org/10.1007/3-540-45351-2_24">https://doi.org/10.1007/3-540-45351-2_24</a>'
  chicago: Henzinger, Thomas A, Marius Minea, and Vinayak Prabhu. “Assume-Guarantee
    Reasoning for Hierarchical Hybrid Systems.” In <i>Proceedings of the 4th International
    Workshop on Hybrid Systems</i>, 2034:275–90. Springer, 2001. <a href="https://doi.org/10.1007/3-540-45351-2_24">https://doi.org/10.1007/3-540-45351-2_24</a>.
  ieee: T. A. Henzinger, M. Minea, and V. Prabhu, “Assume-guarantee reasoning for
    hierarchical hybrid systems,” in <i>Proceedings of the 4th International Workshop
    on Hybrid Systems</i>, Rome, Italy, 2001, vol. 2034, pp. 275–290.
  ista: 'Henzinger TA, Minea M, Prabhu V. 2001. Assume-guarantee reasoning for hierarchical
    hybrid systems. Proceedings of the 4th International Workshop on Hybrid Systems.
    HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 2034, 275–290.'
  mla: Henzinger, Thomas A., et al. “Assume-Guarantee Reasoning for Hierarchical Hybrid
    Systems.” <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>,
    vol. 2034, Springer, 2001, pp. 275–90, doi:<a href="https://doi.org/10.1007/3-540-45351-2_24">10.1007/3-540-45351-2_24</a>.
  short: T.A. Henzinger, M. Minea, V. Prabhu, in:, Proceedings of the 4th International
    Workshop on Hybrid Systems, Springer, 2001, pp. 275–290.
conference:
  end_date: 2001-03-30
  location: Rome, Italy
  name: 'HSCC: Hybrid Systems - Computation and Control'
  start_date: 2001-03-28
date_created: 2018-12-11T12:09:03Z
date_published: 2001-03-14T00:00:00Z
date_updated: 2023-05-09T14:47:37Z
day: '14'
doi: 10.1007/3-540-45351-2_24
extern: '1'
intvolume: '      2034'
language:
- iso: eng
month: '03'
oa_version: None
page: 275 - 290
publication: Proceedings of the 4th International Workshop on Hybrid Systems
publication_identifier:
  isbn:
  - '9783540418665'
publication_status: published
publisher: Springer
publist_id: '250'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Assume-guarantee reasoning for hierarchical hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2034
year: '2001'
...