---
_id: '4433'
abstract:
- lang: eng
  text: "Bisimulations enjoy numerous applications in the analysis of labeled transition
    systems. Many of these applications are based on two central observations: first,
    bisimilar systems satisfy the same branching-time properties; second, bisimilarity
    can be checked efficiently for finite-state systems. The local character of bisimulation,
    however, makes it difficult to address liveness concerns. Indeed, the definitions
    of fair bisimulation that have been proposed in the literature sacrifice locality,
    and with it, also efficient checkability. We put forward a new definition of fair
    bisimulation which does not suffer from this drawback.\r\nThe bisimilarity of
    two systems can be viewed in terms of a game played between a protagonist and
    an adversary. In each step of the infinite bisimulation game, the adversary chooses
    one system, makes a move, and the protagonist matches it with a move of the other
    system. Consistent with this game-based view, we call two fair transition systems
    bisimilar if in the bisimulation game, the infinite path produced in the first
    system is fair iff the infinite path produced in the second system is fair.\r\nWe
    show that this notion of fair bisimulation enjoys the following properties. First,
    fairly bisimilar systems satisfy the same formulas of the logics Fair-AFMC (the
    fair alternation-free μ-calculus) and Fair-CTL*. Therefore, fair bisimulations
    can serve as property-preserving abstractions for these logics and weaker ones,
    such as Fair-CTL and LTL. Indeed, Fair-AFMC provides an exact logical characterization
    of fair bisimilarity. Second, it can be checked in time polynomial in the number
    of states if two systems are fairly bisimilar. This is in stark contrast to all
    trace-based equivalences, which are traditionally used for addressing liveness
    but require exponential time for checking."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
  the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, the DARPA (MARCO) grant
  MDA972-99-1-0001, and the NSF CAREER award CCR-9501708.
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: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: 'Henzinger TA, Rajamani S. Fair bisimulation. In: <i>Proceedings of the 6th
    International Conference on Tools and Algorithms for the Construction and Analysis
    of Systems</i>. Vol 1785. Springer; 2000:299-314. doi:<a href="https://doi.org/10.1007/3-540-46419-0_21">10.1007/3-540-46419-0_21</a>'
  apa: 'Henzinger, T. A., &#38; Rajamani, S. (2000). Fair bisimulation. In <i>Proceedings
    of the 6th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems</i> (Vol. 1785, pp. 299–314). Berlin, Germany: Springer.
    <a href="https://doi.org/10.1007/3-540-46419-0_21">https://doi.org/10.1007/3-540-46419-0_21</a>'
  chicago: Henzinger, Thomas A, and Sriram Rajamani. “Fair Bisimulation.” In <i>Proceedings
    of the 6th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems</i>, 1785:299–314. Springer, 2000. <a href="https://doi.org/10.1007/3-540-46419-0_21">https://doi.org/10.1007/3-540-46419-0_21</a>.
  ieee: T. A. Henzinger and S. Rajamani, “Fair bisimulation,” in <i>Proceedings of
    the 6th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems</i>, Berlin, Germany, 2000, vol. 1785, pp. 299–314.
  ista: 'Henzinger TA, Rajamani S. 2000. Fair bisimulation. Proceedings of the 6th
    International Conference on Tools and Algorithms for the Construction and Analysis
    of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
    LNCS, vol. 1785, 299–314.'
  mla: Henzinger, Thomas A., and Sriram Rajamani. “Fair Bisimulation.” <i>Proceedings
    of the 6th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems</i>, vol. 1785, Springer, 2000, pp. 299–314, doi:<a href="https://doi.org/10.1007/3-540-46419-0_21">10.1007/3-540-46419-0_21</a>.
  short: T.A. Henzinger, S. Rajamani, in:, Proceedings of the 6th International Conference
    on Tools and Algorithms for the Construction and Analysis of Systems, Springer,
    2000, pp. 299–314.
conference:
  end_date: 2000-04-02
  location: Berlin, Germany
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2000-03-25
date_created: 2018-12-11T12:08:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:11:07Z
day: '01'
doi: 10.1007/3-540-46419-0_21
extern: '1'
intvolume: '      1785'
language:
- iso: eng
month: '01'
oa_version: None
page: 299 - 314
publication: Proceedings of the 6th International Conference on Tools and Algorithms
  for the Construction and Analysis of Systems
