---
res:
  bibo_abstract:
  - 'The simulation preorder for labeled transition systems is defined locally, and
    operationally, as a game that relates states with their immediate successor states.
    Simulation enjoys many appealing properties. First, simulation has a denotational
    characterization: system S simulates system I iff every computation tree embedded
    in the unrolling of I can be embedded also in the unrolling of S. Second, simulation
    has a logical characterization: S simulates I iff every universal branching-time
    formula satisfied by S is satisfied also by I. It follows that simulation is a
    suitable notion of implementation, and it is the coarsest abstraction of a system
    that preserves universal branching-time properties. Third, based on its local
    definition, simulation between finite-state systems can be checked in polynomial
    time. Finally, simulation implies trace containment, which cannot be defined locally
    and requires polynomial space for verification. Hence simulation is widely used
    both in manual and in automatic verification. Liveness assumptions about transition
    systems are typically modeled using fairness constraints. Existing notions of
    simulation for fair transition systems, however, are not local, and as a result,
    many appealing properties of the simulation preorder are lost. We propose a new
    view of fair simulation by extending the local definition of simulation to account
    for fairness: system View the MathML sourcefairly simulates system View the MathML
    source iff in the simulation game, there is a strategy that matches with each
    fair computation of View the MathML source a fair computation of View the MathML
    source. Our definition enjoys a denotational characterization and has a logical
    characterization: View the MathML source fairly simulates View the MathML source
    iff every fair computation tree (whose infinite paths are fair) embedded in the
    unrolling of View the MathML source can be embedded also in the unrolling of View
    the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by
    View the MathML source is satisfied also by View the MathML source (∀AFMC is the
    universal fragment of the alternation-free μ-calculus). The locality of the definition
    leads us to a polynomial-time algorithm for checking fair simulation for finite-state
    systems with weak and strong fairness constraints. Finally, fair simulation implies
    fair trace containment and is therefore useful as an efficiently computable local
    criterion for proving linear-time abstraction hierarchies of fair 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: Orna
      foaf_name: Kupferman, Orna
      foaf_surname: Kupferman
  - foaf_Person:
      foaf_givenName: Sriram
      foaf_name: Rajamani, Sriram
      foaf_surname: Rajamani
  bibo_doi: 10.1006/inco.2001.3085
  bibo_issue: '1'
  bibo_volume: 173
  dct_date: 2002^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0890-5401
  dct_language: eng
  dct_publisher: Elsevier@
  dct_title: Fair simulation@
...