diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh
index b5d2cfaf9..d5fd7c630 100644
--- a/include/mata/nft/nft.hh
+++ b/include/mata/nft/nft.hh
@@ -134,13 +134,21 @@ public:
     // TODO: When there is a need for state dictionary, consider creating default library implementation of state
     //  dictionary in the attributes.
 
+    /**
+     * @brief If each level has its own alphabet. alphabets[i] (or rather alphabets->operator[](i)) contains a pointer to the alphabet of level i.
+     *
+     * Each Alphabet can be shared among multiple levels and NFTs. If all levels share the same alphabet, assign std::nullopt here and use alphabet member instead.
+     */
+    std::optional<std::vector<Alphabet*>> alphabets = std::nullopt;
+
 public:
     explicit Nft(
             Delta delta = {}, utils::SparseSet<State> initial_states = {},
             utils::SparseSet<State> final_states = {}, Levels levels = {},
-            Alphabet* alphabet = nullptr)
+            Alphabet* alphabet = nullptr, std::optional<std::vector<Alphabet*>> alphabets = std::nullopt)
         : Nfa{ std::move(delta), std::move(initial_states), std::move(final_states), alphabet },
-          levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) } {}
+          levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) },
+          alphabets{alphabets} {}
 
     /**
      * @brief Construct a new explicit NFT with num_of_states states and optionally set initial and final states.
@@ -153,32 +161,32 @@ public:
      */
     explicit Nft(const size_t num_of_states, utils::SparseSet<State> initial_states = {},
                  utils::SparseSet<State> final_states = {}, Levels levels = {},
-                 Alphabet* alphabet = nullptr)
+                 Alphabet* alphabet = nullptr, std::optional<std::vector<Alphabet*>> alphabets = std::nullopt)
         : Nfa{ num_of_states, std::move(initial_states), std::move(final_states), alphabet },
