Krishnendu Chatterjee
Skip Abstract Section
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.
- Andersson, D. 2006. An improved algorithm for discounted payoff games. In ESSLLI Student Session. 91--98.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Chatterjee, K. 2007a. Concurrent games with tail objectives. Theoretical Computer Science 388, 181--198. Google ScholarDigital Library
- Chatterjee, K. 2007b. Stochastic ω-regular games. Ph.D. dissertation, University of California, Berkeley.Google Scholar
- Chatterjee, K. 2008. Linear time algorithm for weak parity games. CoRR abs/0805.1391.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Condon, A. 1992. The complexity of stochastic games. Inform. Comput. 96, 203--224. Google ScholarDigital Library
- Culik, K. and Karhumäki, J. 1994. Finite automata computing real functions. SIAM J. Comput. 23, 789--814. Google ScholarDigital Library
- Dal-Zilio, S. and Lugiez, D. 2003. Xml schema, tree logic and sheaves automata. In Proceedings of Rewriting Techniques and Applications (RTA). 246--263. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Droste, M. and Gastin, P. 2007. Weighted automata and weighted logics. Theor. Comput. Sci. 380, 69--86. Google ScholarDigital Library
- Droste, M., Kuich, W., and Rahonis, G. 2008. Multi-valued MSO logics over words and trees. Fund. Inform. 84, 305--327. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Ehrenfeucht, A. and Mycielski, J. 1979. Positional strategies for mean payoff games. Int. J. Game Theory. 8, 109--113.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Everett, H. 1957. Recursive games. Ann. Math. Stud. 39. 47--78.Google Scholar
- Filar, J. and Vrieze, K. 1997. Competitive Markov Decision Processes. Springer-Verlag, Berlin. Google ScholarDigital Library
- Gimbert, H. 2006. Jeux positionnels. Ph.D. dissertation, Université Paris 7.Google Scholar
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Hoffman, A. and Karp, R. 1966. On nonterminating stochastic games. Manag. Sci. 12, 5, 359--370.Google ScholarDigital Library
- Karianto, W. 2005. Adding monotonic counters to automata and transition graphs. In Proceedings of Developments in Language Theory (DLT). 308--319. Google ScholarDigital Library
- Karp, R. M. 1978. A characterization of the minimum cycle mean in a digraph. Disc. Math. 23, 3, 309--311.Google ScholarCross Ref
- Kirsten, D. and Mäurer, I. 2005. On the determinization of weighted automata. J. Autom. Lang. Combinat. 10, 287--312.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Kuich, W. and Salomaa, A. 1986. Semirings, Automata, Languages. Monographs in Theoretical Computer Science. An EATCS Series, vol. 5. Springer-Verlag, Berlin. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Kupferman, O. and Vardi, M. Y. 2001. Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2, 3, 408--429. Google ScholarDigital Library
- Liggett, T. A. and Lippman, S. A. 1969. Stochastic games with perfect information and time average payoff. SIAM Rev. 11, 604--607.Google ScholarDigital Library
- Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin. Google ScholarDigital Library
- Mertens, J. and Neyman, A. 1981. Stochastic games. Int. J. Game Theory 10, 53--66.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Mohri, M. 1997. Finite-state transducers in language and speech processing. Comp. Linguistics 23, 2, 269--311. Google ScholarDigital Library
- Paz, A. 1971. Introduction to Probabilistic Automata. Computer Science and Applied Mathematics. Academic Press, New York. Google ScholarDigital Library
- Puterman, M. 1994. Markov Decision Processes. Wiley, New York.Google Scholar
- Schützenberger, M. P. 1961. On the definition of a family of automata. Inform. Cont. 4, 245--270.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Shapley, L. S. 1953. Stochastic games. Proc. National Acad. 39, 1095--1100.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Thomas, W. 1997. Languages, automata, and logic. In Handbook of Formal Languages. Vol. 3, Beyond Words. Springer-Verlag, Berlin, Chapter 7, 389--455. Google ScholarDigital Library
- Wadge, W. 1984. Reducibility and determinateness of Baire spaces. Ph.D. dissertation, University of California, Berkeley.Google Scholar
- Zwick, U. and Paterson, M. 1996. The complexity of mean payoff games on graphs. Theoret. Comput. Sci. 158, 343--359. Google ScholarDigital Library
Index Terms
- Quantitative languages
Recommendations
Expressiveness and Closure Properties for Quantitative Languages
LICS '09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer ScienceWeighted 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 Automata under Probabilistic Semantics
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceAutomata 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,...
Quantitative vs. Weighted Automata
Reachability ProblemsAbstractWeighted 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