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)

Buy & download fulltext article:

Price: $42.29 plus tax (Refund Policy)

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: http://dx.doi.org/10.1093/jigpal/jzi015

Publication date: 2005-03-01

More about this publication?

Logic Journal of the IGPL publishes papers in all areas of pure and applied logic, including pure logical systems, proof theory, model theory, recursion theory, type theory, nonclassical logics, nonmonotonic logic, numerical and uncertainty reasoning, logic and AI, foundations of logic programming, logic and computation, logic and language, and logic engineering.