diff --git a/include/cdd/cdd.h b/include/cdd/cdd.h
index 51c485f..215e222 100644
--- a/include/cdd/cdd.h
+++ b/include/cdd/cdd.h
@@ -881,6 +881,7 @@ class cdd
                                    int32_t num_clock_resets, int32_t* bool_resets, int32_t num_bool_resets);
     friend cdd cdd_transition_back_past(const cdd& state, const cdd& guard, const cdd& update, int32_t* clock_resets,
                                         int32_t num_clock_resets, int32_t* bool_resets, int32_t num_bool_resets);
+    friend cdd cdd_predt(const cdd& target, const cdd& safe);
     friend cdd cdd_reduce2(const cdd&);
     friend bool cdd_contains(const cdd&, raw_t* dbm, int32_t dim);
     friend cdd cdd_extract_dbm(const cdd&, raw_t* dbm, int32_t dim);
diff --git a/src/cppext.cpp b/src/cppext.cpp
index 13ae89e..4e68e32 100644
--- a/src/cppext.cpp
+++ b/src/cppext.cpp
@@ -11,7 +11,10 @@
 
 #include "cdd/kernel.h"
 
-#define ADBM(NAME) raw_t* NAME = allocDBM(size)
+#include <dbm/fed.h>
+#include <dbm/print.h>
+
+#define ADBM(NAME, DIM) raw_t* NAME = allocDBM(DIM)
 
 /* Allocate a DBM. */
 static raw_t* allocDBM(uint32_t dim) { return (raw_t*)malloc(dim * dim * sizeof(raw_t)); }
