The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Dependency Triples for Improving Termination Analysis of
Logic Programs with Cut
Thomas Ströder, Peter Schneider-Kamp, Jürgen Giesl
AIB 2010-12
In very recent work, we introduced a non-termination preserving
transformation from logic programs with cut to definite logic
programs. While that approach allows us to prove termination of a
large class of logic programs with cut automatically, in several
cases the transformation results in a non-terminating definite logic
program. In this paper we extend the transformation such that logic
programs with cut are no longer transformed into definite logic
programs, but into dependency triple problems. By the implementation
of our new method and extensive experiments, we empirically evaluate
the practical benefit of our contributions.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Parametric LTL Games
Martin Zimmermann
AIB 2010-11
We consider graph games of infinite duration with winning conditions
in parameterized linear temporal logic, where the temporal operators
are equipped with variables for time bounds. In model checking such
specifications were introduced as PLTL by Alur et al. and (in a
different version called PROMPT-LTL) by Kupferman et al..
Our work lifts their results on model checking for PLTL and PROMPT-LTL
to the level of games: we present algorithms that determine whether a
player wins a game with respect to some, infinitely many, or all
variable valuations. All these algorithms run in doubly-exponential
time; so, adding bounded temporal operators does not increase the
complexity compared to solving plain LTL games. Furthermore, we show
how to determine optimal valuations that allow a player to win a
game.