In this paper, we further advance a line of work aimed to formally model via epistemic logic (aspects of) the group dynamics of cooperative agents. In fact, we have previously proposed and here extend a particular logical framework (the Logic of “Inferable” L-DINF), where a group of cooperative agents can jointly perform actions. I.e., at least one agent of the group can perform the action, either with the approval of the group or on behalf of the group. In this paper, we introduce agents' roles within a group. We choose to model roles in terms of the actions that each agent is enabled by its group to perform. We extend the semantics and the proof of strong completeness of our logic, and we show the usefulness of the new extension via a significant example.
logics where agents belong to groups, and it is possible for agents to reason about what their group of agents can This paper falls within a research effort whose overall do and what they themselves are able to do or prefer to do objective is to devise a comprehensive framework based (in terms of actions to perform) and which cost they are upon epistemic logic, so as to allows a designer to formal- able to pay for the execution of a costly action, whereas ize and formally verify agents and Multi-Agent Systems however, in case of insufcfiient budget, an agent can be (MAS). We have been particularly interested in modelling supported by its group. the capability to construct and execute joint plans within a In this paper, we introduce roles that agents may assume group of agents. However, such a logical framework will within the group (concerning which actions they are both really be useful if it will be immersed (either fully or in able and enabled to perform). I.e., within a group, an parts) into a real agent-oriented programming language.1 action can be performed only by agents which are allowed To this aim, we have taken all along into particular ac- by the group to do so (supposedly, because they have the count the connection between theory and practice, so as right competences). to make our logic actually usable by a system’s designers. This paper continues, in fact, a long-lasting line of work
Cooperation among agents in a MAS allow agents to aimed to formally model via epistemic logic (aspects of)
achieve better and faster results, and it is often the case the group dynamics of cooperative agents via the Logic of
that a group can fulfil objectives that are out of reach for “Inferable” L-DINF (first introduced in [
agent to perform the physical action in the sense
For an in-depth discussion on the relationship of logic L- of the BDI agent model [
The paper is organized as follows. In Sect. 2 we intro- that intend () holds whenever all agents in group duce syntax and semantics of L-DINF, together with an axiomatization of the proposed logical system.2 In Sect. 3 we discuss an example of application of the new logic. In
The logic L-DINF consists of a static component and a dynamic one. The former, called L-INF, is a logic of explicit beliefs and background knowledge. The dynamic component, called L-DINF, extends the static one with dynamic operators capturing the consequences of the agents’ inferential actions on their explicit beliefs as well as a dynamic operator capturing what an agent can conclude by performing inferential actions in its repertoire.
Let Atm = {, , . . .} be a countable set of atomic propositions. By we denote the set of all propositional formulas, i.e. the set of all Boolean formulas built out of the set of atomic propositions Atm. A set Atm represents the physical actions that an agent can perform, including “active sensing” actions (e.g., “let’s check whether it rains”, “let’s measure the temperature”). The language of L-DINF, denoted by ℒL-DINF, is defined as follows:
intend to perform the action .
The formula doi () indicates actual execution of the action by the agent . This fact is automatically recorded by the new belief () (postfix “ ” standing for “past” action). By precise choice, doi and doiP (and similarly doG and doGP ) are not axiomatized. In fact, we assume they are realized in a way that is unknown at the logical level. Hence, the axiomatization concerns only the relationship between doing and being enabled to do.
The expressions can_doi () and pref _do(, ) are closely related to doi (). In fact, can_doi () is to be seen as an enabling condition, indicating that agent is enabled to execute action , while instead pref _doi (, ) indicates the level of preference/willingness of agent to perform that action. pref _doG (, ) indicates that agent exhibits the maximum level of preference on performing action within all members of its group . Notice that, if a group of can do it, i.e., it can derive can_doi (). agents intends to perform an action , this will entail that the entire group intends to do , that will be enabled to be actually executed only if at least one agent ∈
Formulas of the form B represent beliefs of agent , while those of the form K express background knowledge. Explicit beliefs, i.e., facts and rules acquired via perceptions during an agent’s operation are kept in the working memory of the agent. Unlike explicit beliefs, an agent’s background knowledge is assumed to satisfy omniscience principles, such as closure under conjunction and known implication, and closure under logical consequence, and introspection. In fact, K is actually the well-known S5 modal operator often used to model/represent knowledge. The fact that background knowledge is closed under logical consequence is justified because we conceive it as a kind of stable reliable knowledge base, or long-term memory. We assume the background knowledge to include: facts (formulas) known by the agent from the beginning, and facts the agent has later decided to store in its long-term memory (by means of some decision mechanism not treated here) after having processed them in its working memory. We therefore assume background knowledge to be irrevocable, in the sense of being stable over time.
A formula of the form [ : ] , with ∈ 2Agt , and where must be an inferential action, states that “ holds after action has been performed by at least one of the agents in , and all agents in have common knowledge about this fact”.
Remark 1. If an inferential action is performed by an agent ∈ , the others agents belonging to the same group have full visibility of this action and, therefore, as we suppose agents to be cooperative, it is as if they had performed the action themselves. possibility of execution or actual execution of physical action . In fact, we assume that when inferring () (from _() and possibly other conditions) then the action is actually executed, and the corresponding belief () is asserted, possibly augmented with a time-stamp. Actions are supposed to succeed by default; in case of failure, a corresponding failure event will be perceived by the agent. The beliefs constitute a history of the agent’s operation, so they might be useful for the agent to reason about its own past behaviour, and/or, importantly, they may be useful to provide explanations to human users.
Remark 3. Explainability in our approach can be directly obtained from proofs. Let us assume for simplicity
Borrowing from [
(execi ( 11 2) ∧ . . . ∧ execi ( − 1 )∧ execi ( _()) ∧ ()) ⊢ () where each is one of the (mental) actions discussed above. The proof can possibly be translated into natural language, and declined either top-down or bottom-up. ): this action closes the explicit beliefs and As said in the Introduction, we model agents which, to under conjunction. I.e., ∧ is deduced from execute an action, may have to pay a cost, so they must and . have a consistent budget available. Our agents, moreover, are entitled to perform only those physical actions that ): this inferential action performs a simple form they conclude they can do. In our approach, an action can of “belief revision”. It removes from the work- be executed by a group of agents if at least one agent in ing memory in case is believed and, according the group can do, and the group has the necessary budto agent’s background knowledge, ¬ is logical get available, sharing the cost according to some policy. consequence of . Both and are required to Being our agent cooperative, among the agents that are be ground atoms. able to do some physical action, one is selected (with any ): this inferential action adds to the work- deterministic rule) among those which best prefer to pering memory in case is believed and, according form that action. We assume that agents are aware of and to agent’s working memory, is logical conse- agree with the cost-sharing policy. quence of . Notice that, unlike ∩(, ), this We have not introduced costs and budget, feasibility action operates directly on the working memory of actions and willingness to perform them, in the lanwithout retrieving anything from the background guage for two reasons: to keep the complexity of the logic knowledge. reasonable, and to make such features customizable in a modular way.3 So, as seen below, costs and budget are coped with at the semantic level which easily allows modular modification, for instance to define modalities of cost sharing are different from the one shown here, where group members share an action cost in equal parts. For
executability of inferential actions either by agent , or by a group of agents (which is a consequence of any of the group members being able to execute the action). It has to be read as: “ is an inferential action that agent (resp. an agent in ) can perform”.
Remark 2. In the mental actions ⊢(, ) and ↓(, ),
the formula which is inferred and asserted as a new
belief can be _() or (), which denote the
3We intend to use this logic in practice, to formalize memory in DALI
agents, where DALI is a logic-based agent-oriented programming
language [
(H1) if then (, , ) = (, , ); ∙ : →− 2Atm is a valuation function.
which is then used to introduce semantics of the static To simplify the notation, let () denote the set { ∈ fragment of the logic. | }, for ∈ . The set () identifies the
Notice that many relevant aspects of an agent’s be- situations that agent considers possible at world . It is haviour are specified in the definition of L-INF model, the epistemic state of agent at . In cognitive terms, it including which mental and physical actions an agent can can be conceived as the set of all situations that agent perform, which is the cost of an action and which is the can retrieve from its long-term memory and reason about. budget that the agent has available, which is the preference While () concerns background knowledge, degree of the agent to perform each action. This choice (, ) is the set of all facts that agent explicitly behas the advantages of keeping the complexity of the logic lieves at world , a fact being identified with a set of under control, and of making these aspects modularly worlds. Hence, if ∈ (, ) then, the agent has modifiable. In this paper, we introduce new function the fact under the focus of its attention and believes it. that, for each agent belonging to a group, enables the (, ) is the explicit belief set of agent at world . agent to perform a certain set of actions, so, in this way, it The executability of inferential actions is determined specifies the role of within the group. by the function . For an agent , (, ) is the set of inAs before let Agt be the set of agents. ferential actions that agent can execute at world . The value (, ) is the budget the agent has available to perDefinition 2.1. A model is a tuple = (, , ℛ, , form inferential actions. Similarly, the value (, , ) , , , , , ) where: is the cost to be paid by agent to execute the inferential ∙ is a set of worlds (or situations); action in the world . The executability of physical ∙ ℛ = {}∈Agt is a collection of equivalence rela- actions is determined by the function . For an agent , tions on : ⊆ × for each ∈ Agt ; (, ) is the set of physical actions that agent can ex∙ : Agt × →− 22 is a neighborhood function ecute at world . (, ) instead is the set of physical such that, for each ∈ Agt , each , ∈ , and each actions that agent is enabled by its group to perform. ⊆ these conditions hold: Which means, defines the role of an agent in its group, via the actions that it is allowed to execute. (C1) if ∈ (, ) then ⊆{ ∈ | }, Agent’s preference on executability of physical actions (C2) if then (, ) = (, ); is determined by the function . For an agent , and ∙ : Agt × →− 2ℒACT is an executability function a physical action , (, , ) is an integer value of mental actions such that, for each ∈ Agt and indicating the degree of willingness of agent to execute , ∈ , it holds that: at world .
(D1) if then (, ) = (, ); Constraint (C1) imposes that agent can have explicit in its mind only facts which are compatible with its cur∙ : Agt × →− N is a budget function such that, rent epistemic state. Moreover, according to constraint for each ∈ Agt and , ∈ , the following holds (C2), if a world is compatible with the epistemic state (E1) if then (, ) = (, ); of agent at world , then agent should have the same ∙ : Agt × ℒ ACT × →− N is a cost function such explicit beliefs at and . In other words, if two situathat, for each ∈ Agt , ∈ ℒACT, and , ∈ , it tions are equivalent as concerns background knowledge, holds that: then they cannot be distinguished through the explicit belief set. This aspect of the semantics can be extended in (F1) if then (, , ) = (, , ); future work to allow agents make plausible assumptions. ∙ : Agt × →− 2Atm is an executability function Analogous properties are imposed by constraints (D1), for physical actions such that, for each ∈ Agt and (E1), and (F1). Namely, (D1) imposes that agent always , ∈ , it holds that: knows which inferential actions it can perform and those it (G1) if then (, ) = (, ); cannot. (E1) states that agent always knows the available budget in a world (potentially needed to perform actions). (F1) determines that agent always knows how much it costs to perform an inferential action. (G1) and (H1) ∙ : Agt × →− 2Atm is an enabling function for physical actions such that, for each ∈ Agt and , ∈ , it holds that: determine that an agent always knows which physical conditions, and by which agent(s), an action may be peractions it can perform and those it cannot, and with which formed: degree of willingness, where (G2) specifies that an agent enabled (, ) : ∃ ∈ ( ∈ (, )∧ eaxlseocuktneoawcsewrtahienthaecrtioitns ogrronuopt, gi.iev.e, sifitthtahteapcetiromnispseirotani ntos (|,,| ) ≤ minℎ∈ (ℎ, )). to its role in the group. In the above particular formulation (that is not fixed, but
Truth values of L-DINF formulas are inductively de- can be customized to the specific application domain) ifned as follows. if at least an agent can perform it; and if the “payment”
Given a model = (, , ℛ, , , , , , , ), due by each agent, obtained by dividing the action’s cost ∈ Agt , ⊆ Agt , ∈ , and a formula ∈ ℒL-INF, equally among all agents of the group, is within each we introduce the following shorthand notation: agent’s available budget. In case more than one agent in can execute an action, we implicitly assume the ‖ ‖, = { ∈ : and , |= } agent performing the action to be the one corresponding to the lowest possible cost. Namely, is such that whenever , |= is well-defined (see below). Then, (, , ) = minℎ∈ (ℎ, , ). This definition rewe set: lfects a parsimony criterion reasonably adoptable by co(t1) , |= iff ∈ () operative agents sharing a crucial resource such as, e.g., (t2) , |= execi ( ) iff ∈ (, ) energy or money. Other choices might be viable, so varia(t3) , |= exec( ) iff ∃ ∈ with ∈ (, ) tions of this logic can be easily defined simply by devising (t4) , |= can_do() iff ∈(, )∩(, ) some other enabling condition and, possibly, introducing (t5) , |= can_do() iff ∃ ∈ differences in neighborhood update. Notice that the defwith ∈ (, ) ∩ (, ) inition of the enabling function basically specifies the (t6) , |= pref _do(, ) iff ∈ (, ) and “concrete responsibility” that agents take while concurring (, , ) = with their own resources to actions’ execution. Also, in (t7) , |= pref _do(, ) iff case of specification of various resources, different corre, |= pref _do(, ) sponding enabling functions might be defined. for = max{ (, , ) | Our contribution to modularity is that functions , ∈ ∧ ∈ (, ) ∩ (, )} and , i.e., executability of physical actions, preference (t8) , |= ¬ iff , ̸|= level of an agent about performing each action, and permission concerning which actions to actually perform, (t9) , |= ∧ iff , |= and , |= are not meant to be built-in. Rather, they can be defined (t10) , |= B iff || ||, ∈ (, ) via separate sub-theories, possibly defined using different (t11) , |= K iff , |= for all ∈ () logics, or, in a practical approach, even via pieces of code.
of mental actions instead of being fixed may in principle vary, and be computed upon need.
As seen above, a physical action can be performed by a group of agents if at least one agent of the group can do it, and the level of preference for performing this action is set to the maximum among those of the agents enabled to do this action. For any inferential action performed by any agent , we set:
, |= [ : ] iff [: ], |= accounts to modify the neighborhood of the present world.
The updated neighborhood [: ] resulting from execuWith [: ]=⟨, [: ], ℛ, , [: ], , , , , ⟩. tion of a mental action is specified as follows. Such model [: ] represents the fact that the execution of an inferential action affects the sets of beliefs of ∙ If is ↓(, ), then, for each ∈ Agt and ∈ , agent and modifies the available budget. Such operation [:↓(, )](, ) = (, ) ∪ {|| ||,} can add new beliefs by direct perception, by means of one inference step, or as a conjunction of previous beliefs. if ∈ and enabled (, ↓(, )) and , |= Hence, when introducing new beliefs (i.e., performing B ∧ K( → ). Otherwise, the neighborhood mental actions), the neighborhood must be extended does not change (i.e., [:↓(, )](, ) = (, )). accordingly. ∙ If is ∩(, ), then, for each ∈ Agt and ∈ ,
The following property enabled (, ) (for a world [:∩(, )](, ) = (, ) ∪ {|| ∧ ||,} , an action and a group of agents ) concerns a key aspect in the definition of the logic. Specifically, it states when an inferential action is enabled, i.e., under which if ∈ and enabled (, ∩(, )) and , |= B ∧ B . Otherwise, the neighborhood remains unchanged (i.e., [:∩(, )](, ) = (, )). ∙ If is ⊣ (, ), then, for each ∈ Agt and ∈ , |=L-INF (K( → ¬ )) ∧ B ) → [ : ⊣(, )] ¬B .
→ ¬ K( if ∈ and enabled (, ⊣(,
)) and , |= B ∧ K( → ¬
). Otherwise, the neighborhood does not change (i.e., [:⊣(,
)](, ) = (, )). ∙ If is ⊢(,
), then, for each ∈ Agt and ∈ , [:⊢(, )](, ) = (, ) ∪ {|| ||,}
B if ∈ and enabled (, ⊢(,
)) and , |= remains unchanged: [:⊢(,
)](, ) = (, ). ∧ B(
→ ). Otherwise, the neighborhood
Notice that, after an inferential action has been performed by an agent ∈ , all agents ∈ see the same update in the neighborhood. Conversely, for any agent ℎ ̸∈ the neighborhood remains unchanged (i.e., [: ](ℎ, ) = (ℎ, )). However, even for agents in , the neighborhood remains unchanged if the required preconditions, on explicit beliefs, knowledge, and budget, do not hold (and hence the action is not executed).
Since each agent in has to contribute to cover the each ∈ Agt and each ∈ , we set costs of execution by consuming part of its available budget, an update of the budget function is needed. For an action we assume that ∈ executes . Hence, for [: ](, ) = (, ) − (, , )/||, if ∈ and enabled (, ) and, depending on , , |= B ∧ K( → ) , |= B ∧ B , |= B ∧ K( , |= B ∧ B( → ) if is ∩ (, if is ↓(, ), or )), or ), or if is ⊢(, ).
→ ¬ ) if is ⊣(, Otherwise, [: ](, )=(, ), i.e., the budget is preserved.
We write |=L-DINF to denote that , |= holds for all worlds of every model .
We introduce below relevant consequences of our
formalization. For lack of space we omit the proof, that can
be developed analogously to what done in [
K( → ) in its background knowledge, then ) the agent 3. ¬K( ∧ ¬ ); 4. K 5. ¬K → K K ;
→ K ¬K ; 8. K ; 6. B ∧ K ( 7. B → K B ; 9. [ : ] ↔ ;
↔ ) → B ; 10. [ : ]¬ ↔ ¬[ : ] ; 11. exec( ) → K (exec( )); 12. [ : ]( ∧ ) ↔ [ : ] ∧ [ : ] ; 13. [ : ]K 14. [ : ↓(,
↔ K ([ : ] ); )]B ↔ B ([ : ↓(, 15. [ : ∩(, )]B ↔ B ([ : ∩(, 16. [ : ⊢(, )]B ↔ B ([ : ⊢(,
K [ : ∩(, )] 17. [ : ⊣(, )]¬B ︀( (B ∧ B ) ∧ ︀( (B ∧ K ( K ([ : ↓(, ︀( (B
∧ B ( K ([ : ⊢(, ↔ B ([ : ⊣(, ︀( (B ∧ K ( K ([ : ⊣(, )] )] ) ∨ → )) ∧
↔ ))︀ ; )] ) ∨ ↔ ( ∧ ))︀ ; )] )] ) ∨ → )) ∧ ↔ ))︀ ; )] ) ∨ → ¬ )) ∧ )] ↔ ))︀ ; 19. do() → can_do(); 18. intendG (A) ↔ ∀ ∈ intendi (A); 20. do() → can_do() ∧ pref _doG (i , A); 21. ↔ ↔[/ ] .
We write L-DINF ⊢ to denote that is a theorem of
is sound for the class of L-INF models, namely, all axioms are valid and inference rules preserve validity. In particular, soundness of axioms 14–17 immediately follows from the semantics of [: ] , for each inferential action , as previously defined.
Notice that, by abuse of notation, we have axiomatized the special predicates concerning intention and action enabling. Axioms 18–20 concern in fact physical actions, stating that: what is intended by a group of agents is intended by them all; and, neither an agent nor a group of agents can do what it is not enabled to do. Such axioms are not enforced by the semantics, but are supposed to be enforced by a designer’s/programmer’s encoding of parts of an agent’s behaviour. In fact, axiom 18 enforces agents in a group to be cooperative. Axioms 19 and 20 ensure that agents will attempt to perform actions only if their preconditions are satisfied, i.e., if they can do them.
done, e.g., in dynamic logic, because we want agents’ definition to be independent of the practical aspect, so we explicitly intend to introduce flexibility in the definition of such parts.
Consider a group of four agents, who are the crew of an ambulance, including a driver, two nurses, and a medical doctor. The driver is the only one enabled to drive the ambulance. The nurses are enabled to perform a number of tasks, such as, e.g., administer a pain reliever, or clean, disinfect and bandage a wound, measure vital signs. It is however the task of a doctor to make a diagnosis, to prescribe medications, to order, perform, and interpret diagnostic tests, and to perform complex medical procedures.
Imagine that the hospital received notice of a car accident with an injured person. Then, it will inform the group of the fact that a patient needs help (how exactly is not treated here, because this depends on how the multi-agent system is implemented, but a message exchange will presumably suffice). The group will reason, and devise the intention/goal K(intendG (rescue_patient )).
Among the physical actions that agents in the group can perform are for instance the following: diagnose_patient administer _urgent _treatment measure_vital _signs pneumothorax _aspiration local _anesthesia bandage_wounds drive_to_patient drive_to_hospital .
activity. Assume that, as a result of the planning phase, the knowledge base of each agent contains the following rule, that specifies how to reach the intended goal in terms of actions to perform and sub-goals to achieve: K(︀ intendG (rescue_patient ) → intendG (drive_to_patient ) ∧ intendG (diagnose_patient ) ∧ intendG (stabilize_patient )∧ intendG (drive_to_hospital ))︀ .
also have the specialized rule (for ≤ 4) K(︀ intendG (rescue_patient ) → intendi (drive_to_patient ) ∧ intendi (diagnose_patient ) ∧ intendi (stabilize_patient )∧ intendi (drive_to_hospital ))︀ .
K(︀ intendi (rescue_patient ) → intendi (drive_to_patient ))︀ K(︀ intendi (rescue_patient ) → intendi (diagnose_patient ))︀ K(︀ intendi (rescue_patient ) → intendi (stabilize_patient ))︀ K(︀ intendi (rescue_patient ) → intendi (drive_to_hospital ))︀ .
tal are actions, intendG (stabilize_patient ) is a goal.
contains also the following general rules, stating that the group is available to perform each of the necessary actions.
According to items (t4) and (t7) in the definition of truth values, for L-DINF formulas, this agent will be chosen as the one which best prefers to perform this action, among those that can do it. Formally, in the present situation, pref _doG (i , A) returns the agent in the group with the highest degree of preference on performing , and can_doG (_A) is true if there is some agent in the group which is able and allowed to perform , i.e., ∈ (, ) ∧ ∈ (, ).
K(︀ intendG (drive_to_patient ) ∧ can_doG (drive_to_patient )∧ pref _doG (i , drive_to_patient )
→ doG (drive_to_patient ))︀ K(︀ intendG (diagnose_patient )∧ can_doG (diagnose_patient )∧ pref _doG (i , diagnose_patient ) →
doG (diagnose_patient ))︀ K(︀ intendG (drive_to_hospital )∧ can_doG (drive_to_hospital )∧ pref _doG (i , drive_to_hospital ) →
doG (drive_to_hospital ))︀ .
K(︀ intendi (drive_to_patient ) ∧ can_doi (drive_to_patient )∧ pref _doi (i , drive_to_patient ) → doG (drive_to_patient ))︀ K(︀ intendi (diagnose_patient )∧ can_doi (diagnose_patient )∧ pref _doi (i , diagnose_patient ) → doi (diagnose_patient ))︀ K(︀ intendi (drive_to_hospital )∧ can_doi (drive_to_hospital )∧ pref _doi (i , drive_to_hospital ) → doi (drive_to_hospital ))︀
be some agent (let us assume for simplicity only one), for which doi (A)) will be concluded. In our case, the agent driver will conclude doi (drive_to_patient )) and doi (drive_to_hospital )); the agent doctor will conclude doi (stabilize_patient )).
for any physical action , the action is supposed to have been performed via some kind of semantic attachment which links the agent to the external environment.
Since intendG (stabilize_patient ) is not an action but a sub-goal, the group will have to devise a plan to achieve it. This will imply sensing actions and forms of reasoning not shown here. Assume that the diagnosis has been pneumothorax, and that the patient has also some wounds which are bleeding. Upon completion of the planning phase, the knowledge base of each agent contains the following rule, that specifies how to reach the intended goal in terms of actions to perform:
K(︀ intendG (stabilize_patient ) → intendG (measure_vital _signs ) ∧ intendG (local _anesthesia ) ∧ intendG (bandage_wounds ) ∧ intendG (pneumothorax _aspiration ))︀ .
As before, these rules will be instantiated and elaborated by the single agents, and there will be some agent who will finally perform each action. Specifically, the doctor will be the one to perform pneumothorax aspiration, and the nurses (according to their competences and their preferences) will measure vital signs, administer local anesthesia and bandage the wounds. The new function , in a sensitive domain such as healthcare, guarantees that each procedure is administered by one who is capable to (function ) but also enabled (function ), and so can take responsibility for the action.
An interesting point concerns derogation, i.e., for instance, life or death situations where, unfortunately, noone who is enabled to perform some urgently needed action is available; in such situations perhaps, anyone who is capable to perform this action might perform it. For instance, a nurse, in absence of a doctor, might attempt urgent pneumothorax aspiration.
From such perspective, semantics could be modified as follows: (t4’) , |= able_do() iff ∈ (, ) (t4”) , |= enabled _do() iff ∈ (, ) ∩ (, ) (t4-new) , |= can_do() iff ( ∈ (, ) ∩ (, )) ∨ ( ∈ (, ) ∧ ̸ ∃ ∈ : ∈ (, ) ∩ (, )) (t5-new) , |= can_do() iff ∃ ∈ s.t. , |= can_do()
of our logic, and we outline the proof of strong completeness w.r.t. the proposed class of models (by means of a standard canonical-model argument). As before, let Agt be a set of agents.
Definition 4.1. A canonical L-INF model is a tuple = ⟨, , ℛ, , , , , , , ⟩ where: ∙ is the set of all maximal consistent subsets of ℒL-INF; ∙ ℛ = {,}∈Agt is a collection of equivalence relations on such that, for every ∈ Agt and , ∈ , , if and only if (for all , K ∈ implies ∈ ); ∙ For ∈ , ∈ ℒL-INF let (, ) = { ∈ ,() | ∈ }. Then, we put (, )={ (, ) | B ∈ }; ∙ : Agt × →− 2ℒACT is such that, for each ∈ Agt and , ∈ , if , then (, ) = (, ); ∙ : Agt × →− N is such that, for each ∈ Agt and , ∈ , if , then (, ) = (, ); ∙ : Agt × ℒ ACT × →− N is such that, for each ∈ Agt , ∈ ℒACT, and , ∈ , if , then (, , ) = (, , ); ∙ : Agt × →− 2Atm is such that, for each ∈ Agt and , ∈ , if , then (, ) = (, ); ∙ : Agt × →− 2Atm is such that, for each ∈ Agt and , ∈ , if , then (, ) = (, ); ∙ : Agt × × Atm →− N is such that, for each ∈ Agt and , ∈ , if , then (, , ) = (, , ); ∙ : →− 2Atm is such that () = Atm ∩ . Note that, analogously to what done before, ,() denotes the set { ∈ | ,}, for each ∈ Agt . It is easy to verify that is an L-INF model as defined in Def. 2.1, since, it satisfies conditions (C1),(C2),(D1),(E1),(F1),(G1),(G2),(H1). Hence, it models the axioms and the inference rules 1–17 and 21 introduced before (while, as mentioned in Section 2.4, axioms 18–20 are assumed to be enforced by the specification of agents behaviour). Consequently, the following properties hold too. Let ∈ , then: ∙ given ∈ ℒL-INF, it holds that K ∈ if and only if ∀ ∈ such that , we have ∈ ; ∙ for ∈ℒL-INF, if B ∈ and , then B ∈.
and -related worlds have the same beliefs, i.e. there can be ,-related worlds with different beliefs.
the proof of strong completeness. For lack of space, we
list the main theorems but omit lemmas and proofs, that
we have however developed analogously to what done in
previous work [
Theorem 4.1. L-INF is strongly complete for the class of L-INF models.
Theorem 4.2. L-DINF is strongly complete for the class of L-INF models.
In this paper, we discussed the last advances of a line of work concerning how to exploit a logical formulation for a formal description of the cooperative activities of groups of agents. In past work, we had introduced beliefs about physical actions concerning whether they could, are, or have been executed, preferences in performing actions, single agent’s and group’s intentions. So far however, a limitation was missing about which actions an agent is allowed to perform; in practical situations, in fact, it will hardly be the case that every agent can perform every action.
We have listed some useful properties of the extended logic, that we have indeed proved, mainly strong completeness. Since the extension is small and modular, the complexity of the extended logic has no reason to be higher than that of the original L-DINF. In future work, we mean to extend our logic in the direction of describing multiple groups of agents and their interactions. We also mean to introduce in L-DINF, based on our past work, an explicit notion of time and time intervals.