---
_id: '4587'
abstract:
- lang: eng
  text: We argue that the standard constraints on liveness conditions in nonblocking
    trace models—machine closure for closed systems, and receptiveness for open systems—are
    unnecessarily weak and complex, and that liveness should, instead, be specified
    by augmenting transition systems with acceptance conditions that satisfy a locality
    constraint. First, locality implies machine closure and receptiveness, and thus
    permits the composition and modular verification of live transition systems. Second,
    while machine closure and receptiveness are based on infinite games, locality
    is based on repeated finite games, and thus easier to check. Third, no expressive
    power is lost by the restriction to local liveness conditions. We illustrate the
    appeal of local liveness using the model of Fair Reactive Systems, a nonblocking
    trace model of communicating processes.
acknowledgement: Supported in part by the NSF grant CCR-9200794, by the AFOSR contract
  F49620-93-1-0056, and by the DARPA grant NAG2-892.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Alur R, Henzinger TA. Local liveness for compositional modeling of fair reactive
    systems. In: <i>7th International Conference on Computer Aided Verification</i>.
    Vol 939. Springer; 1995:166-179. doi:<a href="https://doi.org/10.1007/3-540-60045-0_49">10.1007/3-540-60045-0_49</a>'
  apa: 'Alur, R., &#38; Henzinger, T. A. (1995). Local liveness for compositional
    modeling of fair reactive systems. In <i>7th International Conference on Computer
    Aided Verification</i> (Vol. 939, pp. 166–179). Liege, Belgium: Springer. <a href="https://doi.org/10.1007/3-540-60045-0_49">https://doi.org/10.1007/3-540-60045-0_49</a>'
  chicago: Alur, Rajeev, and Thomas A Henzinger. “Local Liveness for Compositional
    Modeling of Fair Reactive Systems.” In <i>7th International Conference on Computer
    Aided Verification</i>, 939:166–79. Springer, 1995. <a href="https://doi.org/10.1007/3-540-60045-0_49">https://doi.org/10.1007/3-540-60045-0_49</a>.
  ieee: R. Alur and T. A. Henzinger, “Local liveness for compositional modeling of
    fair reactive systems,” in <i>7th International Conference on Computer Aided Verification</i>,
    Liege, Belgium, 1995, vol. 939, pp. 166–179.
  ista: 'Alur R, Henzinger TA. 1995. Local liveness for compositional modeling of
    fair reactive systems. 7th International Conference on Computer Aided Verification.
    CAV: Computer Aided Verification, LNCS, vol. 939, 166–179.'
  mla: Alur, Rajeev, and Thomas A. Henzinger. “Local Liveness for Compositional Modeling
    of Fair Reactive Systems.” <i>7th International Conference on Computer Aided Verification</i>,
    vol. 939, Springer, 1995, pp. 166–79, doi:<a href="https://doi.org/10.1007/3-540-60045-0_49">10.1007/3-540-60045-0_49</a>.
  short: R. Alur, T.A. Henzinger, in:, 7th International Conference on Computer Aided
    Verification, Springer, 1995, pp. 166–179.
conference:
  end_date: 1995-07-05
  location: Liege, Belgium
  name: 'CAV: Computer Aided Verification'
  start_date: 1995-07-03
date_created: 2018-12-11T12:09:37Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-09T14:05:04Z
day: '01'
doi: 10.1007/3-540-60045-0_49
extern: '1'
intvolume: '       939'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60045-0_49
month: '01'
oa_version: None
page: 166 - 179
publication: 7th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - 978-3-540-60045-9
publication_status: published
publisher: Springer
publist_id: '120'
quality_controlled: '1'
status: public
title: Local liveness for compositional modeling of fair reactive systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 939
year: '1995'
...