@@ -69,10 +72,9 @@ cdd cdd::operator=(ddNode* node)
  */
 extraction_result cdd_extract_bdd_and_dbm(const cdd& state)
 {
-    uint32_t size = cdd_clocknum;
-    ADBM(dbm);
-    cdd bdd_part = cdd_extract_bdd(state, size);
-    cdd cdd_part = cdd_extract_dbm(state, dbm, size);
+    ADBM(dbm, cdd_clocknum);
+    cdd bdd_part = cdd_extract_bdd(state, cdd_clocknum);
+    cdd cdd_part = cdd_extract_dbm(state, dbm, cdd_clocknum);
     extraction_result res;
     res.BDD_part = bdd_part;
     res.CDD_part = cdd_part;
@@ -93,27 +95,174 @@ extraction_result cdd_extract_bdd_and_dbm(const cdd& state)
  */
 cdd cdd_delay(const cdd& state)
 {
-    if (cdd_isterminal(state.root))
+    // First some trivial cases.
+    if (cdd_isterminal(state.handle()))
         return state;
-    if (cdd_info(state.root)->type == TYPE_BDD)
+    if (cdd_info(state.handle())->type == TYPE_BDD)
         return state;
-    uint32_t size = cdd_clocknum;
+
     cdd copy = state;
     cdd res = cdd_false();
-    ADBM(dbm);
-    while (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type != TYPE_BDD) {
+    ADBM(dbm, cdd_clocknum);
+    while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) {
         copy = cdd_reduce(copy);
-        cdd bottom = cdd_extract_bdd(copy, size);
-        copy = cdd_extract_dbm(copy, dbm, size);
+        cdd bottom = cdd_extract_bdd(copy, cdd_clocknum);
+        copy = cdd_extract_dbm(copy, dbm, cdd_clocknum);
         copy = cdd_reduce(cdd_remove_negative(copy));
-        dbm_up(dbm, size);
-        cdd fixed_cdd = cdd(dbm, size);
+        dbm_up(dbm, cdd_clocknum);
+        cdd fixed_cdd = cdd(dbm, cdd_clocknum);
         fixed_cdd &= bottom;
         res |= fixed_cdd;
     }
     return res;
 }
 
+/**
+ * Construct a cdd from a federation.
+ * @param fed a federation
+ * @return the cdd representing \a fed.
+ */
+cdd cdd_from_fed(const dbm::fed_t& fed)
+{
+    dbm::fed_t copy = dbm::fed_t(fed);
+    cdd res = cdd_false();
+    for (auto& zone : fed) {
+        res |= cdd(zone.const_dbm(), cdd_clocknum);
+    }
+    return res;
+}
+
+/**
+ * Get the timed predecessor of the given (bad) target dbm and target bdd that cannot be
+ * saved (i.e. reached) by delaying into \a safe.
+ *
+ * <p>If there is an overlap between \a target and \a safe, the overlap is considered
+ * to be saved.</p>
+ * @param dbm_target the target dbm
+ * @param bdd_target the target bdd
+ * @param safe the safe cdd
+ * @return a cdd containing states that can delay into \a target without reaching \a safe.
+ */
+cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe)
+{
+    cdd result = cdd_false();
+
+    // Check whether the safe has an overlapping BDD part with the target.
+    cdd good_part_with_fitting_bools = bdd_target & safe;
+    if (good_part_with_fitting_bools != cdd_false()) {
+        // For each possible combination of boolean valuations,
+        // compute the part of safe that overlaps with it.
+        for (auto i = 0u; i < (1u << cdd_varnum); ++i) {
+            cdd all_booleans = cdd_true();
+            for (auto j = 0u; j < cdd_varnum; ++j) {
+                bool current = (i & 1 << j) != 0;
+                if (current) {
+                    all_booleans &= cdd_bddvarpp(bdd_start_level + j);
+                } else {
+                    all_booleans &= cdd_bddnvarpp(bdd_start_level + j);
+                }
+            }
+
+            // No need to test combinations that don't satisfy the bad part.
+            if (cdd_equiv(all_booleans & bdd_target, cdd_false())) {
+                continue;
+            }
+
+            // Paranoia check.
+            assert(!cdd_eval_false(all_booleans & bdd_target));
+
+            auto bad_fed = dbm::fed_t{dbm_target, (uint32_t)cdd_clocknum};
+            ADBM(dbm_good, cdd_clocknum);
+            cdd good_copy = good_part_with_fitting_bools & all_booleans;
+
+            if (!cdd_eval_false(good_copy)) {
+                auto good_fed = dbm::fed_t{(uint32_t)cdd_clocknum};
+                while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) {
+                    extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy);
+                    good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part));
+                    free(dbm_good);
+                    dbm_good = res_good.dbm;
+                    cdd bdd_good = res_good.BDD_part;
+                    good_fed.add(dbm_good, cdd_clocknum);
+                }
+
+                // If good_fed is empty, good_copy did not contain any DBM. This has the interpretation
+                // of an unbounded DBM.
+                if (good_fed.isEmpty()) {
+                    dbm_init(dbm_good, cdd_clocknum);
+                    good_fed.add(dbm_good, cdd_clocknum);
+                }
+
+                auto pred_fed = bad_fed.predt(good_fed);
+                result |= cdd_from_fed(pred_fed) & all_booleans;
+
+            } else {
+                // For all boolean valuations we did not reach with our safe CDD, we take the past of the
+                // current target DBM.
+                ADBM(local, cdd_clocknum);
+                dbm_copy(local, dbm_target, cdd_clocknum);
+                dbm_down(local, cdd_clocknum);
+                cdd past = cdd(local, cdd_clocknum) & all_booleans;
+                result |= past;
+                free(local);
+            }
+            free(dbm_good);
+        }
+
+    } else {
+        // Safe does not have an overlapping part with the target BDD.
+        // So the complete past of this DBM is bad.
+        dbm_down(dbm_target, cdd_clocknum);
+        cdd past = cdd(dbm_target, cdd_clocknum) & bdd_target;
+        result |= past;
+    }
+
+    return result;
+}
+
+/**
+ * Get the timed predecessor of the given (bad) \a target state that cannot be
+ * saved (i.e. reached) by delaying into \a safe.
+ *
+ * <p>If there is an overlap between \a target and \a safe, the overlap is considered
+ * to be saved.</p>
+ * @param target the target cdd
+ * @param safe the safe cdd
+ * @return a cdd containing states that can delay into \a target without reaching \a safe.
+ */
+cdd cdd_predt(const cdd& target, const cdd& safe)
+{
+    // First some trivial cases.
+    if (target == cdd_false())
+        return target;
+    if (safe == cdd_true())
+        return cdd_false();
+
+    cdd allThatKillsUs = cdd_false();
+    cdd copy = target;
+    ADBM(dbm_target, cdd_clocknum);
+
+    if (cdd_isterminal(target.handle()) || cdd_info(target.handle())->type == TYPE_BDD) {
+        dbm_init(dbm_target, cdd_clocknum);
+        cdd result = cdd_predt_dbm(dbm_target, target, safe);
+        free(dbm_target);
+        return result;
+    }
+
+    // Split target into DBMs.
+    while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) {
+        extraction_result res = cdd_extract_bdd_and_dbm(copy);
+        copy = cdd_reduce(cdd_remove_negative(res.CDD_part));
+        free(dbm_target);
+        dbm_target = res.dbm;
+        cdd bdd_target = res.BDD_part;
+
+        allThatKillsUs |= cdd_predt_dbm(dbm_target, bdd_target, safe);
+    }
+    free(dbm_target);
+    return allThatKillsUs;
+}
+
 /**
  * Perform the delay operation on a CDD taking an invariant into account.
  *
@@ -142,21 +291,22 @@ cdd cdd_delay_invariant(const cdd& state, const cdd& invar)
  */
 cdd cdd_past(const cdd& state)
 {
-    if (cdd_isterminal(state.root))
+    // First some trivial cases.
+    if (cdd_isterminal(state.handle()))
         return state;
-    if (cdd_info(state.root)->type == TYPE_BDD)
+    if (cdd_info(state.handle())->type == TYPE_BDD)
         return state;
-    uint32_t size = cdd_clocknum;
+
     cdd copy = state;
     cdd res = cdd_false();
-    ADBM(dbm);
+    ADBM(dbm, cdd_clocknum);
     while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) {
         copy = cdd_reduce(copy);
-        cdd bottom = cdd_extract_bdd(copy, size);
-        copy = cdd_extract_dbm(copy, dbm, size);
+        cdd bottom = cdd_extract_bdd(copy, cdd_clocknum);
+        copy = cdd_extract_dbm(copy, dbm, cdd_clocknum);
         copy = cdd_reduce(cdd_remove_negative(copy));
-        dbm_down(dbm, size);
-        res |= (cdd(dbm, size) & bottom);
+        dbm_down(dbm, cdd_clocknum);
+        res |= (cdd(dbm, cdd_clocknum) & bottom);
     }
     return res;
 }
