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 , using:
: is "false";
: both are true & : at least one of them is true;
: "some position makes true";
: "every position makes true".
We also use for "if , then ", and for truth and falsity. These are the elements of first-order logic, abbreviated FO, over words.
Consider It says that the history contains a . A slightly longer formula is
It says that every has an somewhere later in the history. It is true on and false on .
An occurrence of a variable is free if it is outside the scope of a quantifier binding that variable. The formula needs a choice of position for . A formula with no free variables is a sentence. We write when the word makes the sentence true.
A language is a set of words. It is FO-definable if one FO sentence is true on exactly its members. We can also define useful abbreviations. For example,
means that is the last position. The sentence
therefore, says that the history ends in . Similarly, consecutive positions can be described by
The claim that no two consecutive observations are both becomes
From sentences to policies
Let be the action alphabet. A policy, or agent function, is a total function
It returns the action taken after an observation history. This follows the observation-history view of agent functions used by Russell and Subramanian, §3.1. A policy is memoryless if it depends only on the last observation. It has finite memory if a deterministic Mealy machine with finitely many states computes its successive actions.
For each action , define its action language
Call the policy FO-definable if each action language has an FO sentence such that for every nonempty history :
Exactly one action sentence must hold on to every nonempty history. For example, the policy that outputs once a has appeared, and otherwise, is defined on nonempty words by
With at least two actions, there are uncountably many policies but only countably many finite families of FO formulas. Thus, only countably many policies are FO-definable.
Star-free languages and aperiodicity
A language is regular if a finite automaton recognizes it. A star-free language can be built from finite languages using union, concatenation, and complement relative to . Concatenation means
For a deterministic finite automaton, each word induces a function on its states: start in , read , and record the resulting state. These functions are closed under composition and include the identity function induced by the empty word. Together they form its transition monoid. The same definition applies to the state transitions of a Mealy machine.
A finite transition monoid is aperiodic if there is an integer such that every element satisfies Here means applying repeatedly times. Call a machine aperiodic when its transition monoid is aperiodic. For any fixed input block, the state observed after each complete repetition eventually stabilizes, with one bound working for all blocks and starting states.
The classical characterization says that, for finite words, the following are equivalent: FO-definability, star-freeness, and recognition by an aperiodic finite automaton. The FO & star-free equivalence is due to McNaughton and Papert. The star-free & aperiodic equivalence is due to Schützenberger. Diekert and Gastin, Theorem 1.1 and §1, gives the characterization and its attribution.
Applying it to action languages gives the following statements.
Proposition 1: A policy is FO-definable exactly when every action language is star-free. Every FO-definable policy has finite memory. A finite-memory policy is FO-definable exactly when it has an aperiodic Mealy implementation.
Equivalently, a regular language is FO-definable exactly when its minimal DFA is aperiodic.
For a simple boundary example, let and define
where counts the occurrences of . Two states suffice: each flips the state, and each leaves it unchanged.
This policy has no FO definition. If its action-language was FO-definable, restricting to words consisting entirely of would give an FO definition of odd unary length. The minimal automaton for that language has two states exchanged by . This exchange never stabilizes under repetition, contradicting the aperiodicity characterization. If the logic is extended with quantification over sets of positions, it becomes monadic second-order logic (MSO). Büchi's classical theorem says that MSO on finite words defines all regular languages.
Which machine should we inspect?
A machine that always outputs could still toggle an unused bit on every observation. Its transition monoid would fail aperiodicity, even though a one-state machine implements the same policy. The relevant quotient uses future behavior. For histories , define
Thus, two histories are equivalent when every nonempty continuation produces the same final action. The number of equivalence classes is called the index of the relation.
Proposition 2: The relation has finite index exactly when has finite memory, and that index is the minimum number of reachable Mealy states. When the quotient is finite, its transition monoid is aperiodic exactly when is FO-definable.
Further Reading
Relation to string-transduction:
More general string functions can change output length or postpone output until later input has been read. An FO string transformation specifies output positions, labels, and order using FO formulas over the input, allowing finitely many copies of input positions.
A streaming string transducer is a finite controller with registers storing strings, updated as it reads the input. Filiot, Krishna and Trivedi characterize FO string transformations by aperiodic, 1-bounded streaming string transducers (Theorem 16 in the extended paper).
On the complexity side:
PSPACE is the class of decision problems solvable with memory polynomial in the input length. A problem is PSPACE-complete if it belongs to this class and every problem in the class reduces to it in polynomial time.
Filiot, Gauwin and Lhote (Corollary 5.6, Proposition 5.7) prove that testing FO-definability for a rational function presented by a bimachine is PSPACE-complete. They also prove decidability for a function presented by a finite-state transducer.
So far, the defining formulas must agree with the policy on every possible observation history. In the next post, we will discuss what changes when agreement is required only on histories reachable in a given environment.
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
For example, in
A variable such as
We also use
Consider
It says that every
An occurrence of a variable is free if it is outside the scope of a quantifier binding that variable. The formula
A language is a set of words. It is FO-definable if one FO sentence is true on exactly its members. We can also define useful abbreviations. For example,
means that
therefore, says that the history ends in
The claim that no two consecutive observations are both
From sentences to policies
Let
It returns the action taken after an observation history. This follows the observation-history view of agent functions used by Russell and Subramanian, §3.1. A policy is memoryless if it depends only on the last observation. It has finite memory if a deterministic Mealy machine with finitely many states computes its successive actions.
For each action
Call the policy FO-definable if each action language
Exactly one action sentence must hold on to every nonempty history. For example, the policy that outputs
With at least two actions, there are uncountably many policies but only countably many finite families of FO formulas. Thus, only countably many policies are FO-definable.
Star-free languages and aperiodicity
A language is regular if a finite automaton recognizes it. A star-free language can be built from finite languages using union, concatenation, and complement relative to
For a deterministic finite automaton, each word
A finite transition monoid is aperiodic if there is an integer
The classical characterization says that, for finite words, the following are equivalent: FO-definability, star-freeness, and recognition by an aperiodic finite automaton. The FO & star-free equivalence is due to McNaughton and Papert. The star-free & aperiodic equivalence is due to Schützenberger. Diekert and Gastin, Theorem 1.1 and §1, gives the characterization and its attribution.
Applying it to action languages gives the following statements.
For a simple boundary example, let
where
This policy has no FO definition. If its action-
Which machine should we inspect?
A machine that always outputs
Thus, two histories are equivalent when every nonempty continuation produces the same final action. The number of equivalence classes is called the index of the relation.
Further Reading
Relation to string-transduction:
More general string functions can change output length or postpone output until later input has been read. An FO string transformation specifies output positions, labels, and order using FO formulas over the input, allowing finitely many copies of input positions.
A streaming string transducer is a finite controller with registers storing strings, updated as it reads the input. Filiot, Krishna and Trivedi characterize FO string transformations by aperiodic, 1-bounded streaming string transducers (Theorem 16 in the extended paper).
On the complexity side:
PSPACE is the class of decision problems solvable with memory polynomial in the input length. A problem is PSPACE-complete if it belongs to this class and every problem in the class reduces to it in polynomial time.
Filiot, Gauwin and Lhote (Corollary 5.6, Proposition 5.7) prove that testing FO-definability for a rational function presented by a bimachine is PSPACE-complete. They also prove decidability for a function presented by a finite-state transducer.
So far, the defining formulas must agree with the policy on every possible observation history. In the next post, we will discuss what changes when agreement is required only on histories reachable in a given environment.