Hello, I'm Cata and Dima from the University of Paris-Creté, and I will present our paper on Hennessy Milner Theorem for Alternating Temporal Logic with Imperfect Information,

which is a joint paper by Francesco Bartinelli from the Imperial College London, Vadim Malgone from the University of Paris-Creté, and Harucho Sigra from the University of Riesz, Romania. The outline of this presentation is the following, after briefly calling the Hennessy Milner Theorem for the case of classical bi-simulation. I will recall several

variations of the semantics of the Alternating Temporal Logic with Imperfect Information and the bi-simulations introduced for imperfect and imperfect information. Then I will state the Hennessy Milner Theorem for ACL with Imperfect Information and concentrate on some elements of the proofs, among which the construction of a four-player

bi-simulation game with Imperfect Information and the proof of the determinacy of that game. I will also briefly present the undecidability of bi-simulation with Imperfect Information and then some went with some concluding remarks and directions for further work.

Recall that a bi-simulation is a relation on states of one or two transition systems, which has the diamond property, stating that whenever state Q can make any transition to state R in the first system, and Q is simulated by state Q' in the second system,

then there exists a state R' in the second system, which simulates state R, and Q' can make an A-transition to R'. Then Hennessy Milner Theorems for label transition systems has two implications, the first stating that the bi-simulation preserves the satisfiability

of modal logic, and the second stating that whenever two systems are relating by the with satisfiability relation, then they are bi-simulating. So our aim is to adapt this setting to the case of alternating temporal logic and concurrent game structures with Imperfect Information. It here is a modal logic for expressing the strategic abilities

of coalitions of angles, and its semantics can be given on concurrent game structures, which are label transition systems in which each transition bears a triple of labels, one action label for each agent. The modal operators which led by ATL are strategic operators for coalitions, and the semantics of strategic operators for coalition A is that

A has a strategy for accomplishing some sort of formula. So for our simple example is path from matching pennies, two agents having two actions available, each heads and tails, and the winning state being the one in which both agents have played the same action.

The formula displayed states the existence of a strategy for Alice to reach the winning state, which is obviously false since neither of the two strategies for Alice may reach only the winning state. This also gives an opportunity to recall the dual operator which states that

in state zero for any strategy for Alice there exists an outcome which is not winning. On the other hand if we look at coalition power then the two agents by working together can reach the win state by agreeing beforehand to play the same action, for example heads. Suppose now the game proceeds in steps. First Bob plays and Alice is idle,

then Alice plays and Bob is idle. Now Alice has a winning strategy which is to look at what Bob played and then play the same action. This implies that Alice has perfect information of the system state. The ETL with imperfect information introduces agent observability as

a goodless relation between states, with two states being equivalent for Alice when Alice doesn't know whether the system is in one state or the other. In our case it could be because Bob hides his first action from Alice. Then indistinguishable is taken into account at

the semantic level of ETL by considering uniform strategies in which agents play the same action at indistinguishable states or histories. So when Alice does not see what Bob played at the first round she can play only two strategies, heads or tails, at both first moves which means that

with imperfect information she is no longer able to win. The same situation occurs when games have multiple initial states with indistinguishable abilities. For example, we may abstract from Bob's first action by considering two initial states in the game, each state representing both his and Bob's hidden coin. Then again Alice doesn't have a winning strategy since none

of her uniform strategies is winning in both initial states. The subjective semantics of ETL is a generalization of this situation in that it requires for coalitions to play the same uniform strategy from each state which is indistinguishable for one of the agents.

In the displayed example in state two the coalition does not satisfy the formula Alice and Bob can enforce next win since the unique joint winning strategy is not uniform for Bob between the states two and three as Bob's winning action in state two is different from his

winning action in state three which can be interpreted as the fact that Bob does not know when observing state two which action he should play. Not however that the same formula holds in state one since the coalition now does have a uniform strategy applicable in

all states indistinguishable from state one by one of the agents which amounts to Bob knowing exactly the initial state. But do really Alice and Bob know that they may win with the subjective semantics? Well actually no and we have an example here. With the

subjective semantics Alice and Bob win in state one due to the existence of a joint strategy to win from the three states one two and four strategy which is uniform for both Alice and Bob but Alice is not sure that Bob knows what to play. She knows that the system might be in

state one or two based on her observations and while in state one the existence of a uniform action for Bob is guaranteed it is stale which can be consistently applied by Bob in both states one and four which are the observations that Bob can make of state one. This is no longer

the case in state two since based on his observation of the state which is states two or three Bob does not know whether to play heads or tails. The common knowledge semantics capture this by requiring that the joint uniform strategy ensures the desired objective in all

the states of the common knowledge neighborhood of the state where the formula is tested. So let's see how bi-simulations were adapted to the case of perfect information. Assume two concurrent game structures g1 and g2 and suppose we want to simulate strategic abilities of some