-          levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) } {}
+          levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) }, alphabets{alphabets} {}
 
     static Nft with_levels(
             Levels levels, const size_t num_of_states = 0, utils::SparseSet<State> initial_states = {},
-            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr) {
-        return Nft{ num_of_states, std::move(initial_states), std::move(final_states), std::move(levels), alphabet };
+            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr, std::optional<std::vector<Alphabet*>> alphabets = std::nullopt) {
+        return Nft{ num_of_states, std::move(initial_states), std::move(final_states), std::move(levels), alphabet, alphabets };
     }
 
     static Nft with_levels(
             Levels levels, Delta delta, utils::SparseSet<State> initial_states = {},
-            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr) {
-        return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), std::move(levels), alphabet };
+            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr, std::optional<std::vector<Alphabet*>> alphabets = std::nullopt) {
+        return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), std::move(levels), alphabet, alphabets };
     }
 
     static Nft with_levels(
             const size_t num_of_levels, const size_t num_of_states = 0, utils::SparseSet<State> initial_states = {},
-            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr) {
-        return Nft{ num_of_states, std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet };
+            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr, std::optional<std::vector<Alphabet*>> alphabets = std::nullopt) {
+        return Nft{ num_of_states, std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet, alphabets };
     }
 
     static Nft with_levels(
             const size_t num_of_levels, Delta delta, utils::SparseSet<State> initial_states = {},
-            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr) {
-        return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet };
+            utils::SparseSet<State> final_states = {}, Alphabet* alphabet = nullptr, std::optional<std::vector<Alphabet*>> alphabets = std::nullopt) {
+        return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet, alphabets };
     }
 
     /**
diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc
index 96b869807..8bf492550 100644
--- a/src/nfa/operations.cc
+++ b/src/nfa/operations.cc
@@ -438,6 +438,7 @@ Nfa mata::nfa::simple_revert(const Nfa& aut) {
 
     result.initial = aut.final;
     result.final = aut.initial;
+    result.alphabet = aut.alphabet;
 
     return result;
 }
@@ -1033,6 +1034,8 @@ Nfa mata::nfa::algorithms::minimize_hopcroft(const Nfa& dfa_trimmed) {
         }
     }
 
+    result.alphabet = dfa_trimmed.alphabet;
+
     return result;
 }
 
@@ -1199,6 +1202,7 @@ Nfa mata::nfa::determinize(
                 && !(*macrostate_discover)(result, target_res, targets_orig)) { return result; }
         }
     }
+    result.alphabet = aut.alphabet;
     return result;
 }
 
diff --git a/src/nfa/product.cc b/src/nfa/product.cc
index a688bf7de..010601050 100644
--- a/src/nfa/product.cc
+++ b/src/nfa/product.cc
@@ -161,6 +161,7 @@ Nfa mata::nfa::algorithms::product(
             }
         }
     }
+    product.alphabet = lhs.alphabet; // TODO is this the best choice?
     return product;
 } // intersection().
 
diff --git a/src/nft/builder.cc b/src/nft/builder.cc
index 10085e9b3..7573bd30f 100644
--- a/src/nft/builder.cc
+++ b/src/nft/builder.cc
@@ -286,7 +286,7 @@ Nft builder::from_nfa_with_levels_zero(
     }
 
     const size_t nfa_num_of_states{ nfa.num_of_states() };
-    Nft nft{ Nft::with_levels(num_of_levels, nfa_num_of_states, nfa.initial, nfa.final) };
+    Nft nft{ Nft::with_levels(num_of_levels, nfa_num_of_states, nfa.initial, nfa.final, nfa.alphabet) };
 
     for(State src{ 0 }; src < nfa_num_of_states; ++src) {
         for (const SymbolPost& symbol_post: nfa.delta[src]) {
diff --git a/src/nft/intersection.cc b/src/nft/intersection.cc
index b9a49b693..807fec8d8 100644
--- a/src/nft/intersection.cc
+++ b/src/nft/intersection.cc
@@ -248,6 +248,9 @@ Nft mata::nft::algorithms::product(
             }
         }
     }
+    // TODO is the following the best idea?
+    product.alphabet = lhs.alphabet;
+    product.alphabets = lhs.alphabets;
     return product;
 } // intersection().
 } // namespace mata::nft.
diff --git a/src/nft/nft.cc b/src/nft/nft.cc
index c43dfc7cb..5827c84d2 100644
--- a/src/nft/nft.cc
+++ b/src/nft/nft.cc
@@ -212,6 +212,18 @@ void Nft::print_to_dot(
         }
     };
 
+    auto has_alphabet_at_level = [&](const Level level) -> bool {
+        return this->alphabets.has_value() && this->alphabets->operator[](level) != nullptr;
+    };
+
+    auto translate_symbol_at_level = [&](const Symbol symbol, const Level level) -> std::string {
+        if (!decode_ascii_chars && has_alphabet_at_level(level)) {
+            return this->alphabets->operator[](level)->reverse_translate_symbol(symbol);
+        } else {
+            return translate_symbol(symbol);
+        }
+    };
+
     auto vec_of_symbols_to_string = [&](const OrdVector<Symbol>& symbols) {
         std::string result;
         for (const Symbol& symbol : symbols) { result += translate_symbol(symbol) + ","; }
@@ -219,6 +231,19 @@ void Nft::print_to_dot(
         return result;
     };
 
+    auto vec_of_symbols_to_string_at_level = [&](const OrdVector<Symbol>& symbols, const Level level) {
+        if (has_alphabet_at_level(level)) {
+            std::string result;
+            for (const Symbol& symbol: symbols) {
+                result += translate_symbol_at_level(symbol, level) + ",";
+            }
+            result.pop_back(); // Remove last comma
+            return result;
+        } else {
+            return vec_of_symbols_to_string(symbols);
+        }
+    };
+
     auto vec_of_symbols_to_string_with_intervals = [&](const OrdVector<Symbol>& symbols) {
         std::string result;
 
@@ -281,7 +306,7 @@ void Nft::print_to_dot(
 
             std::string label = use_intervals
                                     ? vec_of_symbols_to_string_with_intervals(symbols)
-                                    : vec_of_symbols_to_string(symbols);
+                                    : vec_of_symbols_to_string_at_level(symbols, levels[source]);
             std::string on_hover_label = replace_all(replace_all(label, "<", "&lt;"), ">", "&gt;");
             bool is_shortened = false;
             if (max_label_length > 0 && label.length() > static_cast<size_t>(max_label_length)) {
diff --git a/src/nft/operations.cc b/src/nft/operations.cc
index 686d2e88f..2fb10369c 100644
--- a/src/nft/operations.cc
+++ b/src/nft/operations.cc
@@ -295,10 +295,16 @@ Nft mata::nft::project_out(const Nft& nft, const utils::OrdVector<Level>& levels
     // project out     x   x   x x
     // new levels    0 0 1 2 2 0 0
     std::vector<Level> new_levels(nft.levels.num_of_levels, 0);
+    std::vector<Level> old_levels {};
     Level lvl_sub{ 0 };
     for (Level lvl_old{ 0 }; lvl_old < seq_start_idx; lvl_old++) {
         new_levels[lvl_old] = static_cast<Level>(lvl_old - lvl_sub);
-        if (levels_to_project.find(lvl_old) != levels_to_project.end()) { lvl_sub++; }
+        if (levels_to_project.find(lvl_old) != levels_to_project.end()) {
+            lvl_sub++;
+        } else {
+            old_levels.push_back(lvl_old);
+            assert(old_levels[new_levels[lvl_old]] == lvl_old);
+        }
     }
 
     // cannot use multimap, because it can contain multiple occurrences of (a -> a), (a -> a)
@@ -339,6 +345,7 @@ Nft mata::nft::project_out(const Nft& nft, const utils::OrdVector<Level>& levels
 
     // Construct the automaton with projected levels.
     Nft result{ Nft::with_levels(nft.levels, Delta{}, nft.initial, nft.final, nft.alphabet) };
+
     for (State src_state{ 0 }; src_state < num_of_states_in_delta; src_state++) { // For every state.
         for (const State cls_state : closure[src_state]) { // For every state in its epsilon closure.
             if (nft.final[cls_state] && can_be_final(src_state)) result.final.insert(src_state);
@@ -373,6 +380,15 @@ Nft mata::nft::project_out(const Nft& nft, const utils::OrdVector<Level>& levels
     for (State s{ 0 }; s < result.levels.size(); s++) { result.levels[s] = new_levels[result.levels[s]]; }
     result.levels.num_of_levels = static_cast<Level>(result.levels.num_of_levels - levels_to_project.size());
 
+    if (nft.alphabets.has_value()) {
+        // retain all alphabets that are not projected out
+        std::vector<Alphabet*> alphabet_ptrs(new_levels.size(), nullptr);
+        for (size_t i{ 0 }; i < result.levels.num_of_levels; ++i) {
+            alphabet_ptrs[i] = nft.alphabets->operator[](old_levels[i]);
+        }
+        result.alphabets = std::make_optional<std::vector<Alphabet*>>(alphabet_ptrs);
+    }
+
     return result;
 }
 
@@ -1033,6 +1049,7 @@ Nft mata::nft::reduce(const Nft& aut, StateRenaming* state_renaming, const Param
 Nft nft::determinize(const Nft& nft, std::unordered_map<StateSet, State>* subset_map) {
     Nft result{ Nft::with_levels(nft.levels.num_of_levels) };
     result.alphabet = nft.alphabet;
+    result.alphabets = nft.alphabets;
     if (nft.initial.empty()) { return result; }
 
     // Assuming all sets targets are non-empty.