research-article

Quantitative languages

Authors:

Krishnendu Chatterjee,

Thomas A. HenzingerAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 11, Issue 4

Article No.: 23, Pages 1 - 38

https://doi.org/10.1145/1805950.1805953

Published: 20 July 2010 Publication History

Abstract

Quantitative generalizations of classical languages, which assign to each word a real number instead of a Boolean value, have applications in modeling resource-constrained computation. We use weighted automata (finite automata with transition weights) to define several natural classes of quantitative languages over finite and infinite words; in particular, the real value of an infinite run is computed as the maximum, limsup, liminf, limit average, or discounted sum of the transition weights. We define the classical decision problems of automata theory (emptiness, universality, language inclusion, and language equivalence) in the quantitative setting and study their computational complexity. As the decidability of the language-inclusion problem remains open for some classes of weighted automata, we introduce a notion of quantitative simulation that is decidable and implies language inclusion. We also give a complete characterization of the expressive power of the various classes of weighted automata. In particular, we show that most classes of weighted automata cannot be determinized.

References

[1]

Andersson, D. 2006. An improved algorithm for discounted payoff games. In ESSLLI Student Session. 91--98.

[2]

Chakrabarti, A., Chatterjee, K., Henzinger, T. A., Kupferman, O., and Majumdar, R. 2005. Verifying quantitative properties using bound functions. In Proceedings of Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science, vol. 3725. Springer-Varlag, Berlin, 50--64.

Digital Library

[3]

Chakrabarti, A., de Alfaro, L., Henzinger, T. A., and Stoelinga, M. 2003. Resource interfaces. In Proceedings of Embedded Software (EMSOFT). Lecture Notes in Computer Science, vol. 2855. Springer-Verlag, Berlin, 117--133.

[4]

Chatterjee, K. 2007a. Concurrent games with tail objectives. Theoretical Computer Science 388, 181--198.

Digital Library

[5]

Chatterjee, K. 2007b. Stochastic ω-regular games. Ph.D. dissertation, University of California, Berkeley.

[6]

Chatterjee, K. 2008. Linear time algorithm for weak parity games. CoRR abs/0805.1391.

[7]

Chatterjee, K., Doyen, L., and Henzinger, T. A. 2009. Alternating weighted automata. In Proceedings of Fundamentals of Computation Theory (FCT). Lecture Notes in Computer Science, vol. 5699. Springer-Verlag, Berlin, 3--13.

Digital Library

[8]

Chatterjee, K., Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., Pinello, C., and Sangiovanni-Vincentelli, A. 2008. Logical reliability of interacting real-time tasks. In Proceedings of DATE Design, Automation and Test. ACM, New York.

Digital Library

[9]

Condon, A. 1992. The complexity of stochastic games. Inform. Comput. 96, 203--224.

Digital Library

[10]

Culik, K. and Karhumäki, J. 1994. Finite automata computing real functions. SIAM J. Comput. 23, 789--814.

Digital Library

[11]

Dal-Zilio, S. and Lugiez, D. 2003. Xml schema, tree logic and sheaves automata. In Proceedings of Rewriting Techniques and Applications (RTA). 246--263.

Digital Library

[12]

de Alfaro, L., Henzinger, T. A., and Majumdar, R. 2003. Discounting the future in systems theory. In Proceedings of International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 2719. Springer-Verlag, Berlin, 1022--1037.

Digital Library

[13]

Droste, M. and Gastin, P. 2007. Weighted automata and weighted logics. Theor. Comput. Sci. 380, 69--86.

Digital Library

[14]

Droste, M., Kuich, W., and Rahonis, G. 2008. Multi-valued MSO logics over words and trees. Fund. Inform. 84, 305--327.

Digital Library

[15]

Droste, M. and Kuske, D. 2003. Skew and infinitary formal power series. In Proceedings of International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 2719. Springer-Verlag, Berlin, 426--438.

Digital Library

[16]

Ehrenfeucht, A. and Mycielski, J. 1979. Positional strategies for mean payoff games. Int. J. Game Theory. 8, 109--113.

Digital Library

[17]

Emerson, E. A. and Jutla, C. 1991. Tree automata, mu-calculus and determinacy. In Proceedings of Foundations of Computer Science (FOCS). IEEE Computer Society Press, Los Alamitos, CA, 368--377.

Digital Library

[18]

Everett, H. 1957. Recursive games. Ann. Math. Stud. 39. 47--78.

