diff --git a/README.md b/README.md
index 1e2e21e..a72dff9 100644
--- a/README.md
+++ b/README.md
@@ -163,7 +163,7 @@ at: [paultristanwagner@gmail.com](mailto:paultristanwagner@gmail.com).
 
 - Improve UI / UX
 - Implement implication and equivalence operators in LTL, CTL, and CTL* grammar
-- Implement bisimulation quotienting algorithm 
+- Implement bisimulation quotienting algorithm
 - Write tests for the LTL, CTL, and CTL* model checking algorithms
 - Optimize the lookup of the next states in the transition system
 - Implement linear-time fixpoint computation in CTL model checking
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
index 7804886..31c2900 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
@@ -1,27 +1,26 @@
 package me.paultristanwagner.modelchecking.automaton;
 
+import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON;
 import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
 
-import com.google.gson.Gson;
-import com.google.gson.GsonBuilder;
+import java.lang.reflect.Type;
 import java.util.HashSet;
 import java.util.Set;
 
-public final class GNBA {
+public class GNBA<ActionType> {
 
-  private static final Gson GSON;
   private final Set<String> states;
   private final Set<String> alphabet;
   private final Set<String> initialStates;
   private final Set<Set<String>> acceptingSets;
-  private final Set<NBATransition> transitions;
+  private final Set<NBATransition<ActionType>> transitions;
 
   public GNBA(
       Set<String> states,
       Set<String> alphabet,
       Set<String> initialStates,
       Set<Set<String>> acceptingSets,
-      Set<NBATransition> transitions) {
+      Set<NBATransition<ActionType>> transitions) {
     this.states = states;
     this.alphabet = alphabet;
     this.initialStates = initialStates;
@@ -29,17 +28,9 @@ public GNBA(
     this.transitions = transitions;
   }
 
-  static {
-    GSON =
-        new GsonBuilder()
-            .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
-            .setPrettyPrinting()
-            .create();
-  }
-
   public Set<String> getSuccessors(String state) {
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (transition.getFrom().equals(state)) {
         successors.add(transition.getTo());
       }
@@ -49,7 +40,7 @@ public Set<String> getSuccessors(String state) {
 
   public Set<String> getSuccessors(String state, String action) {
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (transition.getFrom().equals(state) && transition.getAction().equals(action)) {
         successors.add(transition.getTo());
       }
@@ -57,12 +48,12 @@ public Set<String> getSuccessors(String state, String action) {
     return successors;
   }
 
-  public NBA convertToNBA() {
+  public NBA<ActionType> convertToNBA() {
     if (acceptingSets.size() <= 1) {
       return getCanonicalNBA();
     }
 
-    NBABuilder builder = new NBABuilder();
+    NBABuilder<ActionType> builder = new NBABuilder<>();
     builder.setAlphabet(alphabet);
 
     for (String state : states) {
@@ -85,7 +76,7 @@ public NBA convertToNBA() {
       }
     }
 
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       int i = 0;
       for (Set<String> acceptingSet : acceptingSets) {
         String nbaFrom = stringTuple(transition.getFrom(), i + 1);
@@ -104,12 +95,12 @@ public NBA convertToNBA() {
     return builder.build();
   }
 
-  private NBA getCanonicalNBA() {
+  private NBA<ActionType> getCanonicalNBA() {
     if (acceptingSets.size() > 1) {
       throw new IllegalStateException("GNBA has more than one accepting set");
     }
 
-    NBABuilder builder = new NBABuilder();
+    NBABuilder<ActionType> builder = new NBABuilder<>();
     builder.setAlphabet(alphabet);
     for (String state : states) {
       builder.addState(state);
@@ -129,7 +120,7 @@ private NBA getCanonicalNBA() {
       }
     }
 
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       builder.addTransition(transition.getFrom(), transition.getAction(), transition.getTo());
     }
 
@@ -140,8 +131,8 @@ public String toJson() {
     return GSON.toJson(this);
   }
 
-  public static GNBA fromJson(String json) {
-    return GSON.fromJson(json, GNBA.class);
+  public static <ActionType> GNBA<ActionType> fromJson(String json, Type type) {
+    return GSON.fromJson(json, type);
   }
 
   public Set<String> getStates() {
@@ -160,7 +151,7 @@ public Set<Set<String>> getAcceptingSets() {
     return acceptingSets;
   }
 
-  public Set<NBATransition> getTransitions() {
+  public Set<NBATransition<ActionType>> getTransitions() {
     return transitions;
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
index 76ab9d9..3417c9e 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
@@ -3,13 +3,13 @@
 import java.util.HashSet;
 import java.util.Set;
 
-public class GNBABuilder {
+public class GNBABuilder<ActionType> {
 
   private final Set<String> states;
   private final Set<String> alphabet;
   private final Set<String> initialStates;
   private final Set<Set<String>> acceptingSets;
-  private final Set<NBATransition> transitions;
+  private final Set<NBATransition<ActionType>> transitions;
 
   public GNBABuilder() {
     this.states = new HashSet<>();
@@ -19,7 +19,7 @@ public GNBABuilder() {
     this.transitions = new HashSet<>();
   }
 
-  public GNBABuilder addStates(String... states) {
+  public GNBABuilder<ActionType> addStates(String... states) {
     for (String state : states) {
       addState(state);
     }
@@ -27,33 +27,33 @@ public GNBABuilder addStates(String... states) {
     return this;
   }
 
-  public GNBABuilder addState(String state) {
+  public GNBABuilder<ActionType> addState(String state) {
     this.states.add(state);
     return this;
   }
 
-  public GNBABuilder setAlphabet(Set<String> alphabet) {
+  public GNBABuilder<ActionType> setAlphabet(Set<String> alphabet) {
     this.alphabet.clear();
     this.alphabet.addAll(alphabet);
     return this;
   }
 
-  public GNBABuilder addInitialState(String initialState) {
+  public GNBABuilder<ActionType> addInitialState(String initialState) {
     this.initialStates.add(initialState);
     return this;
   }
 
-  public GNBABuilder addAcceptingSet(Set<String> acceptingSet) {
+  public GNBABuilder<ActionType> addAcceptingSet(Set<String> acceptingSet) {
     this.acceptingSets.add(new HashSet<>(acceptingSet));
     return this;
   }
 
-  public GNBABuilder addTransition(String from, String action, String to) {
+  public GNBABuilder<ActionType> addTransition(String from, ActionType action, String to) {
     this.transitions.add(NBATransition.of(from, action, to));
     return this;
   }
 
-  public GNBA build() {
-    return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
+  public GNBA<ActionType> build() {
+    return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitions);
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
index c41b514..6deb664 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
@@ -1,72 +1,89 @@
 package me.paultristanwagner.modelchecking.automaton;
 
+import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON;
+import static me.paultristanwagner.modelchecking.util.Pair.pair;
 import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
 
-import com.google.gson.Gson;
-import com.google.gson.GsonBuilder;
+import java.lang.reflect.Type;
 import java.util.*;
-import me.paultristanwagner.modelchecking.ts.CyclePath;
 
-public class NBA {
+import com.google.gson.annotations.SerializedName;
+import me.paultristanwagner.modelchecking.ts.CyclePath;
+import me.paultristanwagner.modelchecking.util.Pair;
 
-  private static final Gson GSON;
-
-  static {
-    GSON =
-        new GsonBuilder()
-            .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
-            .setPrettyPrinting()
-            .create();
-  }
+public class NBA<ActionType> {
 
   private final Set<String> states;
   private final Set<String> alphabet;
   private final Set<String> initialStates;
   private final Set<String> acceptingStates;
-  private final Set<NBATransition> transitions;
+  private final Set<NBATransition<ActionType>> transitions;
+
+  private final transient Map<String, Set<String>> successorCache;
+  private final transient Map<Pair<String, ActionType>, Set<String>> successorActionCache;
+
+  private NBA() {
+    this.states = new HashSet<>();
+    this.alphabet = new HashSet<>();
+    this.initialStates = new HashSet<>();
+    this.acceptingStates = new HashSet<>();
+    this.transitions = new HashSet<>();
+
+    this.successorCache = new HashMap<>();
+    this.successorActionCache = new HashMap<>();
+  }
 
   public NBA(
       Set<String> states,
       Set<String> alphabet,
       Set<String> initialStates,
       Set<String> acceptingStates,
-      Set<NBATransition> transitions) {
+      Set<NBATransition<ActionType>> transitions) {
     this.states = states;
     this.alphabet = alphabet;
     this.initialStates = initialStates;
     this.acceptingStates = acceptingStates;
     this.transitions = transitions;
+
+    this.successorCache = new HashMap<>();
+    this.successorActionCache = new HashMap<>();
   }
 
   public Set<String> getSuccessors(String state) {
+    if(successorCache.containsKey(state)) {
+      return successorCache.get(state);
+    }
+
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (transition.getFrom().equals(state)) {
         successors.add(transition.getTo());
       }
     }
+
+    successorCache.put(state, successors);
+
     return successors;
   }
 
-  public Set<String> getSuccessors(String state, String action) {
+  public Set<String> getSuccessors(String state, ActionType action) {
+    if(successorActionCache.containsKey(pair(state, action))) {
+      return successorActionCache.get(pair(state, action));
+    }
+
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (!transition.getFrom().equals(state)) {
         continue;
       }
 
-      // todo: make this more efficient
-      String a = transition.getAction();
-      String b = action;
-      Set<String> left = new HashSet<>(Arrays.asList(a.substring(1, a.length() - 1).split(", ")));
-      Set<String> right = new HashSet<>(Arrays.asList(b.substring(1, b.length() - 1).split(", ")));
-
-      boolean actionMatches = left.equals(right);
-
-      if (actionMatches) {
+      if (transition.getAction().equals(action)) {
         successors.add(transition.getTo());
       }
     }
+
+    successorActionCache.put(pair(state, action), successors);
+
     return successors;
   }
 
@@ -137,20 +154,20 @@ public NBAEmptinessResult checkEmptiness() {
     return NBAEmptinessResult.empty();
   }
 
-  public GNBA toGNBA() {
+  public GNBA<ActionType> toGNBA() {
     Set<String> states = new HashSet<>(this.states);
     Set<String> alphabet = new HashSet<>(this.alphabet);
     Set<String> initialStates = new HashSet<>(this.initialStates);
-    Set<NBATransition> transitions = new HashSet<>(this.transitions);
+    Set<NBATransition<ActionType>> transitions = new HashSet<>(this.transitions);
 
     Set<Set<String>> acceptingSets = new HashSet<>();
     acceptingSets.add(new HashSet<>(this.acceptingStates));
 
-    return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
+    return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitions);
   }
 
-  public GNBA product(NBA other) {
-    GNBABuilder builder = new GNBABuilder();
+  public GNBA<ActionType> product(NBA<ActionType> other) {
+    GNBABuilder<ActionType> builder = new GNBABuilder<>();
     builder.setAlphabet(alphabet);
 
     for (String state1 : states) {
@@ -167,8 +184,8 @@ public GNBA product(NBA other) {
       }
     }
 
-    for (NBATransition transition : transitions) {
-      for (NBATransition otherTransition : other.transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
+      for (NBATransition<ActionType> otherTransition : other.transitions) {
         if (!transition.getAction().equals(otherTransition.getAction())) {
           continue;
         }
@@ -205,8 +222,8 @@ public String toJson() {
     return GSON.toJson(this);
   }
 
-  public static NBA fromJson(String json) {
-    return GSON.fromJson(json, NBA.class);
+  public static <ActionType> NBA<ActionType> fromJson(String json, Type type) {
+    return GSON.fromJson(json, type);
   }
 
   public Set<String> getStates() {
@@ -225,7 +242,7 @@ public Set<String> getAcceptingStates() {
     return acceptingStates;
   }
 
-  public Set<NBATransition> getTransitions() {
+  public Set<NBATransition<ActionType>> getTransitions() {
     return transitions;
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java
index 640d9d4..eae38a5 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java
@@ -3,13 +3,13 @@
 import java.util.HashSet;
 import java.util.Set;
 
-public class NBABuilder {
+public class NBABuilder<ActionType> {
 
   private final Set<String> states;
   private final Set<String> alphabet;
   private final Set<String> initialStates;
   private final Set<String> acceptingStates;
-  private final Set<NBATransition> transitions;
+  private final Set<NBATransition<ActionType>> transitions;
 
   public NBABuilder() {
     this.states = new HashSet<>();
@@ -19,7 +19,7 @@ public NBABuilder() {
     this.transitions = new HashSet<>();
   }
 
-  public NBABuilder addStates(String... states) {
+  public NBABuilder<ActionType> addStates(String... states) {
     for (String state : states) {
       addState(state);
     }
@@ -27,33 +27,33 @@ public NBABuilder addStates(String... states) {
     return this;
   }
 
-  public NBABuilder addState(String state) {
+  public NBABuilder<ActionType> addState(String state) {
     this.states.add(state);
     return this;
   }
 
-  public NBABuilder setAlphabet(Set<String> alphabet) {
+  public NBABuilder<ActionType> setAlphabet(Set<String> alphabet) {
     this.alphabet.clear();
     this.alphabet.addAll(alphabet);
     return this;
   }
 
-  public NBABuilder addInitialState(String initialState) {
+  public NBABuilder<ActionType> addInitialState(String initialState) {
     this.initialStates.add(initialState);
     return this;
   }
 
-  public NBABuilder addAcceptingState(String acceptingState) {
+  public NBABuilder<ActionType> addAcceptingState(String acceptingState) {
     this.acceptingStates.add(acceptingState);
     return this;
   }
 
-  public NBABuilder addTransition(String from, String action, String to) {
+  public NBABuilder<ActionType> addTransition(String from, ActionType action, String to) {
     this.transitions.add(NBATransition.of(from, action, to));
     return this;
   }
 
-  public NBA build() {
+  public NBA<ActionType> build() {
     return new NBA(states, alphabet, initialStates, acceptingStates, transitions);
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java
index 00f50d2..a1ef4f2 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java
@@ -1,28 +1,32 @@
 package me.paultristanwagner.modelchecking.automaton;
 
 import com.google.gson.*;
+import com.google.gson.reflect.TypeToken;
+import java.lang.reflect.Type;
+import java.util.Set;
 
-public class NBATransition {
+public class NBATransition<ActionType> {
 
   private final String from;
-  private final String action;
+  private final ActionType action;
   private final String to;
 
-  private NBATransition(String from, String action, String to) {
+  protected NBATransition(String from, ActionType action, String to) {
     this.from = from;
     this.action = action;
     this.to = to;
   }
 
-  public static NBATransition of(String from, String action, String to) {
-    return new NBATransition(from, action, to);
+  public static <ActionType> NBATransition<ActionType> of(
+      String from, ActionType action, String to) {
+    return new NBATransition<>(from, action, to);
   }
 
   public String getFrom() {
     return from;
   }
 
-  public String getAction() {
+  public ActionType getAction() {
     return action;
   }
 
@@ -30,24 +34,25 @@ public String getTo() {
     return to;
   }
 
-  public static class NBATransitionAdapter
-      implements JsonSerializer<NBATransition>, JsonDeserializer<NBATransition> {
+  public static class BasicNBATransitionAdapter
+      implements JsonSerializer<NBATransition<String>>, JsonDeserializer<NBATransition<String>> {
 
     @Override
     public JsonElement serialize(
-        NBATransition transition,
+        NBATransition<String> transition,
         java.lang.reflect.Type typeOfSrc,
         JsonSerializationContext context) {
       JsonArray jsonArray = new JsonArray();
       jsonArray.add(transition.getFrom());
-      jsonArray.add(transition.getAction());
+      jsonArray.add(
+          context.serialize(transition.getAction(), new TypeToken<String>() {}.getType()));
       jsonArray.add(transition.getTo());
 
       return jsonArray;
     }
 
     @Override
-    public NBATransition deserialize(
+    public NBATransition<String> deserialize(
         JsonElement json, java.lang.reflect.Type typeOfT, JsonDeserializationContext context)
         throws JsonParseException {
       JsonArray tuple = json.getAsJsonArray();
@@ -57,4 +62,35 @@ public NBATransition deserialize(
       return NBATransition.of(from, action, to);
     }
   }
+
+  public static class AdvancedNBATransitionAdapter
+      implements JsonSerializer<NBATransition<Set<String>>>,
+          JsonDeserializer<NBATransition<Set<String>>> {
+
+    @Override
+    public JsonElement serialize(
+        NBATransition<Set<String>> transition,
+        java.lang.reflect.Type typeOfSrc,
+        JsonSerializationContext context) {
+      JsonArray jsonArray = new JsonArray();
+      jsonArray.add(transition.getFrom());
+      jsonArray.add(
+          context.serialize(transition.getAction(), new TypeToken<Set<String>>() {}.getType()));
+      jsonArray.add(transition.getTo());
+
+      return jsonArray;
+    }
+
+    @Override
+    public NBATransition<Set<String>> deserialize(
+        JsonElement json, Type typeOfT, JsonDeserializationContext context)
+        throws JsonParseException {
+      JsonArray tuple = json.getAsJsonArray();
+      String from = tuple.get(0).getAsString();
+      Set<String> action =
+          context.deserialize(tuple.get(1), new TypeToken<Set<String>>() {}.getType());
+      String to = tuple.get(2).getAsString();
+      return NBATransition.of(from, action, to);
+    }
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
index 5df762b..03b8e69 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
@@ -19,11 +19,25 @@ public class BasicLTLModelChecker implements LTLModelChecker {
   public LTLModelCheckingResult check(TransitionSystem ts, LTLFormula formula) {
     ts = ts.copy();
 
+    // Ensure that the transition system contains only the mentioned atomic propositions
+    Set<String> remaining = new HashSet<>(ts.getAtomicPropositions());
+    for (LTLFormula subformula : formula.getAllSubformulas()) {
+      if (subformula instanceof LTLIdentifierFormula identifierFormula) {
+        String identifier = identifierFormula.getIdentifier();
+        remaining.remove(identifier);
+        ts.addAtomicProposition(identifier);
+      }
+    }
+
+    for (String ap : remaining) {
+      ts.removeAtomicProposition(ap);
+    }
+
     LTLFormula negation = formula.negate();
 
-    GNBA gnba = computeGNBA(ts, negation);
+    GNBA<Set<String>> gnba = computeGNBA(ts, negation);
 
-    NBA nba = gnba.convertToNBA();
+    NBA<Set<String>> nba = gnba.convertToNBA();
     TransitionSystem synchronousProduct = ts.reachableSynchronousProduct(nba);
 
     Set<String> persistentStates = new HashSet<>(nba.getStates());
@@ -65,12 +79,12 @@ public Set<String> sat(TransitionSystem ts, LTLFormula formula) {
     return result;
   }
 
-  private GNBA computeGNBA(TransitionSystem ts, LTLFormula formula) {
+  private GNBA<Set<String>> computeGNBA(TransitionSystem ts, LTLFormula formula) {
     Set<String> atomicPropositions = new HashSet<>(ts.getAtomicPropositions());
     Set<LTLFormula> closure = formula.getClosure();
     Set<B> elementarySets = computeElementarySets(atomicPropositions, closure);
 
-    GNBABuilder gnbaBuilder = new GNBABuilder();
+    GNBABuilder<Set<String>> gnbaBuilder = new GNBABuilder<>();
 
     /*
      * Compute the states and transitions of the GNBA
@@ -130,8 +144,9 @@ private GNBA computeGNBA(TransitionSystem ts, LTLFormula formula) {
         if (violates) {
           continue;
         }
+
         gnbaBuilder.addTransition(
-            one.toString(), assumedAtomicPropositions.toString(), potentialSuccessor.toString());
+            one.toString(), assumedAtomicPropositions, potentialSuccessor.toString());
       }
     }
 
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java
index 8434232..d0d6176 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java
@@ -24,7 +24,7 @@
 
 public class LTLParser implements Parser<LTLFormula> {
 
-  // todo: add logical operators for implication and equivalence
+  // todo: add logical operators for equivalence
 
   /*
    * LTL Grammar:
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java
index cb04296..a662084 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java
@@ -2,28 +2,16 @@
 
 import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.notPersistent;
 import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.persistent;
+import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON;
 import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
 
-import com.google.gson.Gson;
-import com.google.gson.GsonBuilder;
 import java.util.*;
 import java.util.AbstractMap.SimpleEntry;
 import me.paultristanwagner.modelchecking.automaton.NBA;
 import me.paultristanwagner.modelchecking.automaton.NBATransition;
-import me.paultristanwagner.modelchecking.ts.TSTransition.TSTransitionAdapter;
 
 public class TransitionSystem {
 
-  private static final Gson GSON;
-
-  static {
-    GSON =
-        new GsonBuilder()
-            .registerTypeAdapter(TSTransition.class, new TSTransitionAdapter())
-            .setPrettyPrinting()
-            .create();
-  }
-
   private final Set<String> states;
   private final Set<TSTransition> transitions;
   private final Set<String> initialStates;
@@ -70,7 +58,7 @@ public TransitionSystem copy() {
         states, transitions, initialStates, atomicPropositions, labelingFunction);
   }
 
-  public TransitionSystem reachableSynchronousProduct(NBA nba) {
+  public TransitionSystem reachableSynchronousProduct(NBA<Set<String>> nba) {
     TransitionSystemBuilder builder = new TransitionSystemBuilder();
 
     for (String state : nba.getStates()) {
@@ -81,7 +69,7 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
     for (String initialState : initialStates) {
       Set<String> label = labelingFunction.get(initialState);
 
-      for (NBATransition nbaTransition : nba.getTransitions()) {
+      for (NBATransition<Set<String>> nbaTransition : nba.getTransitions()) {
         String q0 = nbaTransition.getFrom();
         if (!nba.getInitialStates().contains(q0)) {
           continue;
@@ -89,17 +77,7 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
 
         String q = nbaTransition.getTo();
 
-        String a = nbaTransition.getAction();
-        String b = label.toString();
-
-        // todo: make this more efficient
-        Set<String> left = new HashSet<>(Arrays.asList(a.substring(1, a.length() - 1).split(", ")));
-        Set<String> right =
-            new HashSet<>(Arrays.asList(b.substring(1, b.length() - 1).split(", ")));
-
-        boolean actionMatches = left.equals(right);
-
-        if (!actionMatches) {
+        if (!nbaTransition.getAction().equals(label)) {
           continue;
         }
 
@@ -123,8 +101,7 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
 
       for (String sSuccessor : sSuccessors) {
         Set<String> sSuccessorLabel = labelingFunction.get(sSuccessor);
-        String sSuccessorLabelString = sSuccessorLabel.toString();
-        Set<String> qSuccessors = nba.getSuccessors(q, sSuccessorLabelString);
+        Set<String> qSuccessors = nba.getSuccessors(q, sSuccessorLabel);
         for (String qSuccessor : qSuccessors) {
 
           String from = stringTuple(s, q);
@@ -219,6 +196,15 @@ public TSPersistenceResult checkPersistence(Set<String> persistentStates) {
     return persistent();
   }
 
+  public void addAtomicProposition(String atomicProposition) {
+    atomicPropositions.add(atomicProposition);
+  }
+
+  public void removeAtomicProposition(String atomicProposition) {
+    atomicPropositions.remove(atomicProposition);
+    labelingFunction.forEach((state, labels) -> labels.remove(atomicProposition));
+  }
+
   public String introduceFreshAtomicProposition() {
     int i = 0;
     while (true) {
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java
index cba0633..c5183ee 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java
@@ -1,23 +1,14 @@
 package me.paultristanwagner.modelchecking.ts;
 
-import com.google.gson.Gson;
-import com.google.gson.GsonBuilder;
+import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON;
+
+import com.google.gson.reflect.TypeToken;
 import java.io.File;
 import java.io.IOException;
 import java.nio.file.Files;
 
 public class TransitionSystemLoader {
 
-  private static final Gson GSON;
-
-  static {
-    GSON =
-        new GsonBuilder()
-            .registerTypeAdapter(TSTransition.class, new TSTransition.TSTransitionAdapter())
-            .setPrettyPrinting()
-            .create();
-  }
-
   public static TransitionSystem load(String path) throws IOException {
     File file = new File(path);
     return load(file);
@@ -29,6 +20,6 @@ public static TransitionSystem load(File file) throws IOException {
   }
 
   public static TransitionSystem fromJson(String string) {
-    return GSON.fromJson(string, TransitionSystem.class);
+    return GSON.fromJson(string, new TypeToken<TransitionSystem>() {}.getType());
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/GsonUtil.java b/src/main/java/me/paultristanwagner/modelchecking/util/GsonUtil.java
new file mode 100644
index 0000000..c90d28a
--- /dev/null
+++ b/src/main/java/me/paultristanwagner/modelchecking/util/GsonUtil.java
@@ -0,0 +1,23 @@
+package me.paultristanwagner.modelchecking.util;
+
+import com.google.gson.Gson;
+import com.google.gson.GsonBuilder;
+import com.google.gson.reflect.TypeToken;
+import java.util.Set;
+import me.paultristanwagner.modelchecking.automaton.NBATransition;
+import me.paultristanwagner.modelchecking.ts.TSTransition;
+
+public class GsonUtil {
+
+  static {
+    GSON =
+        new GsonBuilder()
+            .registerTypeAdapter(TSTransition.class, new TSTransition.TSTransitionAdapter())
+            .registerTypeAdapter(new TypeToken<NBATransition<String>>() {}.getType(), new NBATransition.BasicNBATransitionAdapter())
+            .registerTypeAdapter(new TypeToken<NBATransition<Set<String>>>() {}.getType(), new NBATransition.AdvancedNBATransitionAdapter())
+            .setPrettyPrinting()
+            .create();
+  }
+
+  public static final Gson GSON;
+}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/Pair.java b/src/main/java/me/paultristanwagner/modelchecking/util/Pair.java
new file mode 100644
index 0000000..5a258c0
--- /dev/null
+++ b/src/main/java/me/paultristanwagner/modelchecking/util/Pair.java
@@ -0,0 +1,39 @@
+package me.paultristanwagner.modelchecking.util;
+
+import java.util.Objects;
+
+public class Pair<A, B> {
+
+  private final A a;
+  private final B b;
+
+  private Pair(A a, B b) {
+    this.a = a;
+    this.b = b;
+  }
+
+  public static <A, B> Pair<A, B> pair(A a, B b) {
+    return new Pair<>(a, b);
+  }
+
+  public A getFirst() {
+    return a;
+  }
+
+  public B getSecond() {
+    return b;
+  }
+
+  @Override
+  public boolean equals(Object o) {
+    if (this == o) return true;
+    if (o == null || getClass() != o.getClass()) return false;
+    Pair<?, ?> pair = (Pair<?, ?>) o;
+    return Objects.equals(a, pair.a) && Objects.equals(b, pair.b);
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(a, b);
+  }
+}
diff --git a/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java b/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java
index c4c04e3..5f263bf 100644
--- a/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java
+++ b/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java
@@ -1,10 +1,9 @@
 package me.paultristanwagner.modelchecking;
 
+import com.google.gson.reflect.TypeToken;
 import java.io.IOException;
 import java.io.InputStream;
-import me.paultristanwagner.modelchecking.automaton.GNBA;
-import me.paultristanwagner.modelchecking.automaton.NBA;
-import me.paultristanwagner.modelchecking.automaton.NBAEmptinessResult;
+import me.paultristanwagner.modelchecking.automaton.*;
 import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Test;
 
@@ -15,8 +14,8 @@ public void testNBAConstruction() throws IOException {
     InputStream gnbaIs =
         getClass().getClassLoader().getResourceAsStream("gnba_inf_crit1_and_inf_crit2.json");
     String gnbaJson = new String(gnbaIs.readAllBytes());
-    GNBA gnba = GNBA.fromJson(gnbaJson);
-    NBA nba = gnba.convertToNBA();
+    GNBA<String> gnba = GNBA.fromJson(gnbaJson, new TypeToken<GNBA<String>>() {}.getType());
+    NBA<String> nba = gnba.convertToNBA();
 
     NBAEmptinessResult nbaEmptinessResult = nba.checkEmptiness();
     Assertions.assertFalse(nbaEmptinessResult.isEmpty());
@@ -33,11 +32,11 @@ public void testNonEmptyProduct() throws IOException {
     String nba1Json = new String(nba1Is.readAllBytes());
     String nba2Json = new String(nba2Is.readAllBytes());
 
-    NBA nba1 = NBA.fromJson(nba1Json);
-    NBA nba2 = NBA.fromJson(nba2Json);
+    NBA<String> nba1 = NBA.fromJson(nba1Json, new TypeToken<NBA<String>>() {}.getType());
+    NBA<String> nba2 = NBA.fromJson(nba2Json, new TypeToken<NBA<String>>() {}.getType());
 
-    GNBA product = nba1.product(nba2);
-    NBA nbaResult = product.convertToNBA();
+    GNBA<String> product = nba1.product(nba2);
+    NBA<String> nbaResult = product.convertToNBA();
 
     NBAEmptinessResult nbaEmptinessResult = nbaResult.checkEmptiness();
     Assertions.assertFalse(nbaEmptinessResult.isEmpty());
@@ -51,11 +50,11 @@ public void testEmptyProduct() throws IOException {
     String nba1Json = new String(nba1Is.readAllBytes());
     String nba2Json = new String(nba2Is.readAllBytes());
 
-    NBA nba1 = NBA.fromJson(nba1Json);
-    NBA nba2 = NBA.fromJson(nba2Json);
+    NBA<String> nba1 = NBA.fromJson(nba1Json, new TypeToken<NBA<String>>() {}.getType());
+    NBA<String> nba2 = NBA.fromJson(nba2Json, new TypeToken<NBA<String>>() {}.getType());
 
-    GNBA product = nba1.product(nba2);
-    NBA nbaResult = product.convertToNBA();
+    GNBA<String> product = nba1.product(nba2);
+    NBA<String> nbaResult = product.convertToNBA();
 
     NBAEmptinessResult nbaEmptinessResult = nbaResult.checkEmptiness();
     Assertions.assertTrue(nbaEmptinessResult.isEmpty());
diff --git a/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java b/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java
index 215c366..cb3738d 100644
--- a/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java
+++ b/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java
@@ -1,7 +1,9 @@
 package me.paultristanwagner.modelchecking;
 
+import com.google.gson.reflect.TypeToken;
 import java.io.IOException;
 import java.io.InputStream;
+import java.util.Set;
 import me.paultristanwagner.modelchecking.automaton.NBA;
 import me.paultristanwagner.modelchecking.ts.TransitionSystem;
 import me.paultristanwagner.modelchecking.ts.TransitionSystemLoader;
@@ -20,7 +22,7 @@ public void testSynchronousProduct() throws IOException {
     InputStream nbaInputStream =
         getClass().getClassLoader().getResourceAsStream("nba_never_delivered.json");
     String nbaJson = new String(nbaInputStream.readAllBytes());
-    NBA nba = NBA.fromJson(nbaJson);
+    NBA<Set<String>> nba = NBA.fromJson(nbaJson, new TypeToken<NBA<Set<String>>>() {}.getType());
 
     TransitionSystem result = ts.reachableSynchronousProduct(nba);
     Assertions.assertNotNull(result);
diff --git a/src/test/resources/nba_never_delivered.json b/src/test/resources/nba_never_delivered.json
index 43903b6..f96ba68 100644
--- a/src/test/resources/nba_never_delivered.json
+++ b/src/test/resources/nba_never_delivered.json
@@ -2,22 +2,22 @@
   "states": ["q0","qF","q1"],
   "alphabet": ["start","delivered","lost","try_to_send"],
   "transitions": [
-    ["q0","[try_to_send]","qF"],
-    ["q0","[]","q0"],
-    ["q0","[start]","q0"],
-    ["q0","[delivered]","q0"],
-    ["q0","[lost]","q0"],
-    ["q0","[try_to_send]","q0"],
-    ["qF","[delivered]","q1"],
-    ["qF","[]","qF"],
-    ["qF","[start]","qF"],
-    ["qF","[lost]","qF"],
-    ["qF","[try_to_send]","qF"],
-    ["q1","[]","q1"],
-    ["q1","[start]","q1"],
-    ["q1","[delivered]","q1"],
-    ["q1","[lost]","q1"],
-    ["q1","[try_to_send]","q1"]
+    ["q0", ["try_to_send"], "qF"],
+    ["q0", [], "q0"],
+    ["q0", ["start"], "q0"],
+    ["q0", ["delivered"], "q0"],
+    ["q0", ["lost"], "q0"],
+    ["q0", ["try_to_send"], "q0"],
+    ["qF", ["delivered"], "q1"],
+    ["qF", [], "qF"],
+    ["qF", ["start"], "qF"],
+    ["qF", ["lost"], "qF"],
+    ["qF", ["try_to_send"], "qF"],
+    ["q1", [], "q1"],
+    ["q1", ["start"], "q1"],
+    ["q1", ["delivered"], "q1"],
+    ["q1", ["lost"], "q1"],
+    ["q1", ["try_to_send"], "q1"]
   ],
   "initialStates": ["q0"],
   "acceptingStates": ["qF"]