Abstract
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.
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur and T.A. Henzinger. Finitary fairness. ACM TOPLAS, 20:1171–1194, 1994.
R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49:672–713, 2002.
R. Alur, T.A. Henzinger, O. Kupferman, and M.Y. Vardi. Alternating refinement relations. In Concurrency Theory, LNCS 1466, pp. 163–178. Springer, 1998.
M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.
J.R. Büchi. On a decision method in restricted second-order arithmetic. In Congr. Logic, Methodology, and Philosophy of Science 1960, pp. 1–12. Stanford University Press, 1962.
L. de Alfaro. Stochastic transition systems. In Concurrency Theory, LNCS 1466, pp. 423–438. Springer, 1998.
L. de Alfaro, T.A. Henzinger, and O. Kupferman. Concurrent reachability games. In Symp. Foundations of Computer Science, pp. 564–575. IEEE, 1998.
L. de Alfaro, T.A. Henzinger, and R. Majumdar. From verification to control: Dynamic programs for ω-regular objectives. In Symp. Logic in Computer Science, pp. 279–290. IEEE, 2001.
L. de Alfaro and R. Majumdar. Quantitative solution of ω-regular games. In Symp. Theory of Computing, pp. 675–683. ACM, 2001.
C. Derman. Finite-State Markovian Decision Processes. Academic Press, 1970.
J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labeled Markov systems. In Concurrency Theory, LNCS 1664, pp. 258–273. Springer, 1999.
J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Symp. Logic in Computer Science, pp. 413–422. IEEE, 2002.
E.A. Emerson and C.S. Jutla. Tree automata, μ-calculus and determinacy. In Symp. Foundations of Computer Science, pp. 368–377. IEEE, 1991.
E.A. Emerson, C.S. Jutla, and A.P. Sistla. On model checking for fragments of μ-calculus. In Computer-aided Verification, LNCS 697, pp. 385–396. Springer, 1993.
E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Symp. Logic in Computer Science, pp. 267–278. IEEE, June 1986.
J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer, 1997.
Y. Gurevich and L. Harrington. Trees, automata, and games. In Symp. Theory of Computing, pp. 60–65. ACM, 1982.
C.-C. Jou and S.A. Smolka. Equivalences, congruences, and complete axiomatizations for probabilistic processes. In Concurrency Theory, LNCS 458, pp. 367–383. Springer, 1990.
D. Kozen. A probabilistic PDL. In Symp. Theory of Computing, pp. 291–297. ACM, 1983.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Symp. Principles of Distributed Computing, pp. 377–408. ACM, 1990.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1991.
A. McIver. Reasoning about efficiency within a probabilitic μ-calculus. Electronic Notes in Theoretical Computer Science, 22, 1999.
R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, ed., Handbook of Theoretical Computer Science, vol. B, pp. 1202–1242. Elsevier, 1990.
A.W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In Computation Theory, LNCS 208, pp. 157–168. Springer, 1984.
G. Owen. Game Theory. Academic Press, 1995.
A. Pnueli. The temporal logic of programs. In Symp. Foundations of Computer Science, pp. 46–57. IEEE, 1977.
M.O. Rabin. Automata on Infinite Objects and Church’s Problem. Conference Series in Mathematics, vol. 13. AMS, 1969.
R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995. Tech. Rep. MIT/LCS/TR-676.
R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. In Concurrency Theory, LNCS 836, pp. 481–496. Springer, 1994.
L.S. Shapley. Stochastic games. Proc. National Academy of Sciences, 39:1095–1100, 1953.
W. Thomas. On the synthesis of strategies in infinite games. In Theoretical Aspects of Computer Science, LNCS 900, pp. 1–13. Springer, 1995.
M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state systems. In Symp. Foundations of Computer Science, pp. 327–338. IEEE, 1985.
M.Y. Vardi. A temporal fixpoint calculus. In Symp. Principles of Programming Languages, pp. 250–259. ACM, 1988.
J. von Neumann and O. Morgenstern. Theory of Games and Economic Behavior. Princeton University Press, 1947.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Alfaro, L., Henzinger, T.A., Majumdar, R. (2003). Discounting the Future in Systems Theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds) Automata, Languages and Programming. ICALP 2003. Lecture Notes in Computer Science, vol 2719. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45061-0_79
Download citation
DOI: https://doi.org/10.1007/3-540-45061-0_79
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40493-4
Online ISBN: 978-3-540-45061-0
eBook Packages: Springer Book Archive