diff --git a/NEWS b/NEWS
index 6f910ec91..a9e60e82c 100644
--- a/NEWS
+++ b/NEWS
@@ -47,6 +47,18 @@ New in spot 2.1.2.dev (not yet released)
     to setjmp are now avoided when variable reordering is disabled
     (the default).
 
+  * The twa class has three new methods:
+      aut->intersects(other)
+      aut->intersecting_run(other)
+      aut->intersecting_word(other)
+    currently these are just convenient wrappers around
+      !otf_product(aut, other)->is_empty()
+      otf_product(aut, other)->accepting_run()->project(aut)
+      otf_product(aut, other)->accepting_word()
+    with any Fin-acceptance removal performed before the
+    product.  However the plan is that these can be implemented
+    more efficiently in the future.
+
   Bugs:
 
   * ltl2tgba was always using the highest settings for the LTL
diff --git a/doc/org/tut51.org b/doc/org/tut51.org
index 5a5517867..45ba3ebd2 100644
--- a/doc/org/tut51.org
+++ b/doc/org/tut51.org
@@ -438,21 +438,12 @@ counterexample:
       spot::formula f = spot::formula::Not(pf.f);
       spot::twa_graph_ptr af = spot::translator(d).run(f);
 
-      // Construct an "on-the-fly product"
+      // Find a run of or demo_kripke that intersects af.
       auto k = std::make_shared<demo_kripke>(d);
-      auto p = spot::otf_product(k, af);
-
-      if (auto run = p->accepting_run())
-        {
-          std::cout << "formula is violated by the following run:\n";
-          // "run" is an accepting run over the product.  Project it on
-          // the Kripke structure before displaying it.
-          std::cout << *run->project(k);
-        }
+      if (auto run = k->intersecting_run(af))
+        std::cout << "formula is violated by the following run:\n" << *run;
       else
-        {
-          std::cout << "formula is verified\n";
-        }
+        std::cout << "formula is verified\n";
    }
  #+END_SRC
 
@@ -496,38 +487,38 @@ passing the option "~k~" to =print_dot()= will fix that.
   <<demo-succ-iter-2>>
 #+END_SRC
 
- #+NAME: demo-3
- #+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
-   #include <spot/twaalgos/dot.hh>
-   #include <spot/tl/parse.hh>
-   #include <spot/twaalgos/translate.hh>
-   #include <spot/twa/twaproduct.hh>
-   #include <spot/twaalgos/emptiness.hh>
-   #include <spot/twaalgos/copy.hh>
-   <<demo-3-aux>>
-   int main()
-   {
-     auto d = spot::make_bdd_dict();
+#+NAME: demo-3
+#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
+  #include <spot/twaalgos/dot.hh>
+  #include <spot/tl/parse.hh>
+  #include <spot/twaalgos/translate.hh>
+  #include <spot/twa/twaproduct.hh>
+  #include <spot/twaalgos/emptiness.hh>
+  #include <spot/twaalgos/copy.hh>
+  <<demo-3-aux>>
+  int main()
+  {
+    auto d = spot::make_bdd_dict();
 
-     // Parse the input formula.
-     spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
-     if (pf.format_errors(std::cerr))
-       return 1;
+    // Parse the input formula.
+    spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
+    if (pf.format_errors(std::cerr))
+      return 1;
 
-     // Translate its negation.
-     spot::formula f = spot::formula::Not(pf.f);
-     spot::twa_graph_ptr af = spot::translator(d).run(f);
+    // Translate its negation.
+    spot::formula f = spot::formula::Not(pf.f);
+    spot::twa_graph_ptr af = spot::translator(d).run(f);
 
-     // Construct an "on-the-fly product"
-     auto k = spot::copy(std::make_shared<demo_kripke>(d), spot::twa::prop_set::all(), true);
-     auto p = spot::otf_product(k, af);
-
-     if (auto run = p->accepting_run())
-       {
-         run->project(k)->highlight(5); // 5 is a color number.
-         spot::print_dot(std::cout, k, ".k");
-       }
-   }
+    // Convert demo_kripke into an explicit graph
+    spot::twa_graph_ptr k = spot::copy(std::make_shared<demo_kripke>(d),
+                                       spot::twa::prop_set::all(), true);
+     // Find a run of or demo_kripke that intersects af.
+    if (auto run = k->intersecting_run(af))
+      {
+        run->highlight(5); // 5 is a color number.
+        spot::print_dot(std::cout, k, ".k");
+      }
+  }
  #+END_SRC
 
  #+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results
@@ -537,7 +528,7 @@ passing the option "~k~" to =print_dot()= will fix that.
  #+RESULTS:
  [[file:kripke-3.png]]
 
-
+1
 * Possible improvements
 
 The on-the-fly interface, especially as implemented here, involves a
diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc
index 92d29adb2..ffcd7e869 100644
--- a/spot/twa/twa.cc
+++ b/spot/twa/twa.cc
@@ -25,6 +25,7 @@
 #include <spot/twaalgos/gtec/gtec.hh>
 #include <spot/twaalgos/word.hh>
 #include <spot/twaalgos/remfin.hh>
+#include <spot/twa/twaproduct.hh>
 #include <utility>
 
 namespace spot
@@ -44,6 +45,20 @@ namespace spot
     get_dict()->unregister_all_my_variables(this);
   }
 
+
+  namespace
+  {
+    const_twa_ptr remove_fin_maybe(const const_twa_ptr& a)
+    {
+      if (!a->acc().uses_fin_acceptance())
+        return a;
+      auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
+      if (!aa)
+        aa = make_twa_graph(a, twa::prop_set::all());
+      return remove_fin(aa);
+    }
+  }
+
   state*
   twa::project_state(const state* s,
                       const const_twa_ptr& t) const