[19]

Filar, J. and Vrieze, K. 1997. Competitive Markov Decision Processes. Springer-Verlag, Berlin.

Digital Library

[20]

Gimbert, H. 2006. Jeux positionnels. Ph.D. dissertation, Université Paris 7.

[21]

Gurfinkel, A. and Chechik, M. 2003. Multi-valued model checking via classical model checking. In Proceedings of Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol, 2761. Springer-Verlag, Berlin, 263--277.

[22]

Henzinger, T., Kupferman, O., and Rajamani, S. 1997. Fair simulation. In Proceedings of Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 1243. Springer-Verlag, Berlin, 273--287.

Digital Library

[23]

Hoffman, A. and Karp, R. 1966. On nonterminating stochastic games. Manag. Sci. 12, 5, 359--370.

Digital Library

[24]

Karianto, W. 2005. Adding monotonic counters to automata and transition graphs. In Proceedings of Developments in Language Theory (DLT). 308--319.

Digital Library

[25]

Karp, R. M. 1978. A characterization of the minimum cycle mean in a digraph. Disc. Math. 23, 3, 309--311.

[26]

Kirsten, D. and Mäurer, I. 2005. On the determinization of weighted automata. J. Autom. Lang. Combinat. 10, 287--312.

[27]

Klaedtke, F. and Ruess, H. 2003. Monadic second-order logics with cardinalities. In Proceedings of International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol, 2719 Springer-Verlag Berlin, 681--696.

Digital Library

[28]

Krob, D. 1992. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In Proceedings of International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 623. Springer-Verlag, Berlin, 101--112.

Digital Library

[29]

Kuich, W. and Salomaa, A. 1986. Semirings, Automata, Languages. Monographs in Theoretical Computer Science. An EATCS Series, vol. 5. Springer-Verlag, Berlin.

Digital Library

[30]

Kupferman, O. and Lustig, Y. 2007. Lattice automata. In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 4349. Springer-Verlag, Berlin, 199--213.

Digital Library

[31]

Kupferman, O. and Vardi, M. Y. 2001. Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2, 3, 408--429.

Digital Library

[32]

Liggett, T. A. and Lippman, S. A. 1969. Stochastic games with perfect information and time average payoff. SIAM Rev. 11, 604--607.

Digital Library

[33]

Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin.

Digital Library

[34]

Mertens, J. and Neyman, A. 1981. Stochastic games. Int. J. Game Theory 10, 53--66.

Digital Library

[35]

Meyer, A. R. and Stockmeyer, L. J. 1972. The equivalence problem for regular expressions with squaring requires exponential space. In Proceedings of Foundations of Computer Science (FOCS). IEEE Computer Society Press, Los Alamitos, CA, 125--129.

Digital Library

[36]

Miyano, S. and Hayashi, T. 1984. Alternating finite automata on omega-words. In Proceedings of International Colloquium on Trees in Algebra and Programming (CAAP). 195--210.

[37]

Mohri, M. 1997. Finite-state transducers in language and speech processing. Comp. Linguistics 23, 2, 269--311.

Digital Library

[38]

Paz, A. 1971. Introduction to Probabilistic Automata. Computer Science and Applied Mathematics. Academic Press, New York.

Digital Library

[39]

Puterman, M. 1994. Markov Decision Processes. Wiley, New York.

[40]

Schützenberger, M. P. 1961. On the definition of a family of automata. Inform. Cont. 4, 245--270.

[41]

Seidl, H., Schwentick, T., and Muscholl, A. 2003. Numerical document queries. In Proceedings of the ACM Symposium on Principles of Database Systems (PODS). 155--166.

Digital Library

[42]

Seidl, H., Schwentick, T., Muscholl, A., and Habermehl, P. 2004. Counting in trees for free. In Proceedings of International Colloquium on Automata, Languages and Programming (ICALP). 1136--1149.

[43]

Shapley, L. S. 1953. Stochastic games. Proc. National Acad. 39, 1095--1100.

[44]

Sistla, A. P., Vardi, M. Y., and Wolper, P. 1987. The complementation problem for Büchi automata with applications to temporal logic. Theoret. Comput. Sci. 49, 217--237.

Digital Library

[45]

Thomas, W. 1997. Languages, automata, and logic. In Handbook of Formal Languages. Vol. 3, Beyond Words. Springer-Verlag, Berlin, Chapter 7, 389--455.

