# abstraction_of_situation_calculus_concurrent_game_structures__ae1860f3.pdf

Abstraction of Situation Calculus Concurrent Game Structures

Yves Lesp erance1, Giuseppe De Giacomo2, Maryam Rostamigiv3, Shakil M. Khan3

1York University, Toronto, ON, Canada 2University of Oxford, Oxford, UK 3University of Regina, Regina, SK, Canada lesperan@eecs.yorku.ca, giuseppe.degiacomo@cs.ox.ac.uk, maryam.rostamigiv@uregina.ca, shakil.khan@uregina.ca

We present a general framework for abstracting agent behavior in multi-agent synchronous games in the situation calculus, which provides a ﬁrst-order representation of the state and allows us to model how plays depend on the data and objects involved. We represent such games as action theories of a special form called situation calculus synchronous game structures (SCSGSs), in which we have a single action tick whose effects depend on the combination of moves selected by the players. In our framework, one speciﬁes both an abstract SCSGS and a concrete SCSGS, as well as a reﬁnement mapping that speciﬁes how each abstract move is implemented by a Golog program deﬁned over the concrete SCSGS. We deﬁne notions of sound and complete abstraction with respect to a mapping over such SCSGS. To express strategic properties on the abstract and concrete games we adopt a ﬁrst-order variant of alternating-time µ-calculus µATL-FO. We show that we can exploit abstraction in verifying µATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes.

Introduction Many multi-agent applications can be viewed games where some agents try to ensure that certain objectives hold no matter how the environment and other agents behave. Logics such as Alternating-Time Temporal Logic (ATL) (Alur, Henzinger, and Kupferman 2002), Coalition Logic (CL) (Pauly 2002), and Strategy Logic (SL) (Chatterjee, Henzinger, and Piterman 2010; Mogavero et al. 2014) have been deﬁned to specify properties of such systems and verify them through techniques like model checking. However, as the game/system becomes more complex, it becomes very important to use abstraction to explain how the game evolves and do strategic reasoning more effectively. (Banihashemi, De Giacomo, and Lesp erance 2017) (BDL17) recently proposed a formal account of agent abstraction based on the situation calculus (Mc Carthy and Hayes 1969; Reiter 2001) and the Con Golog agent programming language (De Giacomo, Lesp erance, and Levesque 2000). They assume that one has a high-level/abstract action theory, a low-level/concrete action theory, both representing the agent s behavior at different levels of detail, and

Copyright 2024, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

a reﬁnement mapping between the two. The reﬁnement mapping speciﬁes how each high-level action is implemented by a low-level Con Golog program and how each high-level ﬂuent can be translated into a low-level formula. This work deﬁnes notions of abstraction between such action theories in terms of the existence of a suitable bisimulation relation (Milner 1971) between their respective models. Such abstractions have many useful properties that ensure that one can reason about the agent s actions (e.g., executability, projection, and planning) at the abstract level, and reﬁne and concretely execute them at the low level. The framework can also be used to generate high-level explanations of low-level behavior. More recently, (Banihashemi, De Giacomo, and Lesp erance 2023), building upon (De Giacomo and Lesp erance 2021), extended their abstraction framework to agents operating in nondeterministic environments, where the agent does not fully control the outcome of its actions. In this paper, we further generalize this abstraction framework to apply to multi-agent synchronous games. To represent such games, we follow (De Giacomo, Lesp erance, and Pearce 2016) and use action theories of a special form called situation calculus synchronous game structures (SCSGSs), where we have a single action tick whose effects depend on the combination of moves selected by the players. The SCSGS speciﬁes the legal moves available to each agent in each situation and how ﬂuents change value when a tick joint move by all the agents is performed. To express strategic properties on the abstract and concrete games we adopt a ﬁrst-order variant of alternating-time µ-calculus µATL-FO. In our game abstraction framework, one speciﬁes both an abstract SCSGS and a concrete SCSGS, as well as a reﬁnement mapping that speciﬁes how each abstract move is implemented by a Golog (Levesque et al. 1997) program deﬁned over the concrete SCSGS. We show that we can exploit abstraction in verifying µATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes. Our framework is based on the situation calculus which provides a ﬁrst-order representation of the state, allowing us to model how system processes depend on the data and objects involved. Our account is more general than (Banihashemi, De Giacomo, and Lesp erance 2023), as we support multiple agents that act synchronously.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

While this paper has a foundational nature, we note that our results are relevant for concrete applications where various agents need to be controlled and coordinated in a ﬁrstorder state setting, such as those in the context of Smart Manufacturing (De Giacomo et al. 2022) and Smart Business Process Management (Marrella, Mecella, and Sardi na 2017).

Preliminaries Situation Calculus. The situation calculus is a well known predicate logic language for representing and reasoning about dynamically changing worlds (Mc Carthy and Hayes 1969; Reiter 2001). All changes to the world are the result of actions, which are terms in the language. A possible world history is represented by a term called a situation. The constant S0 is used to denote the initial situation. Sequences of actions are built using the function symbol do, such that do(a, s) denotes the successor situation resulting from performing action a in situation s. Predicates and functions whose value varies from situation to situation are called ﬂuents, and are denoted by symbols taking a situation term as their last argument (e.g., Open(Door1, s)). The abbreviation do([a1, . . . , an], s) stands for do(an, do(an 1, . . . , do(a1, s) . . .)); for an action sequence a, we write do( a, s) for do([ a], s). In this language, a dynamic domain can be represented by a basic action theory (BAT), where successor state axioms (SSA) represent the causal laws of the domain and and provide a solution to the frame problem (Reiter 2001). A special predicate Poss(a, s) is used to state that action a is executable in situation s; the precondition axioms characterize this predicate. Executable(s) means that every action done in reaching situation s was executable in the situation in which it occurred.

Synchronous Game Structures. Following (De Giacomo, Lesp erance, and Pearce 2016), we focus on games where there are n players/agents each of whom chooses a move at every time step. All such moves are executed synchronously and determine the next state of the game. At each time step, the state of the game is fully observable by all agents, as are all past moves of every agent. To represent such multi-player synchronous games, we use a special class of BATs, called situation calculus synchronous game structures (SCSGSs), which are deﬁned as follows. Agents A SCSGS D involves a ﬁnite set of n agents, and we use a subsort Agents of Objects which includes these ﬁnitely many agents Ag1, . . . , Agn, each denoted by a constant, and for which unique names Agi = Agj for i = j and domain closure Agent(x) x = Ag1 x = Agn hold. Moves. We also use a second subsort Moves of Objects, representing the possible moves of the agents. These come in ﬁnitely many types, represented by function symbols Mi( x), which are parameterized by objects x, with Move(m) W i x.m = Mi( x). Given that the parameters range over Objects, each agent may have an inﬁnite number of possible moves at each time step. We have unique name and domain closure axioms (parameterized by objects) for these functions Mi( x) = Mj( y) for i = j, and Mi( x) = Mi( y) x = y.

Actions. In SCSGSs, there is only one action type, tick(m1, . . . , mn), which represents the execution of a joint move by all the agents at a given time step. The action tick has exactly n parameters, m1, . . . , mn, one per agent, which are of sort Moves and corresponds to the simultaneous choice of the move to perform by the n different agents. Legal moves. The legal moves available to each agent in a given situation are speciﬁed formally using a special predicate Legal M , which is deﬁned by statements of the following form (one for each agent Agi and move type Mi):

