diff --git a/CMakeLists.txt b/CMakeLists.txt
index f5695a60..71a10d23 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -73,4 +73,4 @@ install(TARGETS UTAP EXPORT UTAPConfig LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDI
 install(EXPORT UTAPConfig DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/UTAP/)
 install(FILES ${CMAKE_CURRENT_BINARY_DIR}/UTAPConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/UTAP )
 
-# set(CMAKE_CXX_STANDARD_LIBRARIES "-static -lwsock32 -lws2_32 -lz -lmcfgthread ${CMAKE_CXX_STANDARD_LIBRARIES}")
+# set(CMAKE_CXX_STANDARD_LIBRARIES "-static -lwsock32 -lws2_32 -lz -lmcfgthread ${CMAKE_CXX_STANDARD_LIBRARIES}")
\ No newline at end of file
diff --git a/include/utap/AbstractBuilder.hpp b/include/utap/AbstractBuilder.hpp
index 1b43870a..ca0cc4ab 100644
--- a/include/utap/AbstractBuilder.hpp
+++ b/include/utap/AbstractBuilder.hpp
@@ -119,7 +119,7 @@ class AbstractBuilder : public ParserBuilder
     void proc_location_urgent(const char* name) override;                          // mark previously decl. state
     void proc_location_init(const char* name) override;                            // mark previously decl. state
     void proc_branchpoint(const char* name) override;
-    void proc_edge_begin(const char* from, const char* to, const bool control, const char* actname) override;
+    void proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname) override;
     void proc_edge_end(const char* from, const char* to) override;
     // 1 epxr,1sync,1expr
     void proc_select(const char* id) override;
@@ -219,6 +219,8 @@ class AbstractBuilder : public ParserBuilder
     void expr_load_strategy() override;
     void expr_save_strategy(const char* strategy_name) override;
 
+    void expr_atl(int, Constants::kind_t) override;
+
     // MITL
     void expr_MITL_formula() override;
     void expr_MITL_until(int, int) override;
diff --git a/include/utap/DocumentBuilder.hpp b/include/utap/DocumentBuilder.hpp
index d2439b8a..6fa3e851 100644
--- a/include/utap/DocumentBuilder.hpp
+++ b/include/utap/DocumentBuilder.hpp
@@ -106,6 +106,8 @@ class DocumentBuilder : public StatementBuilder
 
     void addSelectSymbolToFrame(const std::string& name, frame_t&, position_t pos);
 
+    uint32_t parse_hex_color(const char* color);
+
 public:
     DocumentBuilder(Document&, std::vector<std::filesystem::path> paths = {});
 
@@ -124,7 +126,7 @@ class DocumentBuilder : public StatementBuilder
     void proc_location_urgent(const char* name) override;
     void proc_location_init(const char* name) override;
     void proc_branchpoint(const char* name) override;
-    void proc_edge_begin(const char* from, const char* to, const bool control, const char* actname) override;
+    void proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname) override;
     void proc_edge_end(const char* from = 0, const char* to = 0) override;
     void proc_select(const char* id) override;
     void proc_guard() override;
diff --git a/include/utap/ExpressionBuilder.hpp b/include/utap/ExpressionBuilder.hpp
index 88d469ec..f3857711 100644
--- a/include/utap/ExpressionBuilder.hpp
+++ b/include/utap/ExpressionBuilder.hpp
@@ -195,6 +195,8 @@ class ExpressionBuilder : public AbstractBuilder
     void expr_save_strategy(const char* strategy_name) override;
     void expr_load_strategy() override;
 
+    void expr_atl(int, Constants::kind_t) override;
+
     void expr_simulate(int nb_of_exprs, bool filter_prop = false, int max_accepting_runs = 0) override;
     void expr_MITL_formula() override;
     void expr_MITL_until(int, int) override;
diff --git a/include/utap/builder.h b/include/utap/builder.h
index 32f903bf..a609998c 100644
--- a/include/utap/builder.h
+++ b/include/utap/builder.h
@@ -247,7 +247,7 @@ class ParserBuilder
     virtual void proc_location_commit(const char* name) = 0;                          // mark previously decl. state
     virtual void proc_location_urgent(const char* name) = 0;                          // mark previously decl. state
     virtual void proc_location_init(const char* name) = 0;                            // mark previously decl. state
-    virtual void proc_edge_begin(const char* from, const char* to, const bool control, const char* actname = "") = 0;
+    virtual void proc_edge_begin(const char* from, const char* to, const bool control, const char* color = "#000000", const char* actname = "") = 0;
     virtual void proc_edge_end(const char* from, const char* to) = 0;
     virtual void proc_select(const char* id) = 0;                   // 1 expr
     virtual void proc_guard() = 0;                                  // 1 expr
@@ -363,6 +363,8 @@ class ParserBuilder
     virtual void expr_load_strategy() = 0;
     virtual void expr_save_strategy(const char* strategy_name) = 0;
 
+    virtual void expr_atl(int, Constants::kind_t) = 0;
+
     // MITL Extensions
     virtual void expr_MITL_formula() = 0;
     virtual void expr_MITL_until(int, int) = 0;
diff --git a/include/utap/common.h b/include/utap/common.h
index 1341e605..45ed55f3 100644
--- a/include/utap/common.h
+++ b/include/utap/common.h
@@ -44,6 +44,7 @@ enum kind_t {
     MAX,
     RATE,
     FRACTION,
+    FREEZE,
 
     /********************************************************
      * Relational operators
@@ -143,6 +144,18 @@ enum kind_t {
     ASS_LSHIFT,
     ASS_RSHIFT,
 
+    /*******************************************************
+     * ATL Quantifiers
+     */
+    ATL_ENFORCE_UNTIL,
+    ATL_DESPITE_UNTIL,
+    ATL_ENFORCE_F,
+    ATL_DESPITE_F,
+    ATL_ENFORCE_G,
+    ATL_DESPITE_G,
+    ATL_ENFORCE_NEXT,
+    ATL_DESPITE_NEXT,
+
     /*******************************************************
      * CTL Quantifiers
      */
diff --git a/include/utap/document.h b/include/utap/document.h
index 06ad2fcb..ad4c420e 100644
--- a/include/utap/document.h
+++ b/include/utap/document.h
@@ -107,6 +107,7 @@ struct edge_t : stringify_t<edge_t>
 {
     int nr;       /**< Placement in input file */
     bool control; /**< Controllable (true/false) */
+    uint32_t color;
     std::string actname;
     location_t* src{nullptr};          /**< Pointer to source location */
     branchpoint_t* srcb{nullptr};      /**< Pointer to source branchpoint */
diff --git a/include/utap/expression.h b/include/utap/expression.h
index 2ad68386..7a62da9e 100644
--- a/include/utap/expression.h
+++ b/include/utap/expression.h
@@ -102,6 +102,9 @@ class expression_t
     /** Returns the number of subexpression. */
     size_t get_size() const;
 
+    /** Returns the number of player colors in this expression. */
+    size_t get_player_count() const;
+
     /** Returns the position of this expression. */
     const position_t& get_position() const;
 
diff --git a/include/utap/prettyprinter.h b/include/utap/prettyprinter.h
index d54ba65c..eb557f0b 100644
--- a/include/utap/prettyprinter.h
+++ b/include/utap/prettyprinter.h
@@ -117,7 +117,7 @@ class PrettyPrinter : public AbstractBuilder
     void proc_sync(Constants::synchronisation_t type) override;
     void proc_update() override;
     void proc_edge_begin(const char* source, const char* target, const bool control);
-    void proc_edge_begin(const char* source, const char* target, const bool control, const char* actname) override;
+    void proc_edge_begin(const char* source, const char* target, const bool control, const char* color, const char* actname) override;
     void proc_edge_end(const char* source, const char* target) override;
     void proc_end() override;
     void expr_identifier(const char* id) override;
diff --git a/include/utap/property.h b/include/utap/property.h
index dedaa79f..d50a7aa9 100644
--- a/include/utap/property.h
+++ b/include/utap/property.h
@@ -58,6 +58,9 @@ enum class quant_t {
     probaSimulateReach,  // simulate [...] { ... } : n : p
     Mitl,
 
+    /* ATL quantifiers: */
+    Atl,
+
     /* TIGA quantifiers for controller synthesis:
      * - A[ p U q ] : AUntil
      * - A[ p W q ] : AWeakUntil
@@ -241,7 +244,7 @@ class PropertyBuilder : public std::enable_shared_from_this<PropertyBuilder>, pu
     bool isSMC(UTAP::expression_t* expr = nullptr);
 };
 
-class TigaPropertyBuilder final : public PropertyBuilder
+class TigaPropertyBuilder : public PropertyBuilder
 {
 protected:
     std::map<std::string, PropInfo*> declarations{};
@@ -266,6 +269,15 @@ class TigaPropertyBuilder final : public PropertyBuilder
     */
 };
 
+class AtlPropertyBuilder final : public TigaPropertyBuilder
+{
+public:
+    AtlPropertyBuilder(const UTAP::Document& doc) : TigaPropertyBuilder{doc} {}
+
+protected:
+    void typeProperty(UTAP::expression_t expression) override;
+};
+
 }  // namespace UTAP
 
 #endif /* VERIFIER_PROPERTY */
diff --git a/src/DocumentBuilder.cpp b/src/DocumentBuilder.cpp
index 07611ec1..585d2817 100644
--- a/src/DocumentBuilder.cpp
+++ b/src/DocumentBuilder.cpp
@@ -231,7 +231,7 @@ void DocumentBuilder::proc_location_init(const char* name)
     }
 }
 
-void DocumentBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* actname)
+void DocumentBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname)
 {
     symbol_t fid, tid;
 
@@ -243,6 +243,7 @@ void DocumentBuilder::proc_edge_begin(const char* from, const char* to, const bo
         push_frame(frame_t::create(frames.top()));  // dummy frame for upcoming popFrame
     } else {
         currentEdge = &currentTemplate->add_edge(fid, tid, control, actname);
+        currentEdge->color = parse_hex_color(color);
         currentEdge->guard = make_constant(1);
         currentEdge->assign = make_constant(1);
         // default "probability" weight is 1.
@@ -754,3 +755,8 @@ void DocumentBuilder::model_option(const char* key, const char* value)
     }
     document.get_options().emplace_back(key, value == nullptr ? "" : value);
 }
+
+uint32_t DocumentBuilder::parse_hex_color(const char* color)
+{
+    return std::stoul(color + 1 /* Skip the '#' */, nullptr, 16);
+}
diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp
index e07181a9..ad950f9b 100644
--- a/src/ExpressionBuilder.cpp
+++ b/src/ExpressionBuilder.cpp
@@ -810,6 +810,24 @@ void ExpressionBuilder::expr_proba_expected(const char* aggregatingOp)
     fragments.push(expression_t::create_nary(PROBA_EXP, std::move(args), position));
 }
 
+void ExpressionBuilder::expr_atl(int nbPlayers, Constants::kind_t kind)
+{
+    int nbSubExprs = (kind == ATL_ENFORCE_UNTIL || kind == ATL_DESPITE_UNTIL) ? 2 : 1;
+    std::vector<expression_t> parts;
+    parts.reserve(nbPlayers + nbSubExprs);
+
+    for (int i = 0; i < nbPlayers; ++i) {
+        parts.push_back(fragments[nbPlayers + nbSubExprs - 1 - i]);
+    }
+
+    for (int i = 0; i < nbSubExprs; ++i) {
+        parts.push_back(fragments[nbSubExprs - 1 - i]);
+    }
+
+    fragments.pop(parts.size());
+    fragments.push(expression_t::create_nary(kind, parts, position));
+}
+
 void ExpressionBuilder::expr_simulate(int nbExpr, bool hasReach, int numberOfAcceptingRuns)
 {
     // Stack:
diff --git a/src/abstractbuilder.cpp b/src/abstractbuilder.cpp
index 08621726..41ed5694 100644
--- a/src/abstractbuilder.cpp
+++ b/src/abstractbuilder.cpp
@@ -109,7 +109,7 @@ void AbstractBuilder::proc_location_commit(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::proc_location_urgent(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::proc_location_init(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::proc_branchpoint(const char* name) { UNSUPPORTED; }
-void AbstractBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* actname)
+void AbstractBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname)
 {
     UNSUPPORTED;
 }
@@ -271,6 +271,8 @@ void AbstractBuilder::expr_foreach_dynamic_begin(const char*, const char*) { UNS
 void AbstractBuilder::expr_foreach_dynamic_end(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::expr_dynamic_process_expr(const char*) { UNSUPPORTED; }
 
+void AbstractBuilder::expr_atl(int, Constants::kind_t) { UNSUPPORTED; }
+
 void AbstractBuilder::expr_MITL_forall_dynamic_begin(const char*, const char*) { UNSUPPORTED; }
 void AbstractBuilder::expr_MITL_forall_dynamic_end(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::expr_MITL_exists_dynamic_begin(const char*, const char*) { UNSUPPORTED; }
diff --git a/src/document.cpp b/src/document.cpp
index 6c048bac..f284ed47 100644
--- a/src/document.cpp
+++ b/src/document.cpp
@@ -315,6 +315,7 @@ edge_t& template_t::add_edge(symbol_t src, symbol_t dst, bool control, string ac
     }
 
     edge.control = control;
+    edge.color = 0x000000;
     edge.actname = std::move(actname);
     edge.nr = nr;
     return edge;
diff --git a/src/expression.cpp b/src/expression.cpp
index af2e7499..897fe24b 100644
--- a/src/expression.cpp
+++ b/src/expression.cpp
@@ -327,6 +327,7 @@ size_t expression_t::get_size() const
     case BIT_XOR:
     case BIT_LSHIFT:
     case BIT_RSHIFT:
+    case FREEZE:
     case AND:
     case OR:
     case XOR:
@@ -444,6 +445,15 @@ size_t expression_t::get_size() const
     case SIMULATEREACH:
     case SPAWN: return std::get<int32_t>(data->value);
 
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL: assert(data->sub.size() >= 2); return std::get<int32_t>(data->value);
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT: assert(data->sub.size() >= 1); return std::get<int32_t>(data->value);
+
     case EG:
     case AG:
     case EF:
@@ -496,6 +506,27 @@ size_t expression_t::get_size() const
     }
 }
 
+size_t expression_t::get_player_count() const
+{
+    assert(data);
+    switch (data->kind) {
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL:
+        assert(get_size() >= 2);
+        return get_size() - 2;
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT:
+        assert(get_size() >= 1);
+        return get_size() - 1;
+    default:
+        return 0;
+    }
+}
+
 type_t expression_t::get_type() const
 {
     assert(data);
@@ -837,10 +868,18 @@ int expression_t::get_precedence(kind_t kind)
     case EXISTS:
     case SUM: return 8;
 
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL:
     case A_UNTIL:
     case A_WEAK_UNTIL:
     case A_BUCHI: return 7;
 
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT:
     case EF:
     case EG:
     case AF:
@@ -1425,6 +1464,70 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const
 
     case RATE: get(0).print(os, old) << '\''; break;
 
+    case FREEZE: os << get(0) << " @ " << get(1); break;
+
+    case ATL_ENFORCE_UNTIL:
+    case ATL_ENFORCE_F:
+    case ATL_ENFORCE_G:
+    case ATL_ENFORCE_NEXT: {
+        os << "<<";
+        size_t n = get_player_count();
+        for (int i = 0; i < n; ++i) {
+            get(i).print(os << "#" << std::setfill('0') << std::setw(6) << std::hex, old);
+            if (i < n - 1) os << ", ";
+        }
+        os << std::dec << ">> ";
+        switch (data->kind) {
+        case Constants::ATL_ENFORCE_UNTIL:
+            get(n).print(os << "[", old) << " U ";
+            get(n + 1).print(os, old) << "] ";
+            break;
+        case Constants::ATL_ENFORCE_F:
+            get(n).print(os << "<> ");
+            break;
+        case Constants::ATL_ENFORCE_G:
+            get(n).print(os << "[] ");
+            break;
+        case Constants::ATL_ENFORCE_NEXT:
+            get(n).print(os << "X ");
+            break;
+        default:
+            assert(false);
+        }
+        break;
+    }
+
+    case ATL_DESPITE_UNTIL:
+    case ATL_DESPITE_F:
+    case ATL_DESPITE_G:
+    case ATL_DESPITE_NEXT: {
+        os << "[[";
+        size_t n = get_player_count();
+        for (int i = 0; i < n; ++i) {
+            get(i).print(os << "#" << std::setfill('0') << std::setw(6) << std::hex, old);
+            if (i < n - 1) os << ", ";
+        }
+        os << "]] ";
+        switch (data->kind) {
+        case Constants::ATL_DESPITE_UNTIL:
+            get(n).print(os << "[", old) << " U ";
+            get(n + 1).print(os, old) << "] ";
+            break;
+        case Constants::ATL_DESPITE_F:
+            get(n).print(os << "<> ");
+            break;
+        case Constants::ATL_DESPITE_G:
+            get(n).print(os << "[] ");
+            break;
+        case Constants::ATL_DESPITE_NEXT:
+            get(n).print(os << "X ");
+            break;
+        default:
+            assert(false);
+        }
+        break;
+    }
+
     case EF:
         os << "E<> ";
         get(0).print(os, old);
diff --git a/src/lexer.l b/src/lexer.l
index 90c7dc79..cb5358da 100644
--- a/src/lexer.l
+++ b/src/lexer.l
@@ -150,15 +150,17 @@ idchr        [a-zA-Z0-9_$#]
 ">"        	{ return T_GT; }
 "=="        	{ return T_EQ; }
 "!="        	{ return T_NEQ; }
-
 "++"            { return T_INCREMENT; }
 "--"            { return T_DECREMENT; }
 
+"@"             { return T_FREEZE; }
+
 "A"             { return 'A'; }
 "U"             { return 'U'; }
 "R"             { return 'R'; }
 "W"             { return 'W'; }
 "E"             { return 'E'; }
+"X"             { return 'X'; }
 
 "A<>"           { return T_AF; }
 "A[]"           { return T_AG; }
diff --git a/src/parser.y b/src/parser.y
index 265b992e..1b018e92 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -186,6 +186,7 @@ const char* utap_msg(const char *msg)
 %token T_OR T_XOR T_LSHIFT T_RSHIFT
 %token T_BOOL_AND T_BOOL_OR
 %token T_KW_AND T_KW_OR T_KW_XOR T_KW_IMPLY T_KW_NOT
+%token T_FREEZE
 
 /* Special */
 %token T_SUP T_INF T_BOUNDS
@@ -286,10 +287,10 @@ const char* utap_msg(const char *msg)
 %type <kind> ExpQuantifier ExpPrQuantifier
 %type <kind> PathType
 %type <number> ArgList FieldDeclList FieldDeclIdList FieldDecl
-%type <number> ParameterList FieldInitList
+%type <number> ParameterList FieldInitList PlayerColorList
 %type <number> OptionalInstanceParameterList ExpressionList NonEmptyExpressionList
 %type <prefix> Type TypePrefix
-%type <string> Id NonTypeId
+%type <string> Id NonTypeId PlayerColor
 %type <kind> UnaryOp AssignOp
 %type <flag> VarInit
 %type <kind> CmpGLE
@@ -299,7 +300,7 @@ const char* utap_msg(const char *msg)
 %right T_AF T_AG T_EF T_EG 'A'  'M'
 %right T_AG_PLUS T_EF_PLUS T_AG_MULT T_EF_MULT
 %right T_PMAX T_SCENARIO
-%left 'U' 'W' 'R'
+%left 'U' 'W' 'R' 'X'
 %right T_FORALL T_EXISTS T_SUM
 %right T_ASSIGNMENT T_ASSPLUS T_ASSMINUS T_ASSMULT T_ASSDIV T_ASSMOD T_ASSAND T_ASSOR T_ASSLSHIFT T_ASSRSHIFT T_ASSXOR
 %right '?' ':'
@@ -754,12 +755,25 @@ NonTypeId:
         | 'R' { strncpy($$, "R", MAXLEN); }
         | 'E' { strncpy($$, "E", MAXLEN); }
         | 'M' { strncpy($$, "M", MAXLEN); }
+        | 'X' { strncpy($$, "X", MAXLEN); }
         | T_SUP { strncpy($$, "sup", MAXLEN); }
         | T_INF { strncpy($$, "inf", MAXLEN); }
         | T_BOUNDS { strncpy($$, "bounds", MAXLEN); }
         | T_SIMULATION { strncpy($$, "simulation", MAXLEN); }
         ;
 
+PlayerColor:
+    NonTypeId {
+        CALL(@1, @1, expr_string($1));
+    }
+    ;
+
+PlayerColorList:
+    /* empty */ { $$=0; }
+    | PlayerColor { $$=1; }
+    | PlayerColorList ',' PlayerColor { $$=$1+1; }
+    ;
+
 FieldDeclList:
         FieldDecl { $$=$1; }
         | FieldDeclList FieldDecl { $$=$1+$2; }
@@ -1377,6 +1391,50 @@ DynamicExpression:
 	}
         ;
 
+AtlExpressionOrExpression:
+    '(' AtlExpression ')'
+    // FIXME: Fix ambiguity and remove ugly parenthesis
+    | '(' AtlExpression ')' BoolOrKWAnd AtlExpressionOrExpression {
+      CALL(@1, @5, expr_binary(AND));
+    }
+    // FIXME: Fix ambiguity and remove ugly parenthesis
+    | '(' AtlExpression ')' BoolOrKWOr AtlExpressionOrExpression {
+      CALL(@1, @5, expr_binary(OR));
+    }
+    | T_KW_NOT '(' AtlExpression ')' {
+      CALL(@1, @4, expr_unary(NOT));
+    }
+    | Expression;
+
+AtlExpression:
+    NonTypeId { CALL(@1, @1, expr_identifier($1)); } T_FREEZE AtlExpressionOrExpression {
+        CALL(@1, @3, expr_binary(FREEZE));
+    }
+    | T_LSHIFT PlayerColorList T_RSHIFT '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' {
+        CALL(@1, @8, expr_atl($2, ATL_ENFORCE_UNTIL));
+    }
+    | '[' '[' PlayerColorList ']' ']' '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' {
+        CALL(@1, @10, expr_atl($3, ATL_DESPITE_UNTIL));
+    }
+    | T_LSHIFT PlayerColorList T_RSHIFT T_DIAMOND AtlExpressionOrExpression {
+        CALL(@1, @5, expr_atl($2, ATL_ENFORCE_F));
+    }
+    | '[' '[' PlayerColorList ']' ']' T_DIAMOND AtlExpressionOrExpression {
+        CALL(@1, @7, expr_atl($3, ATL_DESPITE_F));
+    }
+    | T_LSHIFT PlayerColorList T_RSHIFT T_BOX AtlExpressionOrExpression {
+        CALL(@1, @5, expr_atl($2, ATL_ENFORCE_G));
+    }
+    | '[' '[' PlayerColorList ']' ']' T_BOX AtlExpressionOrExpression {
+        CALL(@1, @7, expr_atl($3, ATL_DESPITE_G));
+    }
+    | T_LSHIFT PlayerColorList T_RSHIFT 'X' AtlExpressionOrExpression {
+        CALL(@1, @5, expr_atl($2, ATL_ENFORCE_NEXT));
+    }
+    | '[' '[' PlayerColorList ']' ']' 'X' AtlExpressionOrExpression {
+        CALL(@1, @7, expr_atl($3, ATL_DESPITE_NEXT));
+    }
+;
 
 Assignment:
         Expression AssignOp Expression {
@@ -1733,8 +1791,12 @@ Query:
 BoolOrKWAnd:
         T_KW_AND | T_BOOL_AND;
 
+BoolOrKWOr:
+        T_KW_OR | T_BOOL_OR;
+
 SubProperty:
-        T_AF Expression {
+    AtlExpression
+    | T_AF Expression {
 	    CALL(@1, @2, expr_unary(AF));
 	}
         | T_AG '(' Expression BoolOrKWAnd T_AF Expression ')' {
diff --git a/src/prettyprinter.cpp b/src/prettyprinter.cpp
index 20f4cc05..ba4be443 100644
--- a/src/prettyprinter.cpp
+++ b/src/prettyprinter.cpp
@@ -540,10 +540,10 @@ void PrettyPrinter::proc_update() { update = st.size(); }
 void PrettyPrinter::proc_edge_begin(const char* from, const char* to, const bool control)
 
 {
-    proc_edge_begin(from, to, control, nullptr);
+    proc_edge_begin(from, to, control, nullptr, nullptr);
 }
 
-void PrettyPrinter::proc_edge_begin(const char* source, const char* target, const bool control, const char* actname)
+void PrettyPrinter::proc_edge_begin(const char* source, const char* target, const bool control, const char* color, const char* actname)
 {
     if (first) {
         // this is the first transition
diff --git a/src/property.cpp b/src/property.cpp
index 6f174190..abda815f 100644
--- a/src/property.cpp
+++ b/src/property.cpp
@@ -478,4 +478,22 @@ void TigaPropertyBuilder::imitation(const char* id)
 void TigaPropertyBuilder::expr_optimize(int, int, int, int)
 {
     // nothing for now
-}
\ No newline at end of file
+}
+void AtlPropertyBuilder::typeProperty(UTAP::expression_t expr)
+{
+    switch (expr.get_kind()) {
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL:
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT:
+    case FREEZE:
+        properties.back().type = quant_t::Atl;
+        break;
+    default:
+        TigaPropertyBuilder::typeProperty(expr);
+    }
+}
diff --git a/src/typechecker.cpp b/src/typechecker.cpp
index 553f3463..e8980608 100644
--- a/src/typechecker.cpp
+++ b/src/typechecker.cpp
@@ -26,6 +26,7 @@
 #include "utap/utap.h"
 
 #include <cassert>
+#include <array>
 
 using namespace UTAP;
 using namespace Constants;
@@ -994,6 +995,15 @@ void TypeChecker::visitInstance(instance_t& instance)
 static bool isGameProperty(expression_t expr)
 {
     switch (expr.get_kind()) {
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL:
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT:
+    case FREEZE:
     case CONTROL:
     case SMC_CONTROL:
     case EF_CONTROL:
@@ -1770,6 +1780,8 @@ bool TypeChecker::checkExpression(expression_t expr)
             type = type_t::create_primitive(GUARD);
         } else if (is_constraint(expr[0]) && is_constraint(expr[1])) {
             type = type_t::create_primitive(CONSTRAINT);
+        } else if (is_formula(expr[0]) && is_formula(expr[1])) {
+            type = type_t::create_primitive(FORMULA);
         }
         break;
 
@@ -1779,6 +1791,18 @@ bool TypeChecker::checkExpression(expression_t expr)
         }
         break;
 
+    case FREEZE:
+        if (!is_clock(expr[0])) {
+            handleError(expr, "Left-hand side of freeze operator must be a clock");
+            return false;
+        }
+        if (!is_formula(expr[1])) {
+            handleError(expr, "Right-hand side of freeze operator must be a formula");
+            return false;
+        }
+        type = type_t::create_primitive(FORMULA);
+        break;
+
     case SPAWN: {
         template_t* temp = document.find_dynamic_template(expr[0].get_symbol().get_name());
         if (!temp) {
@@ -1918,6 +1942,8 @@ bool TypeChecker::checkExpression(expression_t expr)
             type = type_t::create_primitive(Constants::BOOL);
         } else if (is_constraint(expr[0])) {
             type = type_t::create_primitive(CONSTRAINT);
+        } else if (is_formula(expr[0])) {
+            type = type_t::create_primitive(FORMULA);
         }
         break;
 
@@ -2221,6 +2247,53 @@ bool TypeChecker::checkExpression(expression_t expr)
         }
         break;
 
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL:
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT: {
+        bool isUntil = expr.get_kind() == ATL_ENFORCE_UNTIL || expr.get_kind() == ATL_DESPITE_UNTIL;
+        int numPlayer = expr.get_size() - (isUntil ? 2 : 1);
+        std::array<std::pair<const char*, int32_t >, 11> color_map {{
+            {"black", 0x000000},
+            {"lightgray", 0xc0c0c0},
+            {"darkgray", 0xa9a9a9},
+            {"red", 0xff0000},
+            {"green", 0x00ff00},
+            {"blue", 0x0000ff},
+            {"yellow", 0xffff00},
+            {"cyan", 0x00ffff},
+            {"magenta", 0xff00ff},
+            {"orange", 0xffa500},
+            {"pink", 0xffc0cb},
+        }};
+        std::array<bool, 11> used{};
+        for (int i = 0; i < numPlayer; ++i) {
+            const auto& str = expr[i].get_string_value();
+            bool found = false;
+            for (int j = 0; j < color_map.size(); ++j) {
+                auto [name, hex] = color_map[j];
+                if (str == name) {
+                    expr[i] = expression_t::create_constant(hex, expr.get_position());
+                    if (used[j]) {
+                        handleError(expr[i], "$Atl_player_color_used_twice");
+                    }
+                    used[j] = found = true;
+                    break;
+                }
+            }
+            if (!found) {
+                handleError(expr[i], "$Atl_unknown_player_color");
+            }
+        }
+        if (is_formula(expr[numPlayer]) && (!isUntil || is_formula(expr[numPlayer + 1]))) {
+            type = type_t::create_primitive(FORMULA);
+        }
+        break;
+    }
     case AF:
     case AG:
     case EF:
diff --git a/src/xmlreader.cpp b/src/xmlreader.cpp
index 08bf03c7..e56f3f48 100644
--- a/src/xmlreader.cpp
+++ b/src/xmlreader.cpp
@@ -1050,6 +1050,10 @@ bool XMLReader::transition()
             bool control = (type == nullptr || (strcmp(type, "true") == 0));
             xmlFree(type);
 
+            char* color_raw = getAttribute("color");
+            auto color = std::string{color_raw ? color_raw : "#000000"};
+            xmlFree(color_raw);
+
             char* id = getAttribute("action");
             auto actname = std::string{id ? id : "SKIP"};
             xmlFree(id);
@@ -1058,7 +1062,7 @@ bool XMLReader::transition()
             std::string from = source();
             std::string to = target();
 
-            parser->proc_edge_begin(from.c_str(), to.c_str(), control, actname.c_str());
+            parser->proc_edge_begin(from.c_str(), to.c_str(), control, color.c_str(), actname.c_str());
             while (label())
                 ;
             while (begin(tag_t::NAIL))
diff --git a/test/test_parser.cpp b/test/test_parser.cpp
index 9d6a208e..50c7254c 100644
--- a/test/test_parser.cpp
+++ b/test/test_parser.cpp
@@ -536,4 +536,155 @@ TEST_CASE("Increment with multiple array subscripting and dot accessing")
                    .parse();
 
     CHECK_MESSAGE(doc->get_errors().size() == 0, doc->get_errors().at(0).msg);
-}
\ No newline at end of file
+}
+
+TEST_CASE("T-ALT properties")
+{
+    auto doc = std::make_unique<UTAP::Document>();
+    auto builder = std::make_unique<UTAP::AtlPropertyBuilder>(*doc);
+    SUBCASE("Basic EnforceUntil property")
+    {
+        auto res = parseProperty("<< red, green >> [ true U false ]", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 4);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_UNTIL);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Basic DespiteUntil property")
+    {
+        auto res = parseProperty("[[ red, green ]] [ true U false ]", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 4);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_UNTIL);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Basic EnforceF property")
+    {
+        auto res = parseProperty("<<magenta, blue>> <> true", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 3);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Basic DespiteF property")
+    {
+        auto res = parseProperty("[[cyan, yellow]] <> true", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 3);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_F);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Basic EnforceG property")
+    {
+        auto res = parseProperty("<<black, orange>> [] true", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 3);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_G);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Basic DespiteG property")
+    {
+        auto res = parseProperty("[[lightgray, darkgray]] [] true", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 3);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_G);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Basic EnforceNext property")
+    {
+        auto res = parseProperty("<<red, cyan>> X true", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 3);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_NEXT);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Basic DespiteNext property")
+    {
+        auto res = parseProperty("[[pink, green]] X true", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 3);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_NEXT);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Repeated player color error")
+    {
+        auto res = parseProperty("<<red, red>> <> true", builder.get());
+        REQUIRE(res == 0);
+        CHECK(doc->get_errors().size() == 1);
+    }
+    SUBCASE("Unknown player color error")
+    {
+        auto res = parseProperty("[[red, giraffe]] [] true", builder.get());
+        REQUIRE(res == 0);
+        CHECK(doc->get_errors().size() == 1);
+    }
+    SUBCASE("Nested ATL until property")
+    {
+        auto res = parseProperty("<<red>> [(<<blue>> <> true) U false]", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 3);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_UNTIL);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Nested ATL eventually property")
+    {
+        auto res = parseProperty("<<red>> <> ([[blue]] <> false)", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 2);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Nested ATL property with negation")
+    {
+        auto res = parseProperty("<<red>> <> not ([[blue]] <> false)", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 2);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+    SUBCASE("Nested ATL property with logical operators")
+    {
+        auto res = parseProperty("<<red>> <> (<<blue>> [] false && true) || ([[black]] [(<<cyan>> <> true) && true U false])", builder.get());
+        REQUIRE(res == 0);
+        REQUIRE(doc->get_errors().empty());
+        auto expr = &builder->getProperties().front();
+        CHECK(expr->intermediate.get_size() == 2);
+        CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F);
+        CHECK(expr->type == UTAP::quant_t::Atl);
+    }
+}
+
+TEST_CASE("Freeze operator")
+{
+    auto doc = document_fixture{}
+                   .add_global_decl("clock x;")
+                   .add_default_process()
+                   .parse();
+
+    auto builder = std::make_unique<UTAP::AtlPropertyBuilder>(*doc);
+    auto res = parseProperty("x @ true", builder.get());
+    REQUIRE(res == 0);
+    REQUIRE(doc->get_errors().empty());
+}