tr-announce

Download

tr-announce@lists.rwth-aachen.de

June 2010

1 participants
2 discussions

2010-12: Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
by Carsten Fuhs 10 Jun '10

10 Jun '10

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.

1 0

2010-11: Parametric LTL Games
by Carsten Fuhs 01 Jun '10

01 Jun '10

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.

1 0