@@ -59,15 +74,7 @@ namespace spot
     // FIXME: This should be improved based on properties of the
     // automaton.  For instance we do not need couvreur99 is we know
     // the automaton is weak.
-    auto a = shared_from_this();
-    if (a->acc().uses_fin_acceptance())
-      {
-        auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
-        if (!aa)
-          aa = make_twa_graph(a, prop_set::all());
-        a = remove_fin(aa);
-      }
-    return !couvreur99(a)->check();
+    return !couvreur99(remove_fin_maybe(shared_from_this()))->check();
   }
 
   twa_run_ptr
@@ -86,15 +93,7 @@ namespace spot
   twa_word_ptr
   twa::accepting_word() const
   {
-    auto a = shared_from_this();
-    if (a->acc().uses_fin_acceptance())
-      {
-        auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
-        if (!aa)
-          aa = make_twa_graph(a, prop_set::all());
-        a = remove_fin(aa);
-      }
-    if (auto run = a->accepting_run())
+    if (auto run = remove_fin_maybe(shared_from_this())->accepting_run())
       {
         auto w = make_twa_word(run->reduce());
         w->simplify();
@@ -106,6 +105,36 @@ namespace spot
       }
   }
 
+  bool
+  twa::intersects(const_twa_ptr other) const
+  {
+    auto a1 = remove_fin_maybe(shared_from_this());
+    auto a2 = remove_fin_maybe(other);
+    return !otf_product(a1, a2)->is_empty();
+  }
+
+  twa_run_ptr
+  twa::intersecting_run(const_twa_ptr other, bool from_other) const
+  {
+    auto a = shared_from_this();
+    if (from_other)
+      other = remove_fin_maybe(other);
+    else
+      a = remove_fin_maybe(a);
+    auto run = otf_product(a, other)->accepting_run();
+    if (!run)
+      return nullptr;
+    return run->project(from_other ? other : a);
+  }
+
+  twa_word_ptr
+  twa::intersecting_word(const_twa_ptr other) const
+  {
+    auto a1 = remove_fin_maybe(shared_from_this());
+    auto a2 = remove_fin_maybe(other);
+    return otf_product(a1, a2)->accepting_word();
+  }
+
   void
   twa::set_named_prop(std::string s, std::nullptr_t)
   {
diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh
index ed3b8deb6..4ec67956e 100644
--- a/spot/twa/twa.hh
+++ b/spot/twa/twa.hh
@@ -824,17 +824,23 @@ namespace spot
     ///@}
 
     /// \brief Check whether the language of the automaton is empty.
+    ///
+    /// If you are calling this method on a product of two automata,
+    /// consider using intersects() instead.
     virtual bool is_empty() const;
 
     /// \brief Return an accepting run if one exists.
     ///
-    /// Note that this method currently onky works for Fin-less
+    /// Note that this method currently only works for Fin-less
     /// acceptance.  For acceptance conditions that contain Fin
     /// acceptance, you can either rely on is_empty() and not use any
     /// accepting run, or remove Fin acceptance using remove_fin() and
     /// compute an accepting run on that larger automaton.
     ///
     /// Return nullptr if no accepting run were found.
+    ///
+    /// If you are calling this method on a product of two automata,
+    /// consider using intersecting_run() instead.
     virtual twa_run_ptr accepting_run() const;
 
     /// \brief Return an accepting word if one exists.
@@ -843,8 +849,44 @@ namespace spot
     /// acceptance.
     ///
     /// Return nullptr if no accepting word were found.
+    ///
+    /// If you are calling this method on a product of two automata,
+    /// consider using intersecting_word() instead.
     virtual twa_word_ptr accepting_word() const;
 
+    /// \brief Check whether the language of this automaton intersects
+    /// that of the \a other automaton.
+    virtual bool intersects(const_twa_ptr other) const;
+
+    /// \brief Return an accepting run recognizing a word accepted by
+    /// two automata.
+    ///
+    /// If \a from_other is true, the returned run will be over the
+    /// \a other automaton.  Otherwise, the run will be over this
+    /// automaton.
+    ///
+    /// Note that this method currently only works if the automaton
+    /// from which the accepting run is extracted uses Fin-less acceptance.
+    /// (The other automaton can have any acceptance condition.)
+    ///
+    /// For acceptance conditions that contain Fin acceptance, you can
+    /// either rely on intersects() and not use any accepting run, or
+    /// remove Fin acceptance using remove_fin() and compute an
+    /// intersecting run on this larger automaton.
+    ///
+    /// Return nullptr if no accepting run were found.
+    virtual twa_run_ptr intersecting_run(const_twa_ptr other,
+                                         bool from_other = false) const;
+
+
+    /// \brief Return a word accepted by two automata.
+    ///
+    /// Note that this method DOES works with Fin
+    /// acceptance.
+    ///
+    /// Return nullptr if no accepting word were found.
+    virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;
+
   private:
     acc_cond acc_;
 
diff --git a/tests/python/bugdet.py b/tests/python/bugdet.py
index ca619cdc4..ea159ecc3 100644
--- a/tests/python/bugdet.py
+++ b/tests/python/bugdet.py
@@ -82,10 +82,10 @@ print("use_simulation=True")
 b1 = spot.tgba_determinize(b, False, True, True, True)
 assert b1.num_states() == 5
 b1 = spot.remove_fin(spot.dtwa_complement(b1))
-assert spot.otf_product(a, b1).is_empty() == True
+assert not a.intersects(b1);
 
 print("\nuse_simulation=False")
 b2 = spot.tgba_determinize(b, False, True, False, True)
 assert b2.num_states() == 5
 b2 = spot.remove_fin(spot.dtwa_complement(b2))
-assert spot.otf_product(a, b1).is_empty() == True
+assert not a.intersects(b1);