publication_identifier:
  isbn:
  - '9783540672821'
publication_status: published
publisher: Springer
publist_id: '297'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fair bisimulation
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1785
year: '2000'
...
---
_id: '4435'
abstract:
- lang: eng
  text: 'An important case of hybrid systems are the rectangular automata. First,
    rectangular dynamics can naturally and arbitrarily closely approximate more general,
    nonlinear dynamics. Second, rectangular automata are the most general type of
    hybrid systems for which model checking -in particular, Ltl model checking- is
    decidable. However, on one hand, the original proofs of decidability did not suggest
    practical algorithms and, on the other hand, practical symbolic model-checking
    procedures -such as those implemented in HyTech- were not known to terminate on
    rectangular automata. We remedy this unsatisfactory situation: we present a symbolic
    method for Ltl model checking which can be performed by HyTech and is guaranteed
    to terminate on all rectangular automata. We do so by proving that our method
    for symbolic Ltl model checking terminates on an infinite-state transition system
    if the trace-equivalence relation of the system has finite index, which is the
    case for all rectangular automata.'
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
  the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660,
  the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
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: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'Henzinger TA, Majumdar R. Symbolic model checking for rectangular hybrid systems.
    In: <i>Proceedings of the 6th International Conference on Tools and Algorithms
    for the Construction and Analysis of Systems</i>. Vol 1785. Springer; 2000:142-156.
    doi:<a href="https://doi.org/10.1007/3-540-46419-0_11">10.1007/3-540-46419-0_11</a>'
  apa: 'Henzinger, T. A., &#38; Majumdar, R. (2000). Symbolic model checking for rectangular
    hybrid systems. In <i>Proceedings of the 6th International Conference on Tools
    and Algorithms for the Construction and Analysis of Systems</i> (Vol. 1785, pp.
    142–156). Berlin, Germany: Springer. <a href="https://doi.org/10.1007/3-540-46419-0_11">https://doi.org/10.1007/3-540-46419-0_11</a>'
  chicago: Henzinger, Thomas A, and Ritankar Majumdar. “Symbolic Model Checking for
    Rectangular Hybrid Systems.” In <i>Proceedings of the 6th International Conference
    on Tools and Algorithms for the Construction and Analysis of Systems</i>, 1785:142–56.
    Springer, 2000. <a href="https://doi.org/10.1007/3-540-46419-0_11">https://doi.org/10.1007/3-540-46419-0_11</a>.
  ieee: T. A. Henzinger and R. Majumdar, “Symbolic model checking for rectangular
    hybrid systems,” in <i>Proceedings of the 6th International Conference on Tools
    and Algorithms for the Construction and Analysis of Systems</i>, Berlin, Germany,
    2000, vol. 1785, pp. 142–156.
  ista: 'Henzinger TA, Majumdar R. 2000. Symbolic model checking for rectangular hybrid
    systems. Proceedings of the 6th International Conference on Tools and Algorithms
    for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
    the Construction and Analysis of Systems, LNCS, vol. 1785, 142–156.'
  mla: Henzinger, Thomas A., and Ritankar Majumdar. “Symbolic Model Checking for Rectangular
    Hybrid Systems.” <i>Proceedings of the 6th International Conference on Tools and
    Algorithms for the Construction and Analysis of Systems</i>, vol. 1785, Springer,
    2000, pp. 142–56, doi:<a href="https://doi.org/10.1007/3-540-46419-0_11">10.1007/3-540-46419-0_11</a>.
  short: T.A. Henzinger, R. Majumdar, in:, Proceedings of the 6th International Conference
    on Tools and Algorithms for the Construction and Analysis of Systems, Springer,
    2000, pp. 142–156.
conference:
  end_date: 2000-04-02
  location: Berlin, Germany
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2000-03-25
date_created: 2018-12-11T12:08:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:08:09Z
day: '01'
doi: 10.1007/3-540-46419-0_11
extern: '1'
intvolume: '      1785'
language:
- iso: eng
month: '01'
oa_version: None
page: 142 - 156
publication: Proceedings of the 6th International Conference on Tools and Algorithms
  for the Construction and Analysis of Systems
publication_identifier:
  isbn:
  - '9783540672821'
publication_status: published
publisher: Springer
publist_id: '293'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for rectangular hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1785
year: '2000'
...