Semipositive LTL with an Uninterpreted Past Operator

Author: Slaney, John

Source: Logic Journal of the IGPL, Volume 13, Number 2, March 2005 , pp. 211-229(19)

Publisher: Oxford University Press

Key:

- Free Content

- New Content

- Subscribed Content

- Free Trial Content

Abstract:

$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.

Keywords: linear temporal logic, decision processes

Document Type: Research article

DOI: 10.1093/jigpal/jzi015

The full text electronic article is available for purchase. You will be able to download the full text electronic article after payment.

$40.03 plus tax Refund Policy