Semipositive LTL with an uninterpreted past operator
Date
2005
Authors
Slaney, John K
Journal Title
Journal ISSN
Volume Title
Publisher
British Academy and Oxford University Press
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.
Description
Keywords
Keywords: Decision processes; Linear temporal logic
Citation
Collections
Source
Logic Journal of the IGPL
Type
Journal article
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description