---
_id: '4628'
abstract:
- lang: eng
  text: 'Discounting the future means that the value, today, of a unit payoffis 1
    if the payoffo ccurs today, a if it occurs tomorrow, a 2 if it occurs the day
    after tomorrow, and so on, for some real-valued discount factor 0 < a <
    1. Discounting (or inflation) is a key paradigm in economics and has been studied
    in Markov decision processes as well as game theory. We submit that discounting
    also has a natural place in systems engineering: for nonterminating systems, a
    potential bug in the far-away future is less troubling than a potential bug today.
    We therefore develop a systems theory with discounting. Our theory includes several
    basic elements: discounted versions of system properties that correspond to the
    ω-regular properties, fixpoint-based algorithms for checking discounted properties,
    and a quantitative notion of bisimilarity for capturing the difference between
    two states with respect to discounted properties. We present the theory in a general
    form that applies to probabilistic systems as well as multicomponent systems (games),
    but it readily specializes to classical transition systems. We show that discounting,
    besides its natural practical appeal, has also several mathematical benefits.
    First, the resulting theory is robust, in that small perturbations of a system
    can cause only small changes in the properties of the system. Second, the theory
    is computational, in that the values of discounted properties, as well as the
    discounted bisimilarity distance between states, can be computed to any desired
    degree of precision.'
acknowledgement: This research was supported in part by the NSF CAREER award CCR-0132780,
  the DARPA grant F33615-C-98-3614, the NSF grants CCR-9988172, CCR-0234690 and CCR-0225610,
  and the ONR grant N00014-02-1-0671.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- 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: 'De Alfaro L, Henzinger TA, Majumdar R. Discounting the future in systems theory.
    In: <i>Proceedings of the 30th International Colloquium on Automata, Languages
    and Programming</i>. Vol 2719. Springer; 2003:1022-1037. doi:<a href="https://doi.org/10.1007/3-540-45061-0_79">10.1007/3-540-45061-0_79</a>'
  apa: 'De Alfaro, L., Henzinger, T. A., &#38; Majumdar, R. (2003). Discounting the
    future in systems theory. In <i>Proceedings of the 30th International Colloquium
    on Automata, Languages and Programming</i> (Vol. 2719, pp. 1022–1037). Eindhoven,
    The Netherlands: Springer. <a href="https://doi.org/10.1007/3-540-45061-0_79">https://doi.org/10.1007/3-540-45061-0_79</a>'
  chicago: De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Discounting
    the Future in Systems Theory.” In <i>Proceedings of the 30th International Colloquium
    on Automata, Languages and Programming</i>, 2719:1022–37. Springer, 2003. <a href="https://doi.org/10.1007/3-540-45061-0_79">https://doi.org/10.1007/3-540-45061-0_79</a>.
  ieee: L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Discounting the future in
    systems theory,” in <i>Proceedings of the 30th International Colloquium on Automata,
    Languages and Programming</i>, Eindhoven, The Netherlands, 2003, vol. 2719, pp.
    1022–1037.
  ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2003. Discounting the future in systems
    theory. Proceedings of the 30th International Colloquium on Automata, Languages
    and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2719,
    1022–1037.'
  mla: De Alfaro, Luca, et al. “Discounting the Future in Systems Theory.” <i>Proceedings
    of the 30th International Colloquium on Automata, Languages and Programming</i>,
    vol. 2719, Springer, 2003, pp. 1022–37, doi:<a href="https://doi.org/10.1007/3-540-45061-0_79">10.1007/3-540-45061-0_79</a>.
  short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 30th International
    Colloquium on Automata, Languages and Programming, Springer, 2003, pp. 1022–1037.
conference:
  end_date: 2003-07-04
  location: Eindhoven, The Netherlands
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2003-06-30
date_created: 2018-12-11T12:09:50Z
date_published: 2003-06-25T00:00:00Z
date_updated: 2023-07-26T13:07:31Z
day: '25'
doi: 10.1007/3-540-45061-0_79
extern: '1'
intvolume: '      2719'
language:
- iso: eng
month: '06'
oa_version: None
page: 1022 - 1037
publication: Proceedings of the 30th International Colloquium on Automata, Languages
  and Programming
publication_identifier:
  isbn:
  - '9783540404934'
publication_status: published
publisher: Springer
publist_id: '77'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discounting the future in systems theory
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2719
year: '2003'
...
---
_id: '4462'
abstract:
- lang: eng
  text: 'A major hurdle in the algorithmic verification and control of systems is
    the need to find suitable abstract models, which omit enough details to overcome
    the state-explosion problem, but retain enough details to exhibit satisfaction
    or controllability with respect to the specification. The paradigm of counterexample-guided
    abstraction refinement suggests a fully automatic way of finding suitable abstract
    models: one starts with a coarse abstraction, attempts to verify or control the
    abstract model, and if this attempt fails and the abstract counterexample does
    not correspond to a concrete counterexample, then one uses the spurious counterexample
    to guide the refinement of the abstract model. We present a counterexample-guided
    refinement algorithm for solving ω-regular control objectives. The main difficulty
    is that in control, unlike in verification, counterexamples are strategies in
    a game between system and controller. In the case that the controller has no choices,
    our scheme subsumes known counterexample-guided refinement algorithms for the
    verification of ω-regular specifications. Our algorithm is useful in all situations
    where ω-regular games need to be solved, such as supervisory control, sequential
    and program synthesis, and modular verification. The algorithm is fully symbolic,
    and therefore applicable also to infinite-state systems.'
acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614,
  the ONR grant N00014-02-1-0671, and the NSF grants CCR-9988172, CCR-0085949, and
  CCR-0225610.
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: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'Henzinger TA, Jhala R, Majumdar R. Counterexample-guided control. In: <i>Proceedings
    of the 30th International Colloquium on Automata, Languages and Programming</i>.
    Vol 2719. Springer; 2003:886-902. doi:<a href="https://doi.org/10.1007/3-540-45061-0_69">10.1007/3-540-45061-0_69</a>'
  apa: 'Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2003). Counterexample-guided
    control. In <i>Proceedings of the 30th International Colloquium on Automata, Languages
    and Programming</i> (Vol. 2719, pp. 886–902). Eindhoven, The Netherlands: Springer.
    <a href="https://doi.org/10.1007/3-540-45061-0_69">https://doi.org/10.1007/3-540-45061-0_69</a>'
  chicago: Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Counterexample-Guided
    Control.” In <i>Proceedings of the 30th International Colloquium on Automata,
    Languages and Programming</i>, 2719:886–902. Springer, 2003. <a href="https://doi.org/10.1007/3-540-45061-0_69">https://doi.org/10.1007/3-540-45061-0_69</a>.
  ieee: T. A. Henzinger, R. Jhala, and R. Majumdar, “Counterexample-guided control,”
    in <i>Proceedings of the 30th International Colloquium on Automata, Languages
    and Programming</i>, Eindhoven, The Netherlands, 2003, vol. 2719, pp. 886–902.
  ista: 'Henzinger TA, Jhala R, Majumdar R. 2003. Counterexample-guided control. Proceedings
    of the 30th International Colloquium on Automata, Languages and Programming. ICALP:
    Automata, Languages and Programming, LNCS, vol. 2719, 886–902.'
  mla: Henzinger, Thomas A., et al. “Counterexample-Guided Control.” <i>Proceedings
    of the 30th International Colloquium on Automata, Languages and Programming</i>,
    vol. 2719, Springer, 2003, pp. 886–902, doi:<a href="https://doi.org/10.1007/3-540-45061-0_69">10.1007/3-540-45061-0_69</a>.
  short: T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the 30th International
    Colloquium on Automata, Languages and Programming, Springer, 2003, pp. 886–902.
conference:
  end_date: 2003-07-04
  location: Eindhoven, The Netherlands
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2003-06-30
date_created: 2018-12-11T12:08:58Z
date_published: 2003-06-25T00:00:00Z
date_updated: 2024-01-10T11:19:41Z
day: '25'
doi: 10.1007/3-540-45061-0_69
extern: '1'
intvolume: '      2719'
language:
- iso: eng
month: '06'
oa_version: None
page: 886 - 902
publication: Proceedings of the 30th International Colloquium on Automata, Languages
  and Programming
publication_identifier:
  isbn:
  - '9783540404934'
publication_status: published
publisher: Springer
publist_id: '265'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Counterexample-guided control
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2719
year: '2003'
...