Legal M (Agi, Mi( x), s) .= ΦAgi,Mi( x, s)

i.e., agent Agi can legally perform move Mi( x) in situation s if and only if ΦAgi,Mi( x, s) holds. Technically Legal M is an abbreviation for ΦAgi,Mi( x, s), which is a uniform formula (i.e., a formula that only refers to a single situation s). Precondition axioms. The precondition axiom for the action tick is ﬁxed and speciﬁed in terms of Legal M as follows:

Poss(tick(m1, . . . , mn), s)

i=1,...,n Legal M (Agi, mi, s)

Thus the joint action by all agents tick(m1, . . . , mn) is executable if and only if each selected move mi is a legal move for agent Agi in situation s. Since we only have one action type tick, this is the only precondition axiom in Dposs. Successor state axioms. We have successor state axioms Dssa, specifying the effects and frame conditions of the joint moves tick(m1, . . . , mn) on the ﬂuents. Such axioms, as usual in basic action theories, are domain speciﬁc, and characterize the actual game under consideration. Within such axioms, the agent moves, which occur as parameters of tick, determine how ﬂuents change as the result of joint moves.1

Initial situation description. Finally, the initial state of the game is axiomatized in the initial situation description DS0 as usual, in a domain speciﬁc way.

High-Level Programs and Golog. To represent and reason about complex actions or processes obtained by suitably executing atomic actions, various so-called high-level programming languages have been deﬁned. Here we concentrate on (a variant of) Golog (Levesque et al. 1997) that includes the following constructs:

δ ::= α | ϕ? | δ1; δ2 | δ1|δ2 | πx.δ | δ

In the above, α is an action term, possibly with parameters. ϕ is a situation-suppressed formula, i.e., a formula with all situation arguments in ﬂuents suppressed. As usual, we denote by ϕ[s] the formula obtained from ϕ by restoring the situation argument s into all ﬂuents in ϕ. The sequence of program δ1 followed by program δ2 is denoted by δ1; δ2. Program δ1|δ2 allows for the nondeterministic choice between programs δ1 and δ2, while πx.δ executes program δ for some nondeterministic choice of a binding for object variable x

1In many cases, moves don t interfere with each other and the effects are just the union of those of each move. One can also exploit previous work on axiomatizing parallel actions to generate successor state axioms (Reiter 2001; Pinto 1998).

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

(observe that such a choice is, in general, unbounded). δ performs δ zero or more times. Formally, the semantics of Golog can be speciﬁed in terms of single-step transitions, using two predicates (De Giacomo, Lesp erance, and Levesque 2000): (i) Trans(δ, s, δ , s ), which holds if one step of program δ in situation s may lead to situation s with δ remaining to be executed; and (ii) Final(δ, s), which holds if program δ may legally terminate in situation s. The deﬁnitions of Trans and Final that we use are as in (De Giacomo, Lesp erance, and Pearce 2010); differently from (De Giacomo, Lesp erance, and Levesque 2000), the test construct ϕ? does not yield any transition, but is ﬁnal when satisﬁed. Predicate Do(δ, s, s ) means that program δ, when executed starting in situation s, has as a legal terminating situation s , and is deﬁned as Do(δ, s, s ) .= δ .Trans (δ, s, δ , s ) Final(δ , s ) where Trans denotes the reﬂexive transitive closure of Trans. For simplicity in this paper, we use a restricted class of Golog programs which are situation-determined (SD) (De Giacomo, Lesp erance, and Muise 2012), i.e., for every sequence of actions, the remaining program is uniquely determined by the resulting situation: Sit Det(δ, s) .= s , δ , δ . Trans (δ, s, δ , s ) Trans (δ, s, δ , s ) δ = δ .

Move-Based Golog. In this paper, we will use standard Golog programs to specify tasks for the system or a coalition of agents in it; we call these system programs. But we will also use a special kind of Golog programs deﬁned in (De Giacomo, Lesp erance, and Pearce 2016) that we call movebased programs to specify the legal moves of an agent in a SCSGS as well as how high-level moves are implemented at the low level. Move-based programs are Golog programs where atomic actions are replaced by atomic moves. Apart from this change the syntax remains the same. To deﬁne the semantics of such programs, they introduce the predicate Trans M (δ, s, δ , m) to mean that the program δ in situation s can perform move m leaving δ as the remaining program to execute, and the predicate Final M (δ, s) to mean that program δ can be considered terminated in situation s. We can then deﬁne the legal moves of agents procedurally in terms of such programs by introducing a special ﬂuent Curr Prog(Agi, δi, s) that stores the remaining program of each agent in the situation:

Legal M (Agi, m, s) .= Curr Prog(Agi, δi, s) δ i.Trans M (δi, s, δ i, m)

where the successor state axiom for Curr Prog is:2

Curr Prog(Agi, δ i, do(tick(m1, . . . , mn), s)) Curr Prog(Agi, δi, s) Trans M (δi, s, δ i, mi)

That is, a move mj is legal for agent Agj in situation s if her current remaining program δj in s can perform mj, and

2Here, we assume that move-based programs are move determined: Move Det(δ, s) .= m, δ , δ .Trans M (δ, s, δ , m) Trans M (δ, s, δ , m) δ = δ . Each agent s program should remain move determined in every game situation: s.δi.Executable(s) Curr Prog(Agi, δi, s) Move Det(δi, s).

when a joint move tick(m1, . . . , mn) is performed, the current remaining program of each agent Agi is updated to be what remains of her current program after her move mi. We use C to denote the axioms deﬁning the Golog language, including Trans M and Final M for move-based programs.

Abstraction of SCSGSs In this section, we show how we can extend the agent abstraction framework of (BDL17) to handle SCSGSs. As in (BDL17), we assume that there is a high-level/abstract (HL) action theory Dh and a low-level/concrete (LL) action theory Dl representing the agent s possible behaviors at different levels of detail. In (BDL17), these are standard BATs; here, we assume that they are both SCSGSs. Dh (resp. Dl) involves a ﬁnite set of agents Agents, a ﬁnite set of move types Movesh (resp. Movesl), a set of primitive actions Ah = {tick h} (resp. Al = {tick l}) , and a ﬁnite set of primitive ﬂuent predicates Fh (resp. Fl). The terms of object sort are assumed be a countably inﬁnite set N of standard names for which we have the unique name assumption and domain closure. Also, Dh and Dl are assumed to share no domain speciﬁc symbols except for the set of standard names for objects N. For simplicity and w.l.o.g., it is assumed that there are no functions other than constants and no non-ﬂuent predicates.

