---
_id: '4486'
abstract:
- lang: eng
  text: 'The simulation preorder on state transition systems is widely accepted as
    a useful notion of refinement, both in its own right and as an efficiently checkable
    sufficient condition for trace containment. For composite systems, due to the
    exponential explosion of the state space, there is a need for decomposing a simulation
    check of the form P< s Q into simpler simulation checks on the components of
    P and Q. We present an assume-guarantee rule that enables such a decomposition.
    To the best of our knowledge, this is the first assume-guarantee rule that applies
    to a refinement relation different from trace containment. Our rule is circular,
    and its soundness proof requires induction on trace trees. The proof is constructive:
    given simulation relations that witness the simulation preorder between corresponding
    components of P and Q, we provide a procedure for constructing a witness relation
    for P< s Q. We also extend our assume-guarantee rule to account for fairness
    assumptions on transition systems'
acknowledgement: This research was supported in part by the Office of Naval Research
  Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER
  award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the
  Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research
  Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation
  contract 97-DC-324.041.
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: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
- first_name: Serdar
  full_name: Tasiran, Serdar
  last_name: Tasiran
citation:
  ama: 'Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for
    checking simulation. In: <i>Proceedings of the 2nd International Conference on
    Formal Methods in Computer-Aided Design</i>. Vol 1522. Springer; 1998:421-432.
    doi:<a href="https://doi.org/10.1007/3-540-49519-3_27">10.1007/3-540-49519-3_27</a>'
  apa: 'Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (1998). An assume-guarantee
    rule for checking simulation. In <i>Proceedings of the 2nd International Conference
    on Formal Methods in Computer-Aided Design</i> (Vol. 1522, pp. 421–432). Palo
    Alto, CA, United States of America: Springer. <a href="https://doi.org/10.1007/3-540-49519-3_27">https://doi.org/10.1007/3-540-49519-3_27</a>'
  chicago: Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran.
    “An Assume-Guarantee Rule for Checking Simulation.” In <i>Proceedings of the 2nd
    International Conference on Formal Methods in Computer-Aided Design</i>, 1522:421–32.
    Springer, 1998. <a href="https://doi.org/10.1007/3-540-49519-3_27">https://doi.org/10.1007/3-540-49519-3_27</a>.
  ieee: T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee
    rule for checking simulation,” in <i>Proceedings of the 2nd International Conference
    on Formal Methods in Computer-Aided Design</i>, Palo Alto, CA, United States of
    America, 1998, vol. 1522, pp. 421–432.
  ista: 'Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 1998. An assume-guarantee
    rule for checking simulation. Proceedings of the 2nd International Conference
    on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided
    Design, LNCS, vol. 1522, 421–432.'
  mla: Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.”
    <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided
    Design</i>, vol. 1522, Springer, 1998, pp. 421–32, doi:<a href="https://doi.org/10.1007/3-540-49519-3_27">10.1007/3-540-49519-3_27</a>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, in:, Proceedings of the
    2nd International Conference on Formal Methods in Computer-Aided Design, Springer,
    1998, pp. 421–432.
conference:
  end_date: 1998-11-06
  location: Palo Alto, CA, United States of America
  name: 'FMCAD: Formal Methods in Computer-Aided Design'
  start_date: 1998-11-04
date_created: 2018-12-11T12:09:06Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T10:00:50Z
day: '01'
doi: 10.1007/3-540-49519-3_27
extern: '1'
intvolume: '      1522'
language:
- iso: eng
month: '01'
oa_version: None
page: 421 - 432
publication: Proceedings of the 2nd International Conference on Formal Methods in
  Computer-Aided Design
publication_identifier:
  isbn:
  - '9783540651918'
publication_status: published
publisher: Springer
publist_id: '242'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An assume-guarantee rule for checking simulation
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1522
year: '1998'
...