TAL formulas

Below, we will define TAL logic formulas. The definition is very informal and some parts have been omitted; see Notes on PMON Circumscription for the formal definition. In short,

Variables are used in quantification.
Timepoints
Elementary fluent formulas state that a fluent has a certain value.
Fluent formulas are logical combinations of elementary fluent formulas.
Fixed fluent formulas are fluent formulas attached to a timepoint or an interval.
Logic formulas are the most complex formulas; they are used in observations.

We will assume that the value domains and features are given.

Variables

You can use universal and existential quantification over values and timepoints. Value variables have the same name as their domain, possibly with a digit suffix: If the domain is called boolean, the value variables you can use are called boolean, boolean1, boolean2, and so on. Temporal variables are named s or t, possibly with a digit suffix.

The VTAL system does not allow you to use free variables: A variable v can only be used inside a forall v or exists v quantifier.

Timepoints

Wherever you can use a timepoint, you can use any expression of the following form:

A temporal variable
A non-negative integer
Timepoint + timepoint
Timepoint - timepoint
(Timepoint)

That is, the following are valid timepoints:

1 + 2 + 3
(0)
t1 - t2 + 7
(t1 - t2) + (t2 + 7)

Elementary fluent formulas

An elementary fluent formula is of the form feature == {value1, value2, ..., valuen}. This means that the feature (which may or may not have arguments) takes on one of the values in the set -- a feature never has more than one value, but we don't have complete information about which value that is. For example,

    color_of(my_car) == {blue, red}

means that the color of my car is blue or red. It does not have both colors at once; I'm simply not sure whether it is blue or red, but I know that it is not yellow.

If there is only one value, it is not necessary to include the braces. The following two lines are equivalent:

door_is_open ==  true
door_is_open ==  {true}

It is also possible to specify that a feature does not have a value:

color_of(my_car) ==  !{green, white}

The above states that my car is not green and not white; it can have any other color (that is, any other color which is allowed by the other formulas in the scenario description).

The values in the set can be value names (such as "blue" or "red"), value variables (such as "color2") or other features (such as "color_of(your_car)"). The following states that my car is blue or red or has the color color2 or the same color as your car:

color_of(my_car) == {blue, red, color2, color_of(your_car)}

Note that there is no timepoint involved in an elementary fluent formula. Therefore, it has no real meaning unless it is a part of a fixed fluent formula.

Fluent formulas

A fluent formula is a boolean combination of elementary fluent formulas, possibly containing quantifiers over values. For example, the car example from above can also be expressed as the following fluent formula:

color_of(my_car) ==  blue  |  color_of(my_car) == red

Quantifiers are written using the following syntax:

forall variable [ formula ]

exists variable [ formula ]

For example, I can state that all cars are red, and that there is a blue car (this is of course a contradiction):

forall car1 [ color_of(car1) ==  red ] & exists car2 [ color_of(car2) == blue ]

There are five logical operators, listed in order of precedence:

! -- negation
& -- conjunction (and)
| -- disjunction (or)
-> -- implication (if-then)
<-> -- equivalence (if and only if)

Some additional examples of fluent formulas:

!canuse(v[vehicle], dist(whereami, nextloc(whereami))) -> !dodepart(v[vehicle])

blocked(duct1) & !blocked(duct2) & at(box1, loc1) & !stuffy

Fixed fluent formulas

A fixed fluent formula is a fluent formula prefixed by a timepoint or a temporal interval. This gives the formula its meaning: The fixed fluent formula is true in an interpretation if and only if the fluent formula is true at the given timepoint or at all timepoints in the temporal interval.

For example, to continue with the car color example from above: If the color of my car is blue or red at timepoint 0, this can be expressed as a fixed fluent formula:

[0] color_of(my_car) ==  {blue, red}

Temporal intervals can be open or closed using the standard notation:

(t1,t2) -- t1 and t2 excluded from the interval
[t1,t2) -- t1 included, t2 excluded
(t1,t2] -- t1 excluded, t2 included
[t1,t2] -- t1 and t2 included in interval

If all cars are green in the time interval [5,20]:

[5,20] forall car1 [ color_of(car1) == green ]

Logic formulas

A logic formula can be any of the following:

t = t', t < t' or t <= t', where t and t' are timepoints -- a comparison between timepoints.
v = v', where v and v' are value names or value variables.
A fixed fluent formula
A boolean combination of other logic formulas, possibly containing quantifiers over timepoints or values.

The following are examples of logic formulas:

[0] color_of(my_car) ==  {blue, red} & [5,20] forall car1 [ color_of(car1) ==  green ]

[0] !inlake & !wet & hat

forall car1 [ [0] color_of(car1) ==  { color_of(my_car) } ]

[0] !on(switch1) & on(switch2) & !on(switch3)