Semipositive LTL with an uninterpreted past operator
$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...[Show more]
|Collections||ANU Research Publications|
|Source:||Logic Journal of the IGPL|
|01_Slaney_Semipositive_LTL_with_an_2005.pdf||388.27 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.