---
res:
  bibo_abstract:
  - '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.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Shaz
      foaf_name: Qadeer, Shaz
      foaf_surname: Qadeer
  - foaf_Person:
      foaf_givenName: Sriram
      foaf_name: Rajamani, Sriram
      foaf_surname: Rajamani
  - foaf_Person:
      foaf_givenName: Serdar
      foaf_name: Tasiran, Serdar
      foaf_surname: Tasiran
  bibo_doi: 10.1145/509705.509707
  bibo_issue: '1'
  bibo_volume: 24
  dct_date: 2002^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0164-0925
  dct_language: eng
  dct_publisher: ACM@
  dct_title: An assume-guarantee rule for checking simulation@
...