@@ -182,7 +332,7 @@ cdd cdd_apply_reset(const cdd& state, int32_t* clock_resets, int32_t* clock_valu
 
     // Apply bool resets.
     if (num_bool_resets > 0)
-        copy = cdd_exist(copy, bool_resets, NULL, num_bool_resets, 0);
+        copy = cdd_exist(copy, bool_resets, nullptr, num_bool_resets, 0);
 
     for (int i = 0; i < num_bool_resets; i++) {
         if (bool_values[i] == 1) {
@@ -196,14 +346,14 @@ cdd cdd_apply_reset(const cdd& state, int32_t* clock_resets, int32_t* clock_valu
     // Special cases when we are already done.
     if (num_clock_resets == 0)
         return copy;
-    if (cdd_isterminal(copy.root))
+    if (cdd_isterminal(copy.handle()))
         return copy;
-    if (cdd_info(copy.root)->type == TYPE_BDD)
+    if (cdd_info(copy.handle())->type == TYPE_BDD)
         return copy;
 
     // Apply the clock resets.
     cdd res = cdd_false();
-    while (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type != TYPE_BDD) {
+    while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) {
         copy = cdd_reduce(copy);
         extraction_result exres = cdd_extract_bdd_and_dbm(copy);
         cdd bottom = exres.BDD_part;
@@ -271,18 +421,18 @@ cdd cdd_transition_back(const cdd& state, const cdd& guard, const cdd& update, i
 
     // Apply bool resets.
     if (num_bool_resets > 0)
-        copy = cdd_exist(copy, bool_resets, NULL, num_bool_resets, 0);
+        copy = cdd_exist(copy, bool_resets, nullptr, num_bool_resets, 0);
 
     // Special cases when we are already done.
     if (num_clock_resets == 0)
         return copy & guard;
-    if (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type == TYPE_BDD)
+    if (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type == TYPE_BDD)
         return copy & guard;
 
     // Apply the clock resets.
     cdd res = cdd_false();
     copy = cdd_remove_negative(copy);
-    while (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type != TYPE_BDD) {
+    while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) {
         copy = cdd_reduce(copy);
         extraction_result exres = cdd_extract_bdd_and_dbm(copy);
         cdd bottom = exres.BDD_part;
diff --git a/test/test_cdd.cpp b/test/test_cdd.cpp
index 13e744d..00306b8 100644
--- a/test/test_cdd.cpp
+++ b/test/test_cdd.cpp
@@ -772,6 +772,54 @@ void test_transition_back_past(size_t size)
                                     num_bools)) == cdd_false());
 }
 
+void test_predt(size_t size)
+{
+    // First some trivial cases.
+    REQUIRE(cdd_equiv(cdd_predt(cdd_true(), cdd_true()), cdd_false()));
+    REQUIRE(cdd_equiv(cdd_predt(cdd_true(), cdd_false()), cdd_remove_negative(cdd_true())));
+    REQUIRE(cdd_equiv(cdd_predt(cdd_false(), cdd_true()), cdd_false()));
+    REQUIRE(cdd_equiv(cdd_predt(cdd_false(), cdd_false()), cdd_false()));
+
+    // Create a CDD containing random DBMs.
+    cdd cdd_part;
+    auto dbm = dbm_wrap{size};
+    int n_dbms = 8;
+
+    for (uint32_t i = 0; i < n_dbms; i++) {
+        dbm.generate();
+        cdd_part |= cdd(dbm.raw(), dbm.size());
+    }
+
+    // Create a random BDD.
+    cdd bdd_part = generate_bdd(size);
+    cdd cdd1 = cdd_part & bdd_part;
+
+    // First some checks when nothing can save us.
+    // cdd_part \subset cdd_predt(cdd_part) <==> cdd_part & !cdd_predt(cdd_part) == false
+    REQUIRE((!cdd_predt(cdd_part, cdd_false()) & cdd_remove_negative(cdd_part)) == cdd_false());
+    // cdd_predt(cdd_part) \subset cdd_past(cdd_part) <==> cdd_predt(cdd_part) & !cdd_past(cdd_part) == false
+    REQUIRE((!cdd_past(cdd_part) & cdd_predt(cdd_part, cdd_false())) == cdd_false());
+    REQUIRE(cdd_equiv(cdd_predt(bdd_part, cdd_false()), cdd_remove_negative(bdd_part)));
+    // cdd_predt(cdd1) \subset cdd_past(cdd1) <==> cdd_predt(cdd1) & !cdd_past(cdd1) == false
+    REQUIRE((!cdd_past(cdd1) & cdd_predt(cdd1, cdd_false())) == cdd_false());
+    REQUIRE(cdd_equiv(cdd_predt(cdd1, cdd_true()), cdd_false()));
+
+    // Check timed predecessor for random, but non-overlapping safe cdd.
+    if (size == 0)
+        return;
+    cdd b1 = cdd_bddvarpp(bdd_start_level);
+    cdd cdd2_part;
+    for (uint32_t i = 0; i < n_dbms; i++) {
+        dbm.generate();
+        cdd_part |= cdd(dbm.raw(), dbm.size());
+    }
+
+    cdd left = cdd_part & b1;
+    cdd right = cdd2_part & !b1;
+    cdd test = left | right;
+    REQUIRE(cdd_equiv(cdd_predt(test, right), cdd_remove_negative(cdd_past(left))));
+}
+
 static void test(const char* name, TestFunction f, size_t size)
 {
     cout << name << " size = " << size << endl;
@@ -809,6 +857,7 @@ static void big_test(uint32_t n)
             test("test_transition  ", test_transition, i);
             test("test_transition_back", test_transition_back, i);
             test("test_transition_back_past", test_transition_back_past, i);
+            test("test_predt       ", test_predt, i);
         }
         test("test_remove_negative", test_remove_negative, n);
         passDBMs = dbm_wrap::get_allDBMs() - DBM_sofar;
@@ -837,6 +886,55 @@ TEST_CASE("CDD intersection with size 3")
     cdd_done();
 }
 
+TEST_CASE("CDD timed predecessor static test")
+{
+    cdd_init(100000, 10000, 10000);
+    cdd_add_clocks(4);
+    cdd_add_bddvar(3);
+
+    cdd b6 = cdd_bddvarpp(bdd_start_level + 0);
+    cdd b7 = cdd_bddvarpp(bdd_start_level + 1);
+    cdd b8 = cdd_bddvarpp(bdd_start_level + 2);
+
+    // Create input cdd.
+    cdd input = cdd_intervalpp(1, 0, 6, 10);
+    input &= cdd_intervalpp(2, 0, 5, dbm_LS_INFINITY);
+    input &= cdd_intervalpp(3, 0, 8, dbm_LS_INFINITY);
+    input &= b6;
+    cdd_reduce(input);
+
+    // Create safe cdd, which will be safe1 | safe2.
+    cdd safe1 = cdd_intervalpp(1, 0, 0, 4);
+    safe1 &= cdd_intervalpp(2, 0, 0, dbm_LS_INFINITY);
+    safe1 &= cdd_intervalpp(3, 0, 0, dbm_LS_INFINITY);
+    safe1 &= b7;
+
+    cdd safe2 = cdd_intervalpp(1, 0, 7, 9);
+    safe2 &= cdd_intervalpp(2, 0, 0, 4);
+    safe2 &= cdd_intervalpp(3, 0, 0, 3);
+    safe2 &= b8;
+    cdd safe = safe1 | safe2;
+    cdd_reduce(safe);
+
+    // Perform the timed predecessor operator and remove any negative clock values.
+    cdd result = cdd_remove_negative(cdd_predt(input, safe));
+
+    // Create the expected cdd.
+    cdd expected1 = cdd_intervalpp(1, 0, 0, 4);
+    expected1 &= cdd_intervalpp(2, 1, -5, dbm_LS_INFINITY);
+    expected1 &= cdd_intervalpp(3, 1, -1, dbm_LS_INFINITY);
+    expected1 &= b6;
+    expected1 &= !b7;
+    cdd expected2 = cdd_intervalpp(1, 0, 4, 10);
+    expected2 &= cdd_intervalpp(2, 1, -5, dbm_LS_INFINITY);
+    expected2 &= cdd_intervalpp(3, 1, -1, dbm_LS_INFINITY);
+    expected2 &= b6;
+    cdd expected = cdd_remove_negative(expected1 | expected2);
+
+    // Check whether the result matches the expected one.
+    REQUIRE(cdd_equiv(result, expected));
+}
+
 // TODO: the bellow test case passes only on 32-bit, need to fix it
 #if INTPTR_MAX == INT32_MAX
 TEST_CASE("CDD reduce with size 3")