---
_id: '4473'
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, denoting "P is simulated by 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 constraints on transition
    systems.'
article_processing_charge: No
article_type: original
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. <i>ACM Transactions on Programming Languages and Systems
    (TOPLAS)</i>. 2002;24(1):51-64. doi:<a href="https://doi.org/10.1145/509705.509707">10.1145/509705.509707</a>
  apa: Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (2002). An assume-guarantee
    rule for checking simulation. <i>ACM Transactions on Programming Languages and
    Systems (TOPLAS)</i>. ACM. <a href="https://doi.org/10.1145/509705.509707">https://doi.org/10.1145/509705.509707</a>
  chicago: Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran.
    “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming
    Languages and Systems (TOPLAS)</i>. ACM, 2002. <a href="https://doi.org/10.1145/509705.509707">https://doi.org/10.1145/509705.509707</a>.
  ieee: T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee
    rule for checking simulation,” <i>ACM Transactions on Programming Languages and
    Systems (TOPLAS)</i>, vol. 24, no. 1. ACM, pp. 51–64, 2002.
  ista: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 2002. An assume-guarantee rule
    for checking simulation. ACM Transactions on Programming Languages and Systems
    (TOPLAS). 24(1), 51–64.
  mla: Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.”
    <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24,
    no. 1, ACM, 2002, pp. 51–64, doi:<a href="https://doi.org/10.1145/509705.509707">10.1145/509705.509707</a>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming
    Languages and Systems (TOPLAS) 24 (2002) 51–64.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-06-05T07:59:47Z
day: '01'
doi: 10.1145/509705.509707
extern: '1'
fulldoi: https://doi.org/10.1145/509705.509707
intvolume: '        24'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 51 - 64
publication: ACM Transactions on Programming Languages and Systems (TOPLAS)
publication_identifier:
  issn:
  - 0164-0925
publication_status: published
publisher: ACM
publist_id: '256'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An assume-guarantee rule for checking simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 24
year: '2002'
...