Search papers, labs, and topics across Lattice.
This paper introduces the categorizer automaton, a deterministic automaton designed to categorize continuous data into discrete bins by reading an infinite sequence of rewards and determining the corresponding discounted sum. The key advancement is the construction of a categorizer automaton with a state space that scales linearly with the number of bins, significantly improving efficiency over the exponential state space of comparator automata. The authors apply this framework to Markov decision processes, demonstrating that it can synthesize policies that maximize expected utility for both piecewise-constant and piecewise-Lipschitz utility functions in pseudo-polynomial time, while also establishing the PSPACE-hardness of the synthesis problem for piecewise-constant utilities.
The categorizer automaton achieves linear state space complexity, revolutionizing how we synthesize policies for maximizing discounted-sum payoffs in Markov decision processes.
Categorizing continuous data into discrete bins is a fundamental operation in artificial intelligence. We introduce the categorizer automaton, a deterministic automaton that reads an infinite sequence of rewards and identifies which of finitely many bins contains its discounted sum. Categorizer automata generalize comparator automata, the special case of two bins, which have already proven useful in quantitative synthesis. Our main technical contribution is the construction of a categorizer automaton whose state space is linear in the number of bins, rather than exponential as obtained by a cross-product of comparator automata. We then apply categorizer automata to Markov decision processes, where they allow one to synthesize policies that maximize the expected utility of a discounted-sum payoff for utility functions that may be discontinuous. For piecewise-constant utility functions, the resulting algorithm is exact and runs in pseudo-polynomial time. For piecewise-Lipschitz utility functions, a class that includes any utility with bounded slope between finitely many jumps, it again runs in pseudo-polynomial time and yields an $\varepsilon$-optimal policy. We also show that the synthesis problem considered is PSPACE-hard already for piecewise-constant utilities.