Digital Library

[46]

Wadge, W. 1984. Reducibility and determinateness of Baire spaces. Ph.D. dissertation, University of California, Berkeley.

[47]

Zwick, U. and Paterson, M. 1996. The complexity of mean payoff games on graphs. Theoret. Comput. Sci. 158, 343--359.

Digital Library

Cited By

Boker USobocinski PLago UEsparza J(2024)Discounted-Sum Automata with Real-Valued Discount FactorsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662090(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662090
Wang FTan LCao ZMa YZhang L(2024)A Formal Language for Performance Evaluation Based on Reinforcement LearningInternational Journal of Software Engineering and Knowledge Engineering10.1142/S0218194024500372(1-23)Online publication date: 30-Sep-2024
https://doi.org/10.1142/S0218194024500372
Shi FHuang ZPan HChang YXu H(2024)Fuzzy Safety and Liveness Properties in Linear-time2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS62785.2024.00060(536-545)Online publication date: 1-Jul-2024
https://doi.org/10.1109/QRS62785.2024.00060
Show More Cited By

Index Terms

Quantitative languages
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

Quantitative Automata under Probabilistic Semantics
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions,...
Expressiveness and Closure Properties for Quantitative Languages
LICS '09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science

Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages L that assign to each word w a real number L(w). In the case of infinite words, the value of a run is naturally computed as the ...
Quantitative vs. Weighted Automata
Reachability Problems
Abstract
Weighted automata are widely researched, but with a variety of different semantics, which mostly fit into either the “quantitative view” or the “algebraic view”. We argue that the two views result with incomparable automata families, each ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 11, Issue 4

July 2010

212 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/1805950

Issue’s Table of Contents

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 July 2010

Accepted: 01 December 2009

Revised: 01 September 2009

Received: 01 August 2008

Published in TOCL Volume 11, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

116
Total Citations
View Citations
732
Total Downloads

Downloads (Last 12 months)62
Downloads (Last 6 weeks)4

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Boker USobocinski PLago UEsparza J(2024)Discounted-Sum Automata with Real-Valued Discount FactorsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662090(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662090
Wang FTan LCao ZMa YZhang L(2024)A Formal Language for Performance Evaluation Based on Reinforcement LearningInternational Journal of Software Engineering and Knowledge Engineering10.1142/S0218194024500372(1-23)Online publication date: 30-Sep-2024
https://doi.org/10.1142/S0218194024500372
Shi FHuang ZPan HChang YXu H(2024)Fuzzy Safety and Liveness Properties in Linear-time2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS62785.2024.00060(536-545)Online publication date: 1-Jul-2024
https://doi.org/10.1109/QRS62785.2024.00060
Aazan GGirard AGreco LMason P(2024)An automata theoretic approach to observer design for switched linear systemsAutomatica10.1016/j.automatica.2024.111689165(111689)Online publication date: Jul-2024
https://doi.org/10.1016/j.automatica.2024.111689
Chalupa MHenzinger TMazzocchi NSaraç N(2024)QuAK: Quantitative Automata KitLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_1(3-20)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_1
Aazan GGirard AMason PGreco L(2024)A Joint Spectral Radius for $$\omega $$-Regular Language-Driven Switched Linear SystemsHybrid and Networked Dynamical Systems10.1007/978-3-031-49555-7_7(161-178)Online publication date: 21-Mar-2024
https://doi.org/10.1007/978-3-031-49555-7_7
Bansal S(2023)Automata-Based Quantitative ReasoningACM SIGLOG News10.1145/3617576.361757810:3(4-19)Online publication date: 24-Aug-2023
https://dl.acm.org/doi/10.1145/3617576.3617578
Boker ULehtinen K(2023)When a Little Nondeterminism Goes a Long WayACM SIGLOG News10.1145/3584676.358468210:1(24-51)Online publication date: 14-Feb-2023
https://dl.acm.org/doi/10.1145/3584676.3584682
Droste MGrabolle GRahonis G(2023)Weighted Linear Dynamic LogicInternational Journal of Foundations of Computer Science10.1142/S012905412348008835:01n02(145-177)Online publication date: 16-Nov-2023
https://doi.org/10.1142/S0129054123480088
Ghorbel BPrabhu V(2023)Quantitative Robustness for Signal Temporal Logic With Time-Freeze QuantifiersIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.328329642:12(4436-4449)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1109/TCAD.2023.3283296
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents