[{"date_created":"2018-12-11T12:09:50Z","month":"06","extern":"1","page":"1022 - 1037","intvolume":"      2719","status":"public","publication":"Proceedings of the 30th International Colloquium on Automata, Languages and Programming","quality_controlled":"1","publisher":"Springer","type":"conference","author":[{"last_name":"De Alfaro","full_name":"De Alfaro, Luca","first_name":"Luca"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"alternative_title":["LNCS"],"day":"25","title":"Discounting the future in systems theory","conference":{"location":"Eindhoven, The Netherlands","name":"ICALP: Automata, Languages and Programming","start_date":"2003-06-30","end_date":"2003-07-04"},"citation":{"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>.","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.","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>","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."},"doi":"10.1007/3-540-45061-0_79","language":[{"iso":"eng"}],"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.","_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 &lt; a &lt; 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."}],"date_published":"2003-06-25T00:00:00Z","article_processing_charge":"No","volume":2719,"publication_status":"published","year":"2003","oa_version":"None","publist_id":"77","publication_identifier":{"isbn":["9783540404934"]},"scopus_import":"1","date_updated":"2023-07-26T13:07:31Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17"},{"volume":2719,"publication_status":"published","abstract":[{"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.","lang":"eng"}],"_id":"4462","date_published":"2003-06-25T00:00:00Z","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2024-01-10T11:19:41Z","scopus_import":"1","publication_identifier":{"isbn":["9783540404934"]},"publist_id":"265","oa_version":"None","year":"2003","quality_controlled":"1","publication":"Proceedings of the 30th International Colloquium on Automata, Languages and Programming","status":"public","intvolume":"      2719","publisher":"Springer","extern":"1","month":"06","date_created":"2018-12-11T12:08:58Z","page":"886 - 902","language":[{"iso":"eng"}],"doi":"10.1007/3-540-45061-0_69","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.","day":"25","alternative_title":["LNCS"],"author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Ranjit","full_name":"Jhala, Ranjit","last_name":"Jhala"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"}],"type":"conference","citation":{"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>.","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.","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>","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":{"location":"Eindhoven, The Netherlands","start_date":"2003-06-30","end_date":"2003-07-04","name":"ICALP: Automata, Languages and Programming"},"title":"Counterexample-guided control"}]