# A Class of Reward-Normal Formulae

The existing decision procedure [41] for determining whether a formula is reward-normal is guaranteed to terminate finitely, but involves the construction and comparison of automata and is rather intricate in practice. It is therefore useful to give a simple syntactic characterisation of a set of constructors for obtaining reward-normal formulae even though not all such formulae are so constructible. We say that a formula is material iff it contains no and no temporal operators - that is, the material formulae are the boolean combinations of atoms. We consider four operations on behaviours representable by formulae of \$FLTL. Firstly, a behaviour may be delayed for a specified number of timesteps. Secondly, it may be made conditional on a material trigger. Thirdly, it may be started repeatedly until a material termination condition is met. Fourthly, two behaviours may be combined to form their union. These operations are easily realised syntactically by corresponding operations on formulae. Where is any material formula:

We have shown [41] that the set of reward-normal formulae is closed under delay, cond (for any material ), loop (for any material ) and union, and also that the closure of under these operations represents a class of behaviours closed under intersection and concatenation as well as union. Many familiar reward-normal formulae are obtainable from by applying the four operations. For example, is . Sometimes a paraphrase is necessary. For example, is not of the required form because of the in the antecedent of the conditional, but the equivalent is . Other cases are not so easy. An example is the formula which stipulates a reward the first time happens and which is not at all of the form suggested. To capture the same behaviour using the above operations requires a formula like .
Sylvie Thiebaux 2006-01-20