First-Order Definable Policies

Which finite-state reactive agents can have their action rules expressed in first-order logic over observation histories? In my previous post , I used Mealy machines to describe finite-state reactive agents. Here we want to ask which policies can be described using first-order logic. I will first explain what this logic can say about a finite observation history, then connect it to the policies. This post reviews the literature on first-order definability and finite automata and explains how the classical results apply to policies over observation histories. The language characterizations used below are classical results of McNaughton and Papert , and Schützenberger . Throughout, observations and actions come from finite, nonempty sets. First-order logic on an observation history Let be the observation alphabet. A finite word is a sequence of observations, we write for all finite words, including the empty word , and for the nonempty ones. To read a word as a logical structure, take its positions as the objects we can talk about. We have their usual order and, for each observation , a predicate meaning "position carries observation ". For example, in and are true, while is false. The position numbers are labels used to describe the structure. The formulas themselves have access to order, equality, and the letter predicates. There is no addition or predicate for even-numbered positions. A variable such as or denotes one position. We build formulas from the tests , , and , usi…