diff --git a/modelchecking/m3c/src/main/javacc/M3C.jj b/modelchecking/m3c/src/main/javacc/M3C.jj
index 01367dda2d..a30e49acb7 100644
--- a/modelchecking/m3c/src/main/javacc/M3C.jj
+++ b/modelchecking/m3c/src/main/javacc/M3C.jj
@@ -98,7 +98,7 @@ PARSER_END(InternalM3CParser)
 |	< IMPLICATION: "->" >
 |	< ID: ["a"-"z","A"-"Z"] (["a"-"z","A"-"Z"] | ["0"-"9"] | "_")* >
 |	< STRING_LITERAL: ("'" (~["'", "\\"])* (("\\\'" | "\\\\") (~["'", "\\"])*)* "'")
-| ("\""  (~["\"", "\\"])* (("\\\"" | "\\\\") (~["\"", "\\"])*)* "\"")>
+					| ("\""  (~["\"", "\\"])* (("\\\"" | "\\\\") (~["\"", "\\"])*)* "\"")>
 }
 
 FormulaNode<L, AP> parse(Function<String, L> labelParser, Function<String, AP> apParser):
@@ -213,8 +213,8 @@ private FormulaNode<L, AP> unary():
 |	<AG> child=unary() {return new AGNode<L, AP>(child);}
 |	<EF> child=unary() {return new EFNode<L, AP>(child);}
 |	<EG> child=unary() {return new EGNode<L, AP>(child);}
-|	<LABRACKET> (action=<ID>)? <RABRACKET> child=unary() {return new DiamondNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
-|	<LBRACKET> (action=<ID>)? <RBRACKET> child=unary() {return new BoxNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
+|	<LABRACKET> (action=action())? <RABRACKET> child=unary() {return new DiamondNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
+|	<LBRACKET> (action=action())? <RBRACKET> child=unary() {return new BoxNode<L, AP>(action==null ? null : this.labelParser.apply(action.toString()), child);}
 |	child=element() {return child;}
 }
 
@@ -260,3 +260,25 @@ private FormulaNode<L, AP> element():
 |	<FALSE> {return new FalseNode<L, AP>();}
 |	<LPAREN> node=formula() <RPAREN> {return node;}
 }
+
+/*
+ * We cannot parse <ID> only, because the input may have been greedily parsed as a different token before.
+ */
+private Token action():
+{
+	Token action;
+}
+{
+	(action=<ALL>
+|	action=<EXISTS>
+|	action=<AF>
+|	action=<AG>
+|	action=<EF>
+|	action=<EG>
+|	action=<UNTIL>
+|	action=<WUNTIL>
+|	action=<NU>
+|	action=<MU>
+|	action=<ID>) { return action; }
+}
+
diff --git a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserCTLTest.java b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserCTLTest.java
index 70a2044a3e..c3057da168 100644
--- a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserCTLTest.java
+++ b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserCTLTest.java
@@ -71,12 +71,24 @@ public void baseCasesTest() throws ParseException {
         assertEquals("[c]true", new BoxNode<>("c", new TrueNode<>()));
     }
 
-    private void assertEquals(String ctlFormula, FormulaNode<String, String> expectedAST) throws ParseException {
-        FormulaNode<String, String> actualAST = M3CParser.parse(ctlFormula);
-        Assert.assertEquals(actualAST, expectedAST);
-        Assert.assertEquals(actualAST.hashCode(), expectedAST.hashCode());
-
-        this.formulas.add(actualAST);
+    @Test
+    public void tokensAsActionsTest() throws ParseException {
+        assertEquals("<A>true", new DiamondNode<>("A", new TrueNode<>()));
+        assertEquals("<AF>true", new DiamondNode<>("AF", new TrueNode<>()));
+        assertEquals("<AG>true", new DiamondNode<>("AG", new TrueNode<>()));
+        assertEquals("<E>true", new DiamondNode<>("E", new TrueNode<>()));
+        assertEquals("<EF>true", new DiamondNode<>("EF", new TrueNode<>()));
+        assertEquals("<EG>true", new DiamondNode<>("EG", new TrueNode<>()));
+        assertEquals("<U>true", new DiamondNode<>("U", new TrueNode<>()));
+        assertEquals("<W>true", new DiamondNode<>("W", new TrueNode<>()));
+        assertEquals("[A]true", new BoxNode<>("A", new TrueNode<>()));
+        assertEquals("[AF]true", new BoxNode<>("AF", new TrueNode<>()));
+        assertEquals("[AG]true", new BoxNode<>("AG", new TrueNode<>()));
+        assertEquals("[E]true", new BoxNode<>("E", new TrueNode<>()));
+        assertEquals("[EF]true", new BoxNode<>("EF", new TrueNode<>()));
+        assertEquals("[EG]true", new BoxNode<>("EG", new TrueNode<>()));
+        assertEquals("[U]true", new BoxNode<>("U", new TrueNode<>()));
+        assertEquals("[W]true", new BoxNode<>("W", new TrueNode<>()));
     }
 
     @Test
@@ -86,7 +98,7 @@ public void nestedFormulasTest() throws ParseException {
                                   new AndNode<>(new FalseNode<>(), new FalseNode<>())));
     }
 
