Guy Hefetz: Discounted-sum automata with multiple discount factors

A Nondeterministic Finite Automaton (NFA) defines a function from finite words to True/False, corresponding to whether or not the word is in the automaton's language. A Nondeterministic Discounted-sum Automaton (NDA) is a weighted automaton that defines a function from finite or infinite words to real numbers. It is an extension of NFAs, realizing the concept that an immediate reward is better than a potential one in the future. Discounted-summation is very useful in economics (interest rate, inflation, etc.) and plays a key role in various computer-science models (Markov decision processes, discounted games, etc.).

In this talk, I will focus on further extending NDAs info Nondeterministic Discounted-sum Automata with Multiple discount factors (NMDAs).

I will first present NDAs whose discount factor is an integer (integral NDAs), and describe their good computational properties: closure under determinizability and under algebraic operations, and the existence of effective algorithms for their basic decision problems, such as automata equivalence and containment. These properties are essential for effectively using them in formal verification.

I will then turn to present our work, defining and analyzing integral NMDAs, which extend the expressiveness of integral NDAs. I will start with showing that arbitrary integral NMDAs do not preserve the good properties of integral NDAs, and continue with presenting in detail a sub-family of integral NMDAs, which we call tidy-NMDAs, that does preserve all the good properties of integral NDAs.

Along the talk, I will briefly present two novel proof techniques we used. The first is for showing a lower bound on the size blow-up involved in arithmetic operations on NDAs, and the other for efficiently solving the containment problem of tidy NMDAs.