coalition in state s of g1 with strategic abilities of the same coalition in s prime. In order to guarantee that any objective which is accomplishable in a state s by coalition a is also accomplishable in state s prime by the same coalition. The idea is to have a way to map each joint strategy sigma for a in s to a joint strategy

sigma prime for a in s prime such that when sigma accomplishes some objective phi sigma prime accomplishes the same objective in s prime and to do this we have to ensure that the set of outcomes of strategy sigma prime are included in the set of outcomes of strategy sigma

that is each run produced by sigma prime in s prime has the same projection on the set of atomic propositions and propositions as some run produced by sigma in s. Note the z exact needed when just proving one way simulation and the quantifier alternation

for each strategy sigma in the first game structure this is such a sigma prime in the second game structure such that for any outcome rho prime of sigma prime there is an outcome rho of sigma such that rho and rho prime have the same projection on the set of atomic propositions

and the way to ensure this in a step-by-step manner is to have a z exact property on joint actions for a correlation and their outcomes as in the finger and we arrived at this variant of alternating by simulation proposed by Allura, Henzinger, Kuferman and Warby for

alternating time-temporal logic in which when state s prime simulates state s some correlation then for each of the correlations joint actions in s there is a joint action for the same correlation in s prime such that each of s prime's outcomes t prime can be

mapped back to one of s outcomes t in such a way that t prime simulates state. For the case of imperfect information we have the following history-based version of a

definition from a previous paper in which when history h prime simulates history h for coalition a then first of all atomic proposition labeling history h prime are the same as the atomic propositions labeling history h then the simulation is compatible with the epistemic

relations like a modern simulation would do and three the simulation is compatible with uniform strategies in a way which generalizes the properties in a case of perfect information and our sketch on the next slide. The place of joint actions in the definition of alternating

by simulation with perfect information is taken by one-step joint uniform strategies for the coalition defined on the whole common knowledge neighborhoods. The idea is that each one-step joint uniform strategy sigma defined on the common knowledge neighborhood of the

simulated strategy must be mapped to a one-step joint uniform strategy sigma prime defined on the whole common knowledge neighborhood of the simulating history such that for any couple of histories which are in the simulation relation and in the respective common knowledge

neighborhoods for example here s2 and s2 prime we have that each target of the sigma prime from s2 prime simulates a target of a sigma transition from s2 for example t3 prime simulates t3 that is the simulation of the effect of a joint one-step uniform strategy has to be

consistent has to have a consistent effect on all couples of simulating states in the

simulation which is both the simulation and the reverse simulation we may then state the desired form of the henna similar theorem for atl with imperfect information which contains two implications for the first one if we fix the coalition and we have a bi-simulation for that correlation between two concurrent gain structures with imperfect information

then any formula which utilizes just the operators for that correlation and is satisfied in a history of g will be also satisfied in a bi-simular history of g prime and vice versa and the reverse property if two histories belonging to two concurrent gain structures with

imperfect information satisfy the same a formulas then there is an a bi-simulation containing that pair of histories note that part one holds for all semantics the part two only holds for the common known semantics and we provide an encounter example

of part two and the subjective semantics in the paper today property can be proved by easy but tedious induction so let's go to the proof of the reverse property for which we introduced the bi-simulation game which is played between four players organized in two

coalitions the spoilers and the duplicators the spoiler coalition has two agents the perfect uniform p-spoiler and i-spoiler which has imperfect information and may have the same structure for duplicator coalition containing p duplicator and i duplicator the positions of

the game are labeled with pairs of histories in the two game structures plus some extra information the moves of the four players simulate the various quantifiers in the definition of the bi-simulation with spoilers simulating the universal quantifier and duplicators simulating the existential quantifier the compatibility of the bi-simulation with the

epistemic relations is encoded in the loop between the two upper positions as follows starting with a pair of histories age h prime which duplicators want to prove by similar p-spoiler chooses a history k prime and an agent a in the coalition such that k prime

is indistinguishable for a from h prime then p-duplicator has to answer by choosing a history k which is indistinguishable from h by the same agent a duplicator must also ensure that the

labeling of the history k with atomic propositions is the same as the labeling of the history k prime in atomic propositions these pairs of mysteries k k prime are gathered in a set of pairs rho which can be thought as a partial function from the common knowledge

neighborhood of history h prime to the common knowledge neighborhood of history h not the reverse direction this stage of the game ends when rho is a total function or p-duplicator file fails in her obligation to ensure the identical labeling

in the second stage we include the third property of by simulations as follows after the set of pairs rho has been completed p-spoiler passes the control to i-spoiler who sees this set of pairs rho and chooses a strategy sigma which is a uniform one-step

joint strategy for coalition a defined on the common knowledge neighborhood of the history h then i-duplicator who sees this sigma and the set of pairs rho must answer with the

