Temporal logic for planning under uncertainty
This is the abstract of the paper:
John Slaney.
Semipositive LTL with an Uninterpreted Past Operator.
Logic Journal of IGPL 13 (2005): 211-229.
$LTL is a version of linear temporal logic in which eventualities are not expressible, but in which there is a sentential constant $ intended to be true just at the end of some behaviour of interest - that is, to mark the end of the accepted (finite) words of some language. There is an effectively recognisable class of $LTL formulae which express behaviours, but in a sense different from the standard one of temporal logics like LTL or CTL. This representation is useful for solving a class of decision processes with temporally extended goals, which in turn are useful for representing an important class of AI planning problems.