-    @Test(dependsOnMethods = {"baseCasesTest", "nestedFormulasTest"})
+    @Test(dependsOnMethods = {"baseCasesTest", "tokensAsActionsTest", "nestedFormulasTest"})
     public void testEqualities() {
         for (FormulaNode<String, String> n1 : formulas) {
             for (FormulaNode<String, String> n2 : formulas) {
@@ -104,6 +116,14 @@ public void testIllegalFormulas() {
         assertIllegal("(mu X.(<b> true || <>X) || (AF true)");
     }
 
+    private void assertEquals(String ctlFormula, FormulaNode<String, String> expectedAST) throws ParseException {
+        FormulaNode<String, String> actualAST = M3CParser.parse(ctlFormula);
+        Assert.assertEquals(actualAST, expectedAST);
+        Assert.assertEquals(actualAST.hashCode(), expectedAST.hashCode());
+
+        this.formulas.add(actualAST);
+    }
+
     private void assertIllegal(String formula) {
         Assert.assertThrows(ParseException.class, () -> M3CParser.parse(formula));
     }
diff --git a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserMuCalcTest.java b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserMuCalcTest.java
index 76ed114d4a..052ff22a86 100644
--- a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserMuCalcTest.java
+++ b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/formula/parser/ParserMuCalcTest.java
@@ -60,6 +60,19 @@ public void testBaseCases() throws ParseException {
                      new LfpNode<>("XY", new OrNode<>(new VariableNode<>("XY"), new FalseNode<>())));
         assertEquals("nu ZY.(ZY || false)",
                      new GfpNode<>("ZY", new OrNode<>(new VariableNode<>("ZY"), new FalseNode<>())));
+        // allow CTL tokens as variable names as well
+        assertEquals("mu E.(E || false)",
+                     new LfpNode<>("E", new OrNode<>(new VariableNode<>("E"), new FalseNode<>())));
+        assertEquals("nu AF.(AF || false)",
+                     new GfpNode<>("AF", new OrNode<>(new VariableNode<>("AF"), new FalseNode<>())));
+    }
+
+    @Test
+    public void tokensAsActionsTest() throws ParseException {
+        assertEquals("<mu>true", new DiamondNode<>("mu", new TrueNode<>()));
+        assertEquals("<nu>true", new DiamondNode<>("nu", new TrueNode<>()));
+        assertEquals("[mu]true", new BoxNode<>("mu", new TrueNode<>()));
+        assertEquals("[nu]true", new BoxNode<>("nu", new TrueNode<>()));
     }
 
     @Test