strategy sigma prime which is a uniform one-step joint strategy for coalition a defined on the common knowledge neighborhood of the history h prime the control then goes back to the p-spoiler who replaces this pair of histories h h prime with another pair of histories k k prime in the set of pairs rho and then p-spoiler challenges

the p-duplicator by choosing the history l prime which is in the outcome of the strategy sigma prime for history k prime sigma prime in the strategy i-duplicator i have chosen previously

then the p-duplicator must respond with the history l in the outcome of study sigma with for run k and the p-duplicator must also ensure that the labeling with atomic propositions of history l is the same as the labeling with atomic propositions of history l prime

then the play resumes with a new stage involving compatibility with epistemic relations and with the current pair of histories set to l l prime and the set of pairs rho initialized to a single pair composed of l l prime this by simulation game has a mirror

variation in which spoiler choices are in the game structure g the first computer game structure and p-duplicator spoilers and in the game structure g prime and with a similar dualization of the choices of i-spoiler and i-duplicator and also p-spoiler

chooses before starting the first stage of the game whether to play the display variation or the dual variation some comments should be made here on the necessity to have the two imperfectly informed players i-duplicator and i-spoiler first game positions must contain an

information about the pairs of states which the duplicators want to prove by similar secondly the choice of the strategy profile for the a coalition in both games structures must be made independently of the game positions in order to ensure that this is really a new form strategy

for the a coalition this can only be be implemented by utilizing the two imperfectly informed agents i-spoiler for the choice of the challenging strategy sigma and i-duplicator for the correct answer of the simulating strategy sigma prime the by simulation game

behaves as expected in that whenever there existed by an a by simulation between two continuity structures in perfect information containing a pair of histories a0 a0 prime then the duplicators win the appropriate by simulation game with initial position

set to a0 a0 prime conversely if duplicators have a joint strategy to win the by simulation game starting with this pair of positions a0 a0 prime then there is an a by simulation which contains all the input positions compatible with duplicators strategy

furthermore we we also define a equivalence as the binary relation on histories of two structures within perfect information which relates to histories whenever they satisfy the same a from this then a equivalence is an a by simulation so in order to settle the reverse

part from the hennessy minima theorem we have to figure out what happens when there's no a by simulation that is when the duplicators cannot win the by simulation game so this is where we have to rely on a deterministic property for by simulation games note that these games

are a four player version of games since spoilers have a reachability objective and there's finitely many choices at each position so we may follow the proof idea for games but trying to prove that if spoilers do not have a winning strategy then duplicators have

a defensive strategy and then observing that a defensive strategy for duplicators is actually winning due to the particular reachability objective for the spoilers here a defensive strategy for a coalition is a strategy that avoids positions where the opponents have a winning strategy

so then the proof works by induction of the depth of the position in the by simulation game by showing that if position is not winning by the spoilers then there must exist a move by the duplicators that put the game into a position which is still not winning for the spoilers

the difficulty is that we want this joint strategy for the duplicators to be uniform for i duplicator but a priori we might have constructed two different strategic choices for i duplicator in two positions giving him the same information that is this row set of pairs

and this sigma which is the strategic choice for i spoiler but let's have a closer look at such a situation on the left after i duplicators choice of sigma one prime p spoiler can change the current history pair to any other pair k k prime in row

with the resulting position still not being winning to the spoiler coalition then i duplicator should sigma one prime two at the right position which has the same information at the left position and this choice would also be safe there hence i duplicators defensive strategy

can be made uniform so now that we know that by simulation gains that determined whatever spoiler coalition wins we may proceed to identify which formula actually separates the concurrent game structures with important information and this can be done in a step

by step manner by building next time from let's add positions where spoilers can are sure to win in one stage and then nesting these progress the ice cooler winning choice of sigma is encoded in the leading coalition next operator then all i duplicator answers with one step

strategy sigma prime are encoded in this big conjunction then followed by this p spoiler choice of the history k prime which is encoded in the disjunction of the k prime follow followed by the p spoilers choice of l prime encoded in the last part of the formula note that the

formulas builded here and needed it yesterday since spoilers choice of a separating strategy is encoded by the strategic next operator but then p spoilers essential move to replace the current history pair by another requires the reference inside this strategy next formula to the previous

position just taken just before taking the separating strategy we also show that the history based by simulation with perfect information is understandable and the proof utilizes the technique behind the undecidability of model checking for alternating temporal logic with

imperfect information namely we encode each turning machine which starts with an entity as a concurrent game structure this concurrent game structure is then shown a by similar with a simple model in which some correlation has a winning strategy if and only if the turning

machine holds conclusion we have shown that by simulations can be adapted to zero sum games information and to alternating time with imperfect information where combinations of alternating by simulation with perfect information and epistemic by simulation does not work

we also showed that this history based by simulation is undecidable two directions for further work are adapting to strategic logic with imperfect information and generalizing to determine the results to other types of multiplayer it means with imperfect information

thank you