In this work, we investigate a variant of the Four Glasses Puzzle (FGP) through the lens of formal verification. Although the puzzle appears to be unsolvable at first glance, formal verification enables the discovery of a correct solution. We demonstrate how the model can be constructed and reduced through progressive abstractions, ultimately yielding a concise and comprehensible model that captures all possible puzzle configurations. This last model is easy to understand, even for non-specialists. Finally, by analysing the strategic capabilities of the player, we present a solution to the puzzle.
• After each turn, the tray is randomly rotated, eliminating any positional reference. • The solution must guarantee success in a finite number of steps, without relying on luck.
The puzzle can be analyzed through the lens of game theory and theoretical computer science. The problem can be reinterpreted as a two-player game where Player 1 (the agent) attempts to align the glasses using limited actions, and Player 2 (the environment) introduces uncertainty by randomly rotating the tray after each move. The agent’s lack of positional knowledge creates a scenario of imperfect information, akin to games like poker or robotics under sensor noise.
The puzzle’s elegance has inspired numerous generalizations. In this paper, we focus on a particularly devilish variant of the original one in which the blindfolded person additionnally wears boxing gloves and cannot sense glass orientations—only flip them blindly. This removes tactile feedback, transforming the problem into a purely combinatorial game.
Purpose of this work In this paper, we model the aforementioned devilish variant of the Four Glasses Puzzle through the lens of formal verification of multi-agent systems .
This approach highlights how abstract logical frameworks can be grounded in tangible, intuitive problems. By distilling complex ideas like strategy invariance and partial observability into the bartender’s challenge, we bridge recreational mathematics and formal verification, ofering a concrete entry point to explore theoretical computer science principles. What makes the bartender problem interesting from a verification perspective is that the bartender has no information about the current state of the system. Whatever action they choose must work regardless of how the glasses are actually arranged. This means the strategy cannot depend on the state—it must be the same for all situations that are indistinguishable from the agent’s point of view. In technical terms, the strategy must be uniform.
This idea has a clear analogue in distributed and autonomous systems. In many real-world cases, agents operate with limited or no access to the global state. A robot, a sensor, or a protocol—all must follow a fixed plan that works in all the situations they cannot tell apart. In this sense, finding a uniform winning strategy is like designing a local, deterministic algorithm that guarantees the right outcome under uncertainty.
The bartender puzzle, in this version, becomes a small but sharp illustration of this challenge. It shows how strategy synthesis under partial information connects logic, games, and system design.
We start with introducing a variant of of the Four Glasses Problem. 2.1. A Devilish Variant of the Four Glasses Problem We consider a variant of the Blind Bartender with Boxing Gloves problem [1]. The setup is as follows: four glasses are placed at the corners of a square tray, and each glass is either upright or upside down. A blindfolded person wearing boxing gloves aims to make all the glasses face the same direction.
On each turn, the person may choose one of three actions: flip a single random glass, flip two adjacent random glasses, or flip two random glasses located on opposite corners (i.e. along a diagonal). After declaring the desired action, the corresponding glasses are flipped—but the person receives no feedback and does not know which glasses were afected. If the goal has not been achieved after the move, the tray is rotated by an unknown angle. 2.2. Formal modelling Given this problem description, we can provide a precise mathematical model in the form of a directed graph with labelled edges. The states of the graph will represent one of the 16 possible configurations of the glasses (each glass can be either up or down, yielding 24 possible combinations). Each edge between two states will be labelled with an action. The input state represents the state from which a given action can be performed, while the output state represents one possible result of applying that action to the given input.
Definition 1 (Game). Given a finite set of actions, we define a game = (,→{− } ∈, , ) as a directed graph, where is a set of nodes (states),→{− } ∈ is a set of edges (arcs) labelled by actions, and ⊆ is a set of initial states and ⊆ is a set of final (winning) states. We say that a game is a turn-based two player game if the set is the union of two disjoints set 1 and 2 and for each , ′ ∈ if →− ′, then ∈ 1 ∧ ′ ∈ 2 or ∈ 2 ∧ ′ ∈ 1.
A play in a game is any non-empty alternated sequence 0, 0, 1, . . . of states and actions such that 0 ∈ , and →− +1 for each index ≥ 0 of the play. Moreover, we require that any play ends in a state if the play is finite, and we call histories finite plays.
A strategy for a player is a function that takes as input a history ending in a state ∈ and outputs an action that labels an edge leaving . A play = 0, 0, 1, . . . is compatible with a strategy if for every index of the play, if ∈ then (0, 0, . . . , − 1, ) = . For each state , by (, ) we denote the set of all maximal (w.r.t. the prefix order) plays starting in that are compatible with the strategy .
We say that a strategy for a player is uniform if it returns the same output for plays that are indistinguishable to the given player. We say that a uniform strategy is winning if the paths compatible with it, starting from any initial state, are all finite.
Our bartender acts without having any information about the current state of the game. Therefore, his strategy should not depend on the current configuration of the game: in other words, the strategy must return the same output for all plays that it cannot distinguish. Remark that in our context two plays are indistinguishable for the bartender if they have the same length, and that all actions are enabled in all three indistinguishable states (see the final attempt), and no action is enabled in the winning states.
First attempt. Now that we have defined the mathematical model for representing the game, let us proceed to its concrete representation. Given that the bartender problem involves two players, it is natural to model it as a turn-based two-player game. To do so, we need to define two disjoint sets of states, each representing the possible configurations of the glasses on the tray. A natural choice is to consider for each of the two sets, the 2×2 matrices over a two-elements set.
Thus we define the first version of the bartender game, 1, as follows. The set of states is defined as the union of the set 1 of 2 × 2 matrices over {0, 1} and the set 2 of 2 × 2 matrices over {, }. The set of actions consists of two main types:
= {t1, t2a, t2d} ∪ {ri | ∈ {0, 90, 180, 270}}, where t1 corresponds to flipping a single glass, t2a to flipping two adjacent glasses, and t2d to flipping two diagonal glasses. Each ri element represents the rotation of the tray by degrees, with ∈ {0, 90, 180, 270}.
To model the transitions between these configurations, we define the edges, which describe how the game state changes due to the actions of the bartender and of the other player. Consider a map that maps 0 to and 1 to , we define the following rules for the transitions, for any matrix diferent from the unit and the zero one: • →−t1 ′ with ∈ 1 if there exists exactly one position (, ) such that ( ) ̸= ′ , and for all other positions (, ) ̸= (, ), we have () = ′. In other words, a single glass is lfipped, and all other glasses remain untouched.
t2d
• →−− ′ with ∈ 1 if there exists a diagonal ∈ {{(
function .
For example:
• →−−
′ with
∈
1 if there exists a pair of adjacent positions
∈
lfipping two adjacent glasses, either horizontally or vertically.
{{(
The set of initial states of 1 is 1 without the zero and the unit matrices. The set of final states Remark: The only states with no outgoing transitions are the final states, corresponding to the bartender’s tray with all glasses upside-down (the zero matrix) and the one with all glasses upright (the unit matrix), i.e. those states where the bartender wins. Given this, asking for a solution to the blind bartender problem with boxing gloves is equivalent to asking the following: we have that each ∈ (, ) is finite?
Question: is there a uniform strategy for player 1 such that for any initial state of 1 Note that this solution has lots of states and transitions, therefore, we do not visualize it. and some action .
Second attempt
Although 1 faithfully represents the turn-based structure of the original game, it is somewhat forced. We had to artificially duplicate the number of states in order to have one set of states from which the bartender can make a move and another set of states from which the other player can act. Fortunately, we can easily address this modeling issue. For any triple of states in the model described above, , , and , if ∈ 1 and →− →− , then ∈ 1, and if ∈ 2 and →− →− , then ∈ 2, since the game is turn-based.
Thus, we can consider a simpler model, which we will call 2, where the set of states is simply 1, the set of actions consists of the three actions of the bartender, the set of initial states is equal to the set of initial states in 1 and →− in 2 if and only if ∈ 1 and →− →− in 1 for some ∈ 2 transitions), so we do not show it.
Given a play on 1, let denote its subsequence containing only states in 1 and actions of the bartender. We have that for every play in 1, is a play in 2, and conversely, for any play in 2, there exists a play in 1 such that = . Furthermore, note that any strategy for the bartender on 1 can be applied to 2. From the observations above, we immediately obtain the following: Proposition 1. There is a winning strategy on 1 if and only if there is a winning strategy on 2.
Even if 2 is smaller than 1, as it shows only the bartender, it is still huge (16 states and many Third (and final) attempt The model just described is certainly more eficient than the first one. In this model, we did not have to unnecessarily multiply the number of states, and we simply modelled the second player by introducing greater non-determinism in the transition relation: given an action and a state, the set of possible outcomes consists of all possible rotations of the tray after the action is performed. However, this model is still not optimal, and we can do better. From the bartender’s perspective, the two configurations where all glasses are either up or down are equivalent: in both cases, the bartender wins. Similarly, the two configurations with two glasses facing one way along a diagonal and two facing the other way are equivalent for the bartender, and so on. To be short, in the Four Glasses with Boxing Gloves Problem, the equivalence between configurations is determined by the symmetry of the 2x2 grid of glasses. This includes rotations (0°, 90°, 180°, 270°) and flipping (inverting the positions of all glasses). The bartender’s goal is to move the glasses in a way that either all are facing up or all are facing down, regardless of their initial orientation. Rotating or flipping the grid does not fundamentally change the problem because the relative positions of the glasses and the actions needed to achieve the goal remain the same. As such, configurations that are rotations or reflections (flips) of each other are considered equivalent, meaning that they require the same strategy to solve.
To sum up: (≡ ) From the bartender’s point of view, two tray configurations M and M’ (with four glasses on the tray) are equivalent if M’ can be obtained by rotating M by 0°, 90°, 180°, or 270°, and flipping all the glasses (changing each glass from up to down, or the other way around).
The equivalence classes generated by the relation defined above can be visualized in Table 1.
Class
Given this, we can define the third (and final) model of the blind bartender with boxing gloves. Let us call this model 3. The set of actions for 3 consists of the three actions of the bartender, the set of states only counts four states ℓ1, ℓ2, ℓ3, and ℓ4. Each of these states represents an equivalence class of glasses on the tray modulo the above-defined relation. In particular, 1. ℓ1 represents the class in which three glasses are equal and one diferent, 2. ℓ2 represents the class of checkerboard patterns, 3. ℓ3 represents the class of configurations with two adjacent equal glasses, 4. ℓ4 represents the class of configurations in which all glasses are equal.
The set of initial states is equal to {ℓ1, ℓ2, ℓ3}. Finally ℓ→− ℓ if there is a state in the class represented by ℓ and a state ′ in the class represented by ℓ such that →− ′ in 2. A representation of 3 is shown in Figure 1. Given the definition of the model, it is fairly immediate to prove the following: Proposition 2. There is a winning strategy on 1 if and only if there is a winning strategy on 3.
So, solving the Blind Bartender with Boxing Gloves Problem comes down to finding a uniform strategy—a fixed sequence of actions that does not rely on knowing the current state—guaranteeing that, no matter the starting configuration, the system eventually reaches the goal state ℓ4.
This problem can be formalised in strategic logics (see [5] for an introduction) as ⟨⟨⟩⟩ ℓ4. This formula states that there exists a strategy (operator ⟨⟨ ⟩⟩) of the model which ensures that ℓ4 is eventually reached (operator ). We consider the following semantics: t2a,t2d t2d ℓ1ℓ3 t 2 a t1 t 2 a ℓ1ℓ2 d 2 t t1
ℓ1 t1 t2a,t2d
• perfect recall: the bartender remembers the sequence of actions he has played.
Let us analyse the behaviour of the system, starting from ℓ1ℓ2ℓ3 (remember the bartender does not know the actual starting point). It is pictured in Fig. 2. Starting from this state, all operations are possible from either ℓ1, or ℓ2, or ℓ3. When taking t1, the bartender can win by getting directly in ℓ4, which is possible from ℓ1 only. Or it can lead to ℓ1 from ℓ2 and ℓ3 ; or to ℓ2 from ℓ1 ; or to ℓ3 from ℓ1. To summarise, from the initial state t1 gets either to win of to any of the three states ℓ1, ℓ2 and ℓ3, without yet any possibility to distinguish them, hence the self-loop on the initial state. Consider now t2d. If in ℓ1, we stay there. From ℓ2 it leads to the winning state ℓ4. If in ℓ3, we stay there. Hence, either we get to win, or we know that we are in ℓ1 or ℓ3, thus the state ℓ1ℓ3 in Fig. 2. Repeating such a reasoning from ℓ1ℓ3 (and so on) allows for constructing the graph in Fig. 2.
The idea here is to find a sequence of actions that necessarily goes to ℓ4. Notice that in the graph of Fig. 2, the bartender may gain knowledge (e.g. can know that the current state is ℓ1) but due to non-determinism, may again lose exact information (e.g. ℓ2ℓ3 is a successor of ℓ1). Choosing an action that may get you to an already visited state in the graph does not help, so we will instead privilege progress. Thus, initially, the bartender will choose action t2d: either the game is immediately won, or the state is ℓ1 or ℓ3, but they cannot be distinguished at this stage. From there, choosing t2d does not help, choosing t1 may win (if the bartender is lucky) or get back to the initial situation. Hence the bartender chooses to progress with t2a. We continue in a similar manner and obtain the following strategy for winning:
t2d, t2a, t2d, t1, t2d, t2a, t2d Note that this strategy is minimal, but other ones exist, including for example a cycle in the graph.
Several semantics exist for strategic abilities (see [5]), some of them being undecidable in general. Depending on the semantics, a winning strategy could be computed using a tool that supports reasoning under imperfect information, such as MCMAS [6] or STV [7, 8].
and variable domains are : ∈ {ℓ1, ℓ2, ℓ3}, ∈ {ℓ1, ℓ3}.
One could argue that the transition t2d which is not leading to the winning state is useless, but this is not the case: it represents a permitted action on ℓ1 and ℓ3 which has no efect.
Another possibility would have been to use a single place (with a slight modification of the functions used on arcs), and winning the game would resume to the reachability of marking ℓ4 in the sole place.
In this paper, we have presented progressively abstracted models for the Four Glasses Puzzle and demonstrated how they can be used to derive a winning strategy for this seemingly unsolvable problem. The puzzle has been employed with the general public—first as a magic trick, and then as a teaching t2d ℓ4 t2a ℓ3 t1 t1 t2d t1 t2a t2a ℓ1 ℓ2 t1 t1 t2a t2d
t2a 2()
t2d t1 1() ℓ2 t2d ℓ4 tool to illustrate how formal modelling and verification can be leveraged to uncover a solution, thereby demystifying mathematical approaches.
As possible extensions, this methodology could be adapted to incorporate timing constraints [9, 10, 11], enabling the discovery of strategies that succeed within a specified time frame. Another interesting direction would be to generalize the puzzle to accommodate any number of glasses. In such a case, Coloured Petri Nets would provide a suitable framework for encoding tray configurations as tuples attached to tokens, similar to what was presented in Section 3.
This work was supported by: CNRS IRP “Le Trójkąt”, the ANR-22-CE48-0012 project BISOUS, the PHC Polonium project MoCcA (BPN/BFR/2023/1/00045).
The author(s) have not employed any Generative AI tools.