Reﬁnement Mapping. In (BDL17), one relates the HL and LL BATs by deﬁning a reﬁnement mapping that speciﬁes how HL atomic actions are implemented at the LL and how HL ﬂuents can be translated into LL state formulas. In a BAT, one can simply map each HL atomic action type to a LL program that the agent uses to implement the action. In a SCSGS however, we need to specify how each HL move is implemented at the LL. Thus we say that a SCSGS reﬁnement mapping m is a triple mm, ma, mf where mm associates each HL move type m in Movesh to a move-determined (MD) move-based Golog program δm deﬁned over the LL SCSGS theory that implements the move, i.e., mm(m( x)) = δm( x), ma maps the unique HL action tick h Ah to a Golog system program that executes the mapping of the moves involved synchronously in parallel, i.e., ma(tick(m1, . . . , mn)) = sync(mm(m1), . . . , mm(mn)), and (as in (BDL17)) mf maps each situation-suppressed HL ﬂuent F( x) in Fh to a situation-suppressed formula φF ( x) deﬁned over the LL theory that characterizes the concrete conditions under which F( x) holds in a situation, i.e., mf(F( x)) = φF ( x). We support the synchronous concurrency construct by extending the Golog semantics as follows:

Trans(sync(δm1, . . . , δmn), s, δ , s ) δ m1, . . . δ mn. m1, . . . , mn.δ = sync(δ m1, . . . , δ mn) Trans M(δm1, s, δ m1, m1) ... Trans M(δmn, s, δ mn, mn) s = do(tick(m1, . . . , mn), s)

Final(sync(δm1, . . . , δmn), s) Final M(δm1, s) . . . Final M(δmn, s)

We can extend a mapping to a sequence of system actions in the obvious way, i.e., ma(α1, . . . , αn) .=

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

ma(α1); . . . ; ma(αn) for n 1 and ma(ϵ) .= nil. We also extend the notation so that mf(φ) stands for the result of substituting every ﬂuent F( x) in situation-suppressed formula φ by mf(F( x)). We also need to ensure that the mapping captures all the legal behaviors that agents can display at the LL. This is essential if we want to do strategic reasoning at the HL and be able to reﬁne the resulting strategies into LL ones that achieve the objectives. This can be done analogously to how BATs for nondeterministic domains (NDBATs) are mapped in (Banihashemi, De Giacomo, and Lesp erance 2023). But there is a new complication here. We need to ensure that at the LL, all agents start their HL moves at the same time and end them at the same time, otherwise ensuring bisimilarity with respect to (wrt) the mapping becomes very difﬁcult. To get this, we impose the following constraint:

Constraint 1 (Proper Reﬁnement Mapping) For every high-level system action sequence α and every agent i Agents, we have that:

Dl C |= s.(Do(ma( α), S0, s) mi, s .(Do(sync( (πm.m) , mm(mi), (πm.m) ), s, s ) m1, . . . , mi 1, mi+1, . . . , mn. Do(ma(tick(m1, . . . , mi 1, mi, mi+1, . . . , mn)), s, s )))

This ensures that for every situation s that can be reached by an agent i executing a reﬁnement of a HL move mi with other agents executing arbitrary legal LL moves, there exist HL legal moves by the other agents that make the system reach s . To guarantee this, we have to ensure that at the LL, agents only perform moves that reﬁne HL moves, and that all agents begin and end reﬁnements of HL moves at the same time. We discuss below how we can specify the legal moves to respect this. We say that a SCSGS reﬁnement mapping m is proper with respect to low-level SCSGS Dl if this constraint holds.

m-Bisimulation. To relate the HL and LL models/theories, (BDL17) deﬁne a variant of bisimulation (Milner 1971, 1989). Let Mh be a model of the HL theory Dh, and Ml a model of the LL theory Dl C. We say that situation sh in Mh is m-isomorphic to situation sl in Ml, written sh Mh,Ml m sl, if and only if

Mh, v[s/sh] |= F( x, s) iff Ml, v[s/sl] |= m(F( x))[s] for every high-level primitive ﬂuent F( x) in Fh and every variable assignment v (v[x/e] stands for the assignment that is like v except that x is mapped to e).

A relation B Mh S Ml S (where M S stands for the situation domain of M) is an m-bisimulation relation between Mh and Ml if sh, sl B implies that:

1. sh Mh,Ml m sl, i.e., sh and sl evaluate HL ﬂuents the same; 2. for every HL primitive action type A in Ah, if there exists s h such that Mh, v[s/sh, s /s h] |= Poss(A( x), s) s = do(A( x), s), then there exists s l such that Ml, v[s/sl, s /s l] |= Do(ma(A( x)), s, s ) and s h, s l B; and

3. for every HL primitive action type A in Ah, if there exists s l such that Ml, v[s/sl, s /s l] |= Do(ma(A( x)), s, s ), then there exists s h such that Mh, v[s/sh, s /s h] |= Poss(A( x), s) s = do(A( x), s) and s h, s l B. Mh is m-bisimilar to Ml, written Mh m Ml, if and only if there exists an m-bisimulation relation B between Mh and Ml such that (SMh 0 , SMl 0 ) B. A situation sh in Mh is mbisimilar to situation sl in Ml, written sh Mh,Ml m sl, if and only if there exists an m-bisimulation relation B between Mh and Ml and (sh, sl) B. The deﬁnition of m-bisimulation for SCSGSs can remain as in (BDL17) where conditions (ii) and (iii) are applied to the high-level primitive action tickh and its mapping ma. The deﬁnition of m-bisimulation ensures that performing a HL tick action results in m-bisimilar situations. (BDL17) use m-bisimulation to deﬁne notions of sound/ complete abstraction. Dh is a sound abstraction of Dl relative to reﬁnement mapping m if and only if, for all models Ml of Dl C, there exists a model Mh of Dh such that Mh m Ml. With a sound abstraction, whenever the HL theory entails that a sequence of actions is executable and achieves a certain condition, then the LL must also entail that there exists an executable reﬁnement of the sequence such that the mapped condition holds afterwards. Moreover, whenever the LL takes the executability of a reﬁnement of a HL action to be satisﬁable, then the HL does as well. A dual notion is also deﬁned: Dh is a complete abstraction of Dl relative to reﬁnement mapping m if and only if, for all models Mh of Dh, there exists a model Ml of Dl C such that Ml m Mh.

Example. Our running example involves a repair shop where a set of agents collaborate to repair items and ship them to customers. The set of agents consists of two repair robots RR1 and RR2, a dispatcher Disp that assigns items to either of these, a shipper Sh, and an agent representing the customers Cust. We assume that items arrive at the shop, are assigned to one of the repair robots by the dispatcher, then are repaired, and ﬁnally are shipped by the shipper. The HL SCSGS Drs h has the following Legal M axioms:

Legal M (ag, arrive(i), s) .= ag = Cust Arrived(i, s) Legal M (ag, assign(i, ag ), s) .= ag = Disp (ag = RR1 ag = RR2) Arrived(i, s) ag .Assigned(i, ag , s) Legal M (ag, repair(i), s) .= (ag = RR1 ag = RR2) Assigned(i, ag, s) Repaired(i, s) Legal M (ag, ship(i), s) .= ag = Sh Repaired(i, s) Shipped(i, s) Legal M (ag, wait, s) .= True

Drs h also includes the following SSAs (we use the shorthand notation m a to mean that move m is one of the moves in the joint move a = tick(m1, . . . , mn)):

Arrived(i, do(a, s)) arrive(i) a Arrived(i, s) Assigned(i, ag, do(a, s)) assign(i, ag) a Assigned(i, ag, s) Repaired(i, do(a, s)) repair(i) a Repaired(i, s) Shipped(i, do(a, s)) ship(i) a Shipped(i, s)

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

Drs h also contains the following initial state axioms:

i.Arrived(i, S0) i = 1 i, ag. Assigned(i, ag, S0) i. Repaired(i, S0) i. Shipped(i, S0)

Before presenting the LL theory, let us deﬁne the reﬁnement mapping mrs (we use subscripts to disambiguate HL and LL moves with the same name):

mrs(arrive HL(i))= Arrived LL(i)?; arrive LL(i); wait LL mrs(assign HL(i, ag)) = ((ag = RR1 ag = RR2) Arrived LL(i) ag .Assigned LL(i, ag ))?; assign LL(i, ag); wait LL mrs(repair(i)) = ( ag.Assigned LL(i, ag) (Diagnosed(i) Fixed(i)))?; diagnose(i); fix(i) mrs(ship(i)) = (Diagnosed(i) Fixed(i) (Packed(i) Dropped Oﬀ(i)))?; pack(i); drop Oﬀ(i) mrs(wait HL) = wait LL; wait LL mrs(Arrived HL(i)) = Arrived LL(i) mrs(Assigned HL(i, ag)) = Assigned LL(i, ag) mrs(Repaired(i)) = Diagnosed(i) Fixed(i) mrs(Shipped(i)) = Packed(i) Dropped Oﬀ(i)

We specify agents LL legal moves procedurally using the move-based Golog language discussed earlier. Thus, in the LL SCSGS Drs l , we have the following initial state axioms specifying the agents initial move-based programs:

Curr Prog(Cust, δi, S0) δi = ((πi.mrs(arrive HL(i)))|mrs(wait))

Curr Prog(Disp, δi, S0) δi = ((πi, ag.mrs(assign HL(i, ag)))|mrs(wait))

Curr Prog(ag, δi, S0) (ag = RR1 ag = RR2) δi = ((πi.mrs(repair(i)))|mrs(wait))

Curr Prog(Sh, δi, S0) δ =((πi.mrs(ship(i)))|mrs(wait))

This says that agents can perform any sequence of reﬁnements of their HL moves as speciﬁed by the mapping. We also have the standard legal move axiom for procedural move-based Golog legal move speciﬁcations, as well as the standard SSA for Current Prog, as discussed earlier. Drs l also includes the following SSAs:

Arrived(i, do(a, s)) arrive(i) a Arrived(i, s) Assigned(i, ag, do(a, s)) assign(i, ag) a Assigned(i, ag, s) Diagnosed(i, do(a, s)) diagnose(i) a Diagnosed(i, s) Fixed(i, do(a, s)) fix(i) a Fixed(i, s) Packed(i, do(a, s)) pack(i) a Packed(i, s) Dropped Oﬀ(i, do(a, s)) drop Oﬀ(i) a Dropped Oﬀ(i, s)

Drs l also contains the following initial state axioms:

i.Arrived(i, S0) i = 1 i, ag. Assigned(i, ag, S0) i. Diagnosed(i, S0) i. Fixed(i, S0) i. Packed(i, S0) i. Dropped Oﬀ(i S0)

In general, to ensure that a LL SCSGS satisﬁes Constraint 1, we need to make sure that agents begin and end reﬁnements of HL moves at the same time. A simple way to ensure this is to have all HL moves perform the same number

of LL moves, as we did above. But a more ﬂexible way to do this is to add synchronization moves at the LL.3 As well as ensuring that reﬁnements of HL moves begin and end at the same time, we must make sure that the LL move sequences produced match those allowed by the HL move mapping. If we specify agents legal moves at the LL procedurally using Golog programs as above, this is easy to do. If instead we want to provide a declarative speciﬁcation, then we need to tailor the LL legal move conditions to ensure that moves can only occur as allowed by the mapping. We can show that:

Proposition 2 SCSGS Drs h is a sound and complete abstraction of SCSGS Drs l wrt reﬁnement mapping mrs.

Proof Sketch We use Theorems 9 and 12 from (BDL17) which identify a number of properties that must be entailed by the low-level theory to have sound and complete abstraction wrt a mapping. First, we must show that after any reﬁnement of a HL action sequence, a reﬁnement of a HL action is executable if and only if the mapped precondition of the HL action holds. Second, we must show that after any reﬁnement of a HL action sequence, the mapped HL successor state axioms hold over any reﬁnement of a HL action. Finally, we must show that the initial situations are m-isomorphic (as we have complete information about the initial state here).

Proposition 3 SCSGS reﬁnement mapping mrs is proper wrt SCSGS Drs l .

Proof Sketch We prove this by induction on the length of α. Drs l uses a procedural speciﬁcation of legal moves, so the proof is easy: the only legal moves at the LL are those that are produced by a sequence of reﬁnements of the agent s HL moves.

Notice that our framework supports synchronous moves by the agents, not just turn-based games. In our example, we can have a joint move where a repair robot repairs an item at the same time as the shipper agent ships another item. Furthermore, the effects of a joint move can depend on the moves of several agents and their interaction, e.g., we can represent a domain where two robots are able to lift a heavy object only if they both make a lift move synchronously.

Abstraction in Verifying Strategic Properties µATL-FO. To express properties about SCSGSs, (De Giacomo, Lesp erance, and Pearce 2016) introduces the logic µATL-FO, inspired by alternating-time µ-calculus, µATL, a well-known generalization of ATL (Alur, Henzinger, and

3We can do this by introducing a new ﬂuent Done HLmove(agt, s) and new moves set Done HLmove(agt) and unset Done HLmove(agt) that toggle it. We then modify the implementation of moves to ensure that after completing a reﬁnement of their HL move, agents ﬁrst do set Done HLmove(self) and then repeatedly do a wait move until all agents have set their Done HLmove; also, before starting a reﬁnement of a HL move, all agents must do unset Done HLmove(self).

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

Kupferman 2002). This logic is a ﬁrst-order variant of the µcalculus (Bradﬁeld and Stirling 2007) that works on games, by suitably considering coalitions acting towards the realization of a temporally extended goal, as in µATL. We have the following syntax for µATL-FO formulas:

Ψ ϕ | Z | Ψ | Ψ1 Ψ2 | x.Ψ | G Ψ | µZ.Ψ(Z)

In the above, ϕ is an arbitrary, possibly open, situationsuppressed situation calculus uniform formula and Z is a predicate variable of a given arity. G Ψ means that coalition G can force Ψ to hold next, i.e., there is a vector of legal moves for the agents in G such that for all legal moves by the other agents, Ψ holds afterwards. µZ.Ψ(Z) is the least ﬁxpoint construct from the µ-calculus, which denotes the least ﬁxpoint of the formula Ψ(Z) (we use this notation to emphasize that Z may occur free, i.e., not quantiﬁed by µ in Ψ). Similarly νZ.Ψ(Z), deﬁned as µZ. Φ[Z/ Z] (where we denote with Φ[Z/ Z] the formula obtained from Φ by substituting each occurrence of Z with Z), denotes the greatest ﬁxpoint of Ψ(Z). We also use the usual abbreviations for ﬁrst-order logic such as disjunction ( ) and universal quantiﬁcation . Moreover we denote by [[G]] Ψ the dual of G Ψ, i.e., [[G]] Ψ .= G Ψ. As usual in the µ-calculus, formulas of the form µZ.Ψ(Z) (and νZ.Ψ(Z)) must obey the syntactic monotonicity of Ψ( ) w.r.t. Z, which states that every occurrence of the second-order variable Z in Ψ(Z) must be within the scope of an even number of negation symbols. This ensures that both the least ﬁxpoint µZ.Ψ(Z) and the greatest ﬁxpoint νZ.Ψ(Z) always exist. Using these least and greatest ﬁxpoint constructs, we can express the ability of forcing arbitrary temporal and dynamic properties. For instance, to say that group G has a strategy to force achieving ϕ( x) eventually, where ϕ( x) is a situation suppressed formula with free variables x, we use µZ. ϕ( x) G Z; in a ﬁrst-order ATL, this could be expressed as G 3ϕ( x). Other ATL constructs such as G can force always ϕ( x), G 2ϕ( x), and G can force ϕ( x) to hold until ϕ ( y), G ϕ( x) U ϕ ( y), can also be expressed. The formal semantics of µATL-FO is based on characterizing how to evaluate µATL-FO formulas in a situation calculus model M. To do so, since µATL-FO contains formulas with both individual and predicate free variables, we need to introduce an individual variable valuation v, and a predicate variable valuation V , i.e., a mapping from predicate variables Z to subsets of the set of all situations S. Then, we assign meaning to formulas by associating to M, v, and V an extension function ( )M v,V , which maps formulas to subsets of S, and is deﬁned inductively as follows:

(ϕ)M v,V = {s S | M |= ϕ[s]} ( Ψ)M v,V = S (Ψ)M v,V (Ψ1 Ψ2)M v,V = (Ψ1)M v,V (Ψ2)M v,V ( x.Ψ)M v,V = {s S | exists t s.t. s (Ψ)M v[x/t],V } ( G Ψ)M v,V = {s S | s Pre(G, (Ψ)M v,V )} (Z( t)M v,V ) = V (Z) (µZ.Ψ)M v,V = T{E S | (Ψ)M v,V [Z/E] E}

where Pre(G, E) = {s S | m1, ..., mk. V

gi {g1,...,gk}=G(M |= Legal M (gi, mi, s)) mk+1, ..., mn. V

gj {gk+1,...,gn}=G(M|=Legal M (gj, mj, s)) mk+1, ..., mn. V

gj {gk+1,...,gn}=G(M |= Legal M (gj, mj, s)) do(tick(m1, ..., mn), s) E}

Note that given a valuation V and a predicate variable Z and a set of situations E we denote by V [Z/E] the valuation obtained from V by changing the value of Z to E, and similarly for v. Notice also that when a µATL-FO formula Ψ is closed (w.r.t. individual and predicate variables), its extension (Ψ)M v,V does not depend on the valuations v and V , and we denote the extension of Ψ simply by (Ψ)M. We say that a closed formula Ψ holds in the situation calculus model M, denoted by M |= Ψ, if S0 (Ψ)M.

Strategic Ability to Execute Programs. Adapting (De Giacomo and Lesp erance 2021), we deﬁne an agent strategy as a function from situations to (instantiated) agent moves. That is, f(s) = M( t) denotes that the strategy f applied to situation s returns M( t) as the agent s next move. The special agent move stop (with no effects and always legal) may be returned when the strategy wishes to stop. Given an agent strategy fi for every agent i in a coalition C, we denote the joint strategy where every agent i in C follows agent strategy fi by f C, where f C(i) = fi for all i C. To represent the ability of a coalition C to execute a system program/task δ in a SCSGS domain, we write Can Force By(C, δ, s, f C), which can be viewed as an adversarial version of Do in presence of agents outside the coalition. This predicate states that joint strategy f C executes SD Golog system program δ in situation s considering its nondeterminism angelic, as in the standard Do, but also considering the nondeterminism of agents outside the coalition devilish/adversarial:

Can Force By(C, δ, s, f C) .= P.[. . . P(δ, s)] where . . . stands for [(( i C.fi(s) = stop) Final(δ, s)) P(δ, s)] [ i C. mi.(fi(s) = mi = stop j C. ( mj.Poss(tick( mi mj), s)) mj.Poss(tick( mi mj), s) δ .Trans(δ, s, δ , do(tick( mi mj), s)) P(δ , do(tick( mi mj), s))) P(δ, s)] Note that the coalition s joint move mi selected by its strategy must successfully complete the task for every legal joint move mj by agents outside the coalition. We also say that predicate Can Force(C, δ, s) holds if and only if there exists a joint strategy f C for agents in coalition C such that Can Force By(C, δ, s, fc) holds.

Strategic reasoning in executing reﬁnements of HL moves. To exploit abstraction in verifying strategic properties, we ﬁrst need to consider how much strategic reasoning an agent (resp. a coalition) needs to do to execute a HL atomic move (resp. joint move) at the LL. A given HL agent

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

move M( x) is mapped to a LL agent program mm(M( x)) that implements it. In m-bisimilar models, if a coalition C has a vector of legal moves m C and the agents outside the coalition also have legal moves m C, then there exists a terminating execution of ma(tick( m C m C)) at the LL for any vector of legal moves m C by agents outside the coalition. But this does not mean that all executions of mm( m C) terminate when executed together with legal moves by the agents outside the coalition mm( m C), as some executions may block or diverge, due to choices of the agents in the coalition or that of agents outside it. In general, the agents in the coalition must do strategic reasoning to ensure that the execution of mm( m C) terminates (and the agents outside the coalition may need to cooperate as well). But we can impose further constraints on the mapping of HL moves to avoid this or ensure that an execution strategy exists. Note that ensuring that the execution of mm( m C) terminates does not mean that the agents in C control the joint move s outcome; the outcome still depends on the moves that the agents outside the coalition select. One simple approach to ensure that we can reﬁne HL strategies into LL ones is to constrain the mapping of HL moves to ensure that the implementation program always terminates and no LL strategic reasoning is required to ensure termination. But here we follow a less restrictive approach that requires that for any HL move by an agent that is possibly executable at the LL, the agent has a strategy to execute it to termination no matter how the other agents act (even if not controlling the outcome). Formally:

Constraint 4 (Agents Can Always Execute HL Moves) For every high-level system action sequence α and every agent i Agents, we have that:

Dl C |= s.(Do(ma( α), S0, s) mi.( s .Do(sync( (πm.m) , mm(mi), (πm.m) ), s, s ) Can Force({i}, sync( (πm.m) , mm(mi), (πm.m) ), s)))

Given this constraint, it follows that for any HL joint action by a non-empty coalition that is possibly executable at the LL, the coalition has a strategy to execute it to termination no matter how the agents outside the coalition behave.

Proposition 5 Constraint 4 holds for SCSGS Drs l and reﬁnement mapping mrs.

Proof Sketch We prove this by induction on the length of α. According to Drs l , the only legal moves at the LL are those that are produced by a sequence of reﬁnements of the agent s HL moves. We can show that the implementations of the HL moves that can be executed synchronously by the agents never interfere with each other. The only nondeterminism in the implementation of the HL moves themselves is the initial choice of item (as well as the agent for assign(i, agt )); when the initial test is satisﬁed, the body can always be executed successfully.

Using abstraction in Verifying µATL-FO Properties. We would like to show that if we have m-bisimilar models and a µATL-FO property Ψ holds in some situation sh at the HL,

then at the LL the mapped version of Ψ holds in any situation sl that is m-bisimilar to sh. The ﬁrst question we face is how to map µATL-FO formulas, in particular G Ψ. Since HL moves are mapped to programs, if a condition Ψ holds at the next instant at the HL, then the mapped condition will hold not at the next LL instant but in the one where the reﬁnements of the HL moves have ﬁnished executing, at the next LL state where a HL joint move has been completed. First, following (BDL17), we will impose a constraint on the reﬁnements of high-level joint moves/actions:

Constraint 6 For any distinct ground high-level system action terms α and α we have that:

(a) Dl C |= s, s .Do(ma(α), s, s ) δ.Trans (ma(α ), s, δ, s ) (b) Dl C |= s, s .Do(ma(α), s, s ) a δ.Trans (ma(α), s, δ, do(a, s )) (c) Dl C |= s, s .Do(ma(α), s, s ) s < s

Part (a) ensures that different HL primitive system actions have disjoint sets of reﬁnements; (b) ensures that once a reﬁnement of a HL primitive system action is complete, it cannot be extended further; and (c) ensures that a reﬁnement of a HL primitive system action will produce at least one LL action. As shown in (BLD17), these restrictions ensure that we can map a LL system action sequence back to a unique HL system action sequence that produced it.

Proposition 7 Constraint 6 holds for SCSGS Drs l and reﬁnement mapping mrs.

Proof Sketch The result follows easily from the fact that the HL moves are mapped to programs that each contains a distinctive LL move. Also, they all perform exactly two LL moves.

We will also assume that the LL model/theory tracks when reﬁnements of HL actions start and end through a state formula Hlc(s), which means that a HL action sequence has just completed in situation s:

Constraint 8 Dl C |= Hlc(s) if and only if there exists a HL system action sequence α such that Dl C |= Do( α, S0, s).

Hlc can be deﬁned in various ways. If all reﬁnements of HL actions have the same number of LL actions k, we can add a ﬂuent ctr that counts how many LL actions have occurred since that last HL action completed and deﬁne Hlc(s) .= ctr mod k = 0. If we add synchronization moves and ﬂuents at the low level as discussed in the previous section, we can use them to deﬁne Hlc (e.g., Hlc(s) .= agt.Done HLmove(agt, s)).

Proposition 9 Constraint 8 holds for SCSGS Drs l and reﬁnement mapping mrs.

Proof Sketch We can introduce a counter ﬂuent ctr and deﬁne Hlc(s) .= ctr mod 2 = 0 as discussed above. The result can then be shown easily by induction on the length of α.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

Using this, we can introduce an abbreviation G h Ψ, meaning that coalition G can force Ψ to hold next after the execution of one HL action:

G h Ψ .= G ( Hlc U (Hlc Ψ)) .= G µZ.((Hlc Ψ) ( Hlc G Z))

Using this, we extend the mapping to µATL-FO formulas:

ml(ϕ) .= mf(ϕ) ml( Ψ) .= ml(Ψ) ml(Ψ1 Ψ2) .= ml(Ψ1) ml(Ψ2) ml( x.Ψ) .= x.ml(Ψ) ml( G Ψ) .= G h ml(Ψ) ml(Z( t)) .= Z( t) ml(µZ.Ψ) .= µZ.ml(Ψ)

We can now show that we can exploit abstraction in verifying µATL-FO properties. First, we will show this for the sublanguage of µATL-FO without predicate variables and the µ operator, call this ATL-FO:

Lemma 10 For any ATL-FO formula Ψ, if Mh m Ml, Constraints 4, 6, and 8 hold, sh Mh,Ml m sl, and sh (Ψ)Mh v , then sl (ml(Ψ))Ml v .

Proof By induction on the structure of Ψ. Base case: If Ψ is a situation-suppressed situation calculus formula, the result follows immediately by Lemma 1 in (BDL17). Inductive step: If Ψ is Ψ , Ψ1 Ψ2, or x.Ψ, the result follows by the induction hypothesis and the deﬁnition of the extension function. If Ψ is G Ψ , then at the high level, by the deﬁnition of of the extension function, we have that there exists a HL joint move m C for agents in the coalition such that there exists a joint move m C by agents outside the coalition such that Mh, v[s/sh] |= Poss(tick( m C m C), s), and for all joint moves m C by agents outside the coalition, if Mh, v[s/sh] |= Poss(tick( m C m C), s) then do(tick( m C m C), s) (Ψ )Mh v,V . Since Constraint 4 holds, the coalition always knows how to execute joint high-level moves to completion at the low level, and thus there exists a low-level strategy gl for the coalition such that Ml, v[s/sl] |= Can Force(C, sync(mm( m C), (πm.m) ), s, gl). Take an arbitrary s l such that Ml, v[s/sl, s /s l] |= Do(sync( gl, (πm.m) ), s, s ). By Constraint 1, we have that there exist some vector of HL moves for the agents outside the coalition m C such that Ml, v[s/sl, s /s l] |= Do(ma(tick( m C m C)), s, s ). Since sh Mh,Ml m sl, it then follows that there exists s h such that Mh, v[s/sh, s /s h] |= Do(tick(( m C m C), s, s ) and s h Mh,Ml m s l. Then by the induction hypothesis, we have that s l (ml(Ψ ))Ml v,V . By Constraint 6, it must be the case that at least one LL action occurs between sl and s l and that no reﬁnement of a HL action is complete between them. Then by Constraint 8, we have that Ml, v[s/sl, s /s l] |= Hlc(s ) s .s <

s < s Hlc(s ). Thus, we also have that sl ( G h ml(Ψ))Ml v,V .

We can now extend the result to all of µATL-FO:

Theorem 11 For any µATL-FO formula Ψ, if Mh m Ml, Constraints 4, 6, and 8 hold, sh Mh,Ml m sl, and sh (Ψ)Mh v,V , then sl (ml(Ψ))Ml v,V .

Proof We prove the theorem in two steps. First, we show that Lemma 10 can be extended to the inﬁnitary version of ATL-FO that supports arbitrary inﬁnite disjunction of formulas sharing the same free variables (van Benthem 1983). Then, we recall that ﬁxpoints can be translated into this inﬁnitary logic, thus guaranteeing that the result extends to the whole µATL-FO logic. Let Γ be a possibly inﬁnite set of open ATL-FO formulas. The semantics of W Γ is sh (W Γ)Mh v if and only if sh (Ψ )Mh v for some Ψ Γ. Arbitrary inﬁnite conjunction is obtained for free through negation. Lemma 10 extends to this arbitrary inﬁnite disjunction. By the induction hypothesis, we have that if sh (Ψ)Mh v , then sl (ml(Ψ))Ml v . Given the semantics of W Γ above, this implies that if sh (W Γ)Mh v , then sl (ml(W Γ))Ml v (we assume that ml(W{Ψ, . . . , Ψ }) .= W{ml(Ψ), . . . , ml(Ψ )}). In order to extend the result to the whole µATL-FO, we translate µ-calculus approximates into the inﬁnitary ATL-FO (see (Bradﬁeld and Stirling 2007; van Benthem 1983)), where the approximate of index α is denoted by µαZ.Ψ for least ﬁxpoint formulas µZ.Ψ and ναZ.Ψ for greatest ﬁxpoint formulas νZ.Ψ. This is a standard result that holds also for µATL-FO. In particular, such approximates are as follows:

µ0Z.Ψ = False ν0Z.Ψ = True µβ+1Z.Ψ = Ψ[Z/µβZ.Ψ] νβ+1Z.Ψ = Φ[Z/νβZ.Ψ] µλZ.Ψ = W

β<λ µβZ.Ψ νλZ.Ψ = V

where λ is a limit ordinal, and the notation Ψ[Z/νβZ.Ψ] denotes the formula obtained from Ψ by replacing each occurrence of Z by νβZ.Ψ. By the Tarski and Knaster Theorem (Tarski 1955), the ﬁxpoints and their approximates are connected by the following properties:

s (µZ.Ψ)M v,V if and only if there exists an ordinal α such that s (µαZ.Ψ)M v,V and, for every β < α, it holds that s (µβZ.Ψ)M v,V ;

s (νZ.Ψ)M v,V if and only if there exists an ordinal α such that s (ναZ.Ψ)M v,V and, for every β < α, it holds that s (νβZ.Ψ)M v,V .

Since each approximate, including the ones corresponding exactly to the least and greatest ﬁxpoints, can be written as an inﬁnitary ATL-FO formula, we get the thesis.

Notice that the HL game structure is usually much smaller than the LL one, so verifying that a µATL-FO property holds at that HL would typically be much easier than doing so at

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

the LL. By the above theorem, if a µATL-FO property holds at the HL, then it immediately follows that the mapped property also holds at the LL, provided that the constraints are satisﬁed.

Example Cont. Using µATL-FO, we can express a wide range of strategic properties involving temporally extended goals. For a ﬁrst example, consider the ﬁrstorder ATL property that the dispatcher and ﬁrst repair robot can ensure that some item is eventually repaired {Disp, RR1} 3 i.Repaired(i), which can be expressed in µATL-FO as µZ. i.Repaired(i) {Disp, RR1} Z, call this ΨF r h . This holds at the HL, i.e., S0 (ΨF r h )M rs h , because item 1 has arrived initially, and the joint strategy where Disp assigns the item to RR1 who then repairs it achieves the goal no matter what other agents do. Since Constraints 4, 6, and 8 hold, by Theorem 11 it follows that the mapped property holds at the LL as well, i.e., S0 (ml(ΨF r h ))M rs l For a second example, consider the ﬁrst-order ATL property stating that the coalition of all the repair shop agents C = {Disp, RR1, RR2, Sh} has a joint strategy to ensure that all the items that arrive are eventually shipped C i.2(Arrived(i) 3Shipped(i)), which can be expressed in µATL-FO as

i.νX.(Arrived(i) µY.Shipped(i) C Y ) C X

We can show that this property, call it ΨGa F s h holds at the HL, i.e., S0 (ΨGa F s h )M rs h .4 By Theorem 11, it follows that the mapped property also holds at the LL: S0 (ml(ΨGa F s h ))M rs l .

Discussion and Conclusion

In this paper, we presented a general ﬁrst-order framework for abstraction of synchronous multi-agent game structures. We showed that we can exploit abstraction in verifying strategic properties expressed in µATL-FO over SCSGSs if we assume that agents can always execute abstract moves to completion even if not fully controlling their outcomes. Note that our approach is quite different from the usual abstraction techniques employed in model checking (Clarke et al. 2000). The latter apply automatic abstraction and reﬁnement methods to address state-explosion in the veriﬁcation of system speciﬁcations. Such techniques have also been proposed for concurrent game structures and strategy logics, e.g., (Belardinelli, Ferrando, and Malvone 2023). The abstractions that these methods generate need not be meaningful to users of the system. Our abstractions involve new HL ﬂuents and moves that are meaningful to the users and can be used to express many HL temporally extended goals. They can be used to speed up strategic reasoning and

4A suitable strategy is for the dispatcher to assign the items to a repair agent in the order in which they arrive, for each repair agent to repair the items in the order in which they are assigned to them, and for the shipper to ship the items in the order they are repaired.

verifying strategic properties, and also to give HL explanations of system behavior. In future work, we would like to extend µATL-FO to support the use of programs to express dynamic properties. In the propositional setting our programs could be captured by Linear Dynamic Logic on Finite Traces (LDLf) (De Giacomo and Vardi 2013), for which veriﬁcation and synthesis have been shown to be decidable and effective (De Giacomo and Vardi 2015; De Giacomo and Rubin 2018; Camacho et al. 2018). However, when we move to the (ﬁrstorder) situation calculus, reasoning becomes undecidable in general. Interestingly, conditions for decidability are known both for veriﬁcation (De Giacomo, Lesp erance, and Patrizi 2016; Calvanese et al. 2022) and synthesis (De Giacomo et al. 2022). It would be worthwhile to investigate how to leverage these results in our context. We are also interested in developing techniques for automated generation of abstractions that serve users purposes. (Luo et al. 2020) shows that one can use the notion of forgetting (of LL ﬂuent and action symbols) to automatically obtain a sound and complete HL abstraction of a LL BAT for a given mapping under certain conditions; they also show that such an abstraction is computable in the propositional case. (Luo 2023) studies automated veriﬁcation of the existence of a propositional agent abstraction given a LL ﬁnite-state labeled transition system and a reﬁnement mapping where HL actions are mapped into loop-free LL programs. He shows that the problem can be reduced to a CTLK (an extension of CTL with an epistemic operator) model checking problem, which can be solved in PTIME. But in general, there are many different abstractions of a LL theory, each of which may be useful for a different purpose. So deﬁning an abstract language and mapping for a domain is non-trivial. Some human input is likely to be required, e.g., the modeler might specify the goals of the abstraction, or which details can be considered unimportant. We also want to generalize our framework for imperfect information game settings. There has been a lot of work on strategy logics for such settings including the case where one wants to ensure that each agent knows her strategy (van der Hoek and Wooldridge 2002; Jamroga and van der Hoek 2004; van der Hoek, Jamroga, and Wooldridge 2005; Herzig, Lorini, and Walther 2013; Xiong and Liu 2016; Berthon et al. 2021). The Game Description Language has also been extended for them (Thielscher 2010; Schiffel and Thielscher 2014; Engesser et al. 2021) and there is also related work in multi-agent epistemic planning (Muise et al. 2015; Le et al. 2018; Bolander et al. 2020). Finally, we plan to investigate the use of multi-tier game models/structures (Ciolek et al. 2020) to support ﬂexible strategic reasoning, where one only considers unlikely contingencies when necessary, as well as reasoning about cooperative strategies where agents delegate subgoals to others without knowing how these agents will achieve the delegated subgoals.

Acknowledgements This work is partially supported by the National Science and Engineering Research Council of Canada, by the ERC Advanced Grant White Mech (No. 834228), by the EU ICT-48

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

Project TAILOR (No. 952215), by York University, and by the University of Regina.

References Alur, R.; Henzinger, T. A.; and Kupferman, O. 2002. Alternating-time temporal logic. J. ACM, 49(5): 672 713. Banihashemi, B.; De Giacomo, G.; and Lesp erance, Y. 2017. Abstraction in Situation Calculus Action Theories. In AAAI, 1048 1055. Banihashemi, B.; De Giacomo, G.; and Lesp erance, Y. 2023. Abstraction of Nondeterministic Situation Calculus Action Theories. In IJCAI, 3112 3122. Belardinelli, F.; Ferrando, A.; and Malvone, V. 2023. An abstraction-reﬁnement framework for verifying strategic properties in multi-agent systems with imperfect information. Artif. Intell., 316: 103847. Berthon, R.; Maubert, B.; Murano, A.; Rubin, S.; and Vardi, M. Y. 2021. Strategy Logic with Imperfect Information. ACM Trans. Comput. Log., 22(1): 5:1 5:51. Bolander, T.; Charrier, T.; Pinchinat, S.; and Schwarzentruber, F. 2020. DEL-based epistemic planning: Decidability and complexity. Artif. Intell., 287: 103304. Bradﬁeld, J.; and Stirling, C. 2007. Modal mu-calculi. In Handbook of Modal Logic, volume 3, 721 756. Calvanese, D.; De Giacomo, G.; Montali, M.; and Patrizi, F. 2022. Veriﬁcation and Monitoring for First-Order LTL with Persistence-Preserving Quantiﬁcation over Finite and Inﬁnite Traces. In IJCAI, 2553 2560. Camacho, A.; Baier, J. A.; Muise, C. J.; and Mc Ilraith, S. A. 2018. Finite LTL Synthesis as Planning. In ICAPS, 29 38. Chatterjee, K.; Henzinger, T. A.; and Piterman, N. 2010. Strategy logic. Inf. Comput., 208(6): 677 693. Ciolek, D. A.; D Ippolito, N.; Pozanco, A.; and Sardi na, S. 2020. Multi-Tier Automated Planning for Adaptive Behavior. In ICAPS, 66 74. Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; and Veith, H. 2000. Counterexample-Guided Abstraction Reﬁnement. In CAV, volume 1855 of Lecture Notes in Computer Science, 154 169. De Giacomo, G.; Felli, P.; Logan, B.; Patrizi, F.; and Sardi na, S. 2022. Situation calculus for controller synthesis in manufacturing systems with ﬁrst-order state representation. Artif. Intell., 302: 103598. De Giacomo, G.; and Lesp erance, Y. 2021. The Nondeterministic Situation Calculus. In KR, 216 226. De Giacomo, G.; Lesp erance, Y.; and Levesque, H. J. 2000. Con Golog, A Concurrent Programming Language Based on the Situation Calculus. Artif. Intell, 121(1 2): 109 169. De Giacomo, G.; Lesp erance, Y.; and Muise, C. J. 2012. On supervising agents in situation-determined Con Golog. In AAMAS, 1031 1038. De Giacomo, G.; Lesp erance, Y.; and Patrizi, F. 2016. Bounded Situation Calculus Action Theories. Artif. Intell, 237: 172 203.

De Giacomo, G.; Lesp erance, Y.; and Pearce, A. R. 2010. Situation Calculus Based Programs for Representing and Reasoning about Game Structures. In KR. De Giacomo, G.; Lesp erance, Y.; and Pearce, A. R. 2016. Situation Calculus Game Structures and GDL. In ECAI, 408 416. De Giacomo, G.; and Rubin, S. 2018. Automata-Theoretic Foundations of FOND Planning for LTLf and LDLf Goals. In IJCAI, 4729 4735. De Giacomo, G.; and Vardi, M. Y. 2013. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In IJCAI, 854 860. De Giacomo, G.; and Vardi, M. Y. 2015. Synthesis for LTL and LDL on Finite Traces. In IJCAI, 1558 1564. Engesser, T.; Mattm uller, R.; Nebel, B.; and Thielscher, M. 2021. Game description language and dynamic epistemic logic compared. Artif. Intell., 292: 103433. Herzig, A.; Lorini, E.; and Walther, D. 2013. Reasoning about Actions Meets Strategic Logics. In LORI, volume 8196 of Lecture Notes in Computer Science, 162 175. Jamroga, W.; and van der Hoek, W. 2004. Agents that Know How to Play. Fundam. Informaticae, 63(2-3): 185 219. Le, T.; Fabiano, F.; Son, T. C.; and Pontelli, E. 2018. EFP and PG-EFP: Epistemic Forward Search Planners in Multi Agent Domains. In ICAPS, 161 170. Levesque, H. J.; Reiter, R.; Lesp erance, Y.; Lin, F.; and Scherl, R. B. 1997. GOLOG: A Logic Programming Language for Dynamic Domains. J. Logic Programming, 31: 59 84. Luo, K. 2023. Automated Veriﬁcation of Propositional Agent Abstraction for Classical Planning via CTLK Model Checking. In AAAI, 6475 6482. Luo, K.; Liu, Y.; Lesp erance, Y.; and Lin, Z. 2020. Agent Abstraction via Forgetting in the Situation Calculus. In ECAI, volume 325, 809 816. Marrella, A.; Mecella, M.; and Sardi na, S. 2017. Intelligent Process Adaptation in the Smart PM System. ACM Trans. Intell. Syst. Technol., 8(2): 25:1 25:43. Mc Carthy, J.; and Hayes, P. J. 1969. Some Philosophical Problems From the Standpoint of Artiﬁcial Intelligence. Machine Intelligence, 4: 463 502. Milner, R. 1971. An Algebraic Deﬁnition of Simulation Between Programs. In IJCAI, 481 489. Milner, R. 1989. Communication and concurrency. PHI Series in computer science. ISBN 978-0-13-115007-2. Mogavero, F.; Murano, A.; Perelli, G.; and Vardi, M. Y. 2014. Reasoning About Strategies: On the Model-Checking Problem. ACM Trans. Comput. Log., 15(4): 34:1 34:47. Muise, C. J.; Belle, V.; Felli, P.; Mc Ilraith, S. A.; Miller, T.; Pearce, A. R.; and Sonenberg, L. 2015. Planning Over Multi-Agent Epistemic States: A Classical Planning Approach. In AAAI, 3327 3334. Pauly, M. 2002. A Modal Logic for Coalitional Power in Games. J. Log. Comput., 12(1): 149 166.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

Pinto, J. 1998. Concurrent Actions and Interacting Effects. In KR, 292 303. Reiter, R. 2001. Knowledge in Action. Logical Foundations for Specifying and Implementing Dynamical Systems. Schiffel, S.; and Thielscher, M. 2014. Representing and Reasoning About the Rules of General Games With Imperfect Information. J. Artif. Intell. Res., 49: 171 206. Tarski, A. 1955. A lattice-theoretical ﬁxpoint theorem and its applications. Paciﬁc J. of Mathematics, 5(2): 285 309. Thielscher, M. 2010. A General Game Description Language for Incomplete Information Games. In AAAI. van Benthem, J. 1983. Modal Logic and Classical Logic. van der Hoek, W.; Jamroga, W.; and Wooldridge, M. J. 2005. A logic for strategic reasoning. In AAMAS, 157 164. van der Hoek, W.; and Wooldridge, M. J. 2002. Tractable multiagent planning for epistemic goals. In AAMAS, 1167 1174. Xiong, L.; and Liu, Y. 2016. Strategy Representation and Reasoning for Incomplete Information Concurrent Games in the Situation Calculus. In IJCAI, 1322 1329.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)