From 7e2609e8282d091c2217dce9c3d41d1ceb1d5f12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98=20Jensen?= Date: Thu, 30 Oct 2025 14:01:25 +0100 Subject: [PATCH 1/4] Add TATL documentation --- .../query-syntax/controller_synthesis.md | 80 +++++++++++++++++++ 1 file changed, 80 insertions(+) diff --git a/content/language-reference/query-syntax/controller_synthesis.md b/content/language-reference/query-syntax/controller_synthesis.md index efa01812..fa883494 100644 --- a/content/language-reference/query-syntax/controller_synthesis.md +++ b/content/language-reference/query-syntax/controller_synthesis.md @@ -15,6 +15,7 @@ ControlQuery ::= | PartialControlSpecifier Goal Subjection | TimeEfficientGameSpecifier Goal | ApproximateControlSpecifier // In section below + | TatlExpression // In section below ControlSpecifier ::= 'control:' @@ -115,3 +116,82 @@ strategy shield = acontrol: A[] water_level < 10 && water_level > 0 { WaterTank. ``` Declares a strategy called `shield` to enforce the desired invaraint `water_level < 10 && water_level > 0`. The system has two, state variables. First, the `WaterTank` template has 5 locations, so `WaterTank.location` has 5 possible values. The second variable, `water_level[-1, 11]:24` is a double which gets split up into 24 intervals, with the corresponding size of 0.5. So the partition will contain `5·24 = 120` cells. + + +### Timed Alternating-Time Temporal Logic (TATL) + +{{% notice info %}} +TATL queries are available in the UPPAAL TATL version only. +{{% /notice %}} + +{{% notice info %}} +Due to some yet-to-be resolved parsing conflicts, TATL sub-expressions are wrapped in parenthesis if they themselves are also valid TATL expressions. +{{% /notice %}} + +```EBNF +TatlExpression ::= + Identifier '¤' TatlExpressionOrExpression // (A) + | TatlCoalitition TatlPathProp + ; + +TatlCoalitition ::= + '<<' PlayerColorList '>>' // (B1) + | '[[' PlayerColorList ']]' // (B2) + ; + +TatlPathProp ::= + '[' TatlExpressionOrExpression 'U' TatlExpressionOrExpression ']' // (C1) + | '<>' TatlExpressionOrExpression // (C2) + | '[]' TatlExpressionOrExpression // (C3) + | 'X' TatlExpressionOrExpression // (C4) + ; + +TatlExpressionOrExpression ::= + '(' TatlExpression ')' + | '(' TatlExpression ')' BoolOrKWAnd TatlExpressionOrExpression + | '(' TatlExpression ')' BoolOrKWOr TatlExpressionOrExpression + | '!' '(' TatlExpression ')' + | Expression + ; + +PlayerColorList ::= + /* empty */ + | PlayerColor + | PlayerColorList ',' PlayerColor + ; + +PlayerColor ::= + 'black' | 'lightgray' | 'darkgray' | 'red' | 'green' | 'blue' | 'yellow' | 'cyan' | 'magenta' | 'orange' | 'pink' ; +``` + +Alternating-Time Temporal (ATL) logic is an extension of computation-tree logic (CTL), where the traditional for-all- and exists path quantifiers have been replaced with outcome quantifiers, quantifying over the possible outcome paths resulting from a coalition of players working together. The timed extension comes from the addition of the freeze operator. + +- **(A) The freeze operator.** The left-hand side must be a globally defined clock that is not used in any automata (undefined behavior otherwise). `z ¤ RHS` is satisfied if the right-hand side is satisfied after the clock `z` is reset in the current state. +- **(B) Outcome quantifiers.** + - `<< S >> rho` (B1) is satisfied if there *exists* strategies for the players `S` such that *all* outcome paths satisfies path property `rho`. + - `[[ S ]] rho` (B2) is satisfied if there *exists* an outcome path satisfying `rho` for *all* strategies the players `S`. + - Empty clauses: `<< >>` is equivalent to `A`, and `[[ ]]` is equivalent to `E`. +- **(C) Path Properties.** Your typical CTL temporal operators. Note that `X` is *next location*. + +#### Players + +TATL queries are defined over timed *multi-player* games. A TATL query considers each edge color a different player (it does not matter if an edge is marked uncontrollable). +There are 11 different edge colors available in the UPPAAL GUI and they are referred to using their natural language name, i.e. `red`, `green`, `blue`, etc. + +The semantics are similar to that of a standard 2-player game. The player `red` may activate enabled red edges at any time, and must do it in a timed-locked state. +If two players activate an edge in the same instant, it is non-deterministic which activation happens. +If a synchronization involves more than one player, it is consider "uncontrollable". + +#### Examples + +`<< green >> [] safe` +: satisfied if there exists a strategy for `green` such that only `safe` states are visited (despite the actions of other players). + +`[[ red ]] [ safe U goal ]` +: satisfied if the system *can* stay in `safe` states until eventually reaching a `goal` state despite the actions of player `red`. + +`<<>> [] (<> <> goal)` +: satisfied if in all reachable states `red` and `blue` can cooperate such that `goal` is eventually reached. + +`z ¤ (<< green, blue >> [ (safe && z <= 5) U goal ])` +: satisfied if `green` and `blue` can cooperate to reach a `goal` state within 5 time units and only visiting `safe` states along the way (`z` is a global clock). \ No newline at end of file From a1cd38dd892e13df7552f92fe07dc5e21384f449 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98=20Jensen?= Date: Wed, 5 Nov 2025 11:44:37 +0100 Subject: [PATCH 2/4] Fix typo and clarify semantics --- .../query-syntax/controller_synthesis.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/content/language-reference/query-syntax/controller_synthesis.md b/content/language-reference/query-syntax/controller_synthesis.md index fa883494..514c67fe 100644 --- a/content/language-reference/query-syntax/controller_synthesis.md +++ b/content/language-reference/query-syntax/controller_synthesis.md @@ -131,10 +131,10 @@ Due to some yet-to-be resolved parsing conflicts, TATL sub-expressions are wrapp ```EBNF TatlExpression ::= Identifier '¤' TatlExpressionOrExpression // (A) - | TatlCoalitition TatlPathProp + | TatlCoalition TatlPathProp ; -TatlCoalitition ::= +TatlCoalition ::= '<<' PlayerColorList '>>' // (B1) | '[[' PlayerColorList ']]' // (B2) ; @@ -171,16 +171,16 @@ Alternating-Time Temporal (ATL) logic is an extension of computation-tree logic - `<< S >> rho` (B1) is satisfied if there *exists* strategies for the players `S` such that *all* outcome paths satisfies path property `rho`. - `[[ S ]] rho` (B2) is satisfied if there *exists* an outcome path satisfying `rho` for *all* strategies the players `S`. - Empty clauses: `<< >>` is equivalent to `A`, and `[[ ]]` is equivalent to `E`. -- **(C) Path Properties.** Your typical CTL temporal operators. Note that `X` is *next location*. +- **(C) Path Properties.** Your typical CTL temporal operators. Note that `X` is the next *location* operator. #### Players TATL queries are defined over timed *multi-player* games. A TATL query considers each edge color a different player (it does not matter if an edge is marked uncontrollable). There are 11 different edge colors available in the UPPAAL GUI and they are referred to using their natural language name, i.e. `red`, `green`, `blue`, etc. -The semantics are similar to that of a standard 2-player game. The player `red` may activate enabled red edges at any time, and must do it in a timed-locked state. +The semantics are similar to that of a standard 2-player game. The player `red` may activate enabled red edges at any time, and must do it in a timed-locked state, if any is enabled. If two players activate an edge in the same instant, it is non-deterministic which activation happens. -If a synchronization involves more than one player, it is consider "uncontrollable". +If a synchronization involves more than one player, it is consider "uncontrollable", unless they are all working together. #### Examples From ed8e8a9ff553d39600e12a4751bf3de805db3d07 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98=20Jensen?= Date: Wed, 5 Nov 2025 11:48:46 +0100 Subject: [PATCH 3/4] Fix another typo --- content/language-reference/query-syntax/controller_synthesis.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/language-reference/query-syntax/controller_synthesis.md b/content/language-reference/query-syntax/controller_synthesis.md index 514c67fe..6a7b94f2 100644 --- a/content/language-reference/query-syntax/controller_synthesis.md +++ b/content/language-reference/query-syntax/controller_synthesis.md @@ -168,7 +168,7 @@ Alternating-Time Temporal (ATL) logic is an extension of computation-tree logic - **(A) The freeze operator.** The left-hand side must be a globally defined clock that is not used in any automata (undefined behavior otherwise). `z ¤ RHS` is satisfied if the right-hand side is satisfied after the clock `z` is reset in the current state. - **(B) Outcome quantifiers.** - - `<< S >> rho` (B1) is satisfied if there *exists* strategies for the players `S` such that *all* outcome paths satisfies path property `rho`. + - `<< S >> rho` (B1) is satisfied if there *exist* strategies for the players `S` such that *all* outcome paths satisfies path property `rho`. - `[[ S ]] rho` (B2) is satisfied if there *exists* an outcome path satisfying `rho` for *all* strategies the players `S`. - Empty clauses: `<< >>` is equivalent to `A`, and `[[ ]]` is equivalent to `E`. - **(C) Path Properties.** Your typical CTL temporal operators. Note that `X` is the next *location* operator. From a7f7e67d6edc6be67aa6e8594becc83a85a58d86 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98=20Jensen?= Date: Wed, 5 Nov 2025 16:18:53 +0100 Subject: [PATCH 4/4] Change freeze operator to @ --- .../language-reference/query-syntax/controller_synthesis.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/content/language-reference/query-syntax/controller_synthesis.md b/content/language-reference/query-syntax/controller_synthesis.md index 6a7b94f2..d6c4f5d8 100644 --- a/content/language-reference/query-syntax/controller_synthesis.md +++ b/content/language-reference/query-syntax/controller_synthesis.md @@ -130,7 +130,7 @@ Due to some yet-to-be resolved parsing conflicts, TATL sub-expressions are wrapp ```EBNF TatlExpression ::= - Identifier '¤' TatlExpressionOrExpression // (A) + Identifier '@' TatlExpressionOrExpression // (A) | TatlCoalition TatlPathProp ; @@ -166,7 +166,7 @@ PlayerColor ::= Alternating-Time Temporal (ATL) logic is an extension of computation-tree logic (CTL), where the traditional for-all- and exists path quantifiers have been replaced with outcome quantifiers, quantifying over the possible outcome paths resulting from a coalition of players working together. The timed extension comes from the addition of the freeze operator. -- **(A) The freeze operator.** The left-hand side must be a globally defined clock that is not used in any automata (undefined behavior otherwise). `z ¤ RHS` is satisfied if the right-hand side is satisfied after the clock `z` is reset in the current state. +- **(A) The freeze operator.** The left-hand side must be a globally defined clock that is not used in any automata (undefined behavior otherwise). `z @ RHS` is satisfied if the right-hand side is satisfied after the clock `z` is reset in the current state. - **(B) Outcome quantifiers.** - `<< S >> rho` (B1) is satisfied if there *exist* strategies for the players `S` such that *all* outcome paths satisfies path property `rho`. - `[[ S ]] rho` (B2) is satisfied if there *exists* an outcome path satisfying `rho` for *all* strategies the players `S`. @@ -193,5 +193,5 @@ If a synchronization involves more than one player, it is consider "uncontrollab `<<>> [] (<> <> goal)` : satisfied if in all reachable states `red` and `blue` can cooperate such that `goal` is eventually reached. -`z ¤ (<< green, blue >> [ (safe && z <= 5) U goal ])` +`z @ (<< green, blue >> [ (safe && z <= 5) U goal ])` : satisfied if `green` and `blue` can cooperate to reach a `goal` state within 5 time units and only visiting `safe` states along the way (`z` is a global clock). \ No newline at end of file