This paper is aimed as a contribution to the use of formal modal languages in Artificial Intelligence. We introduce a multi-modal version of Second-order Propositional Modal Logic (SOPML), an extension of modal logic with propositional quantification, and illustrate its usefulness as a specification language for knowledge representation as well as temporal and spatial reasoning. Then, we define novel notions of (bi)simulation and prove that these preserve the interpretation of SOPML formulas. Finally, we apply these results to assess the expressive power of SOPML.

The paper analyses multi-agent strategic dialogues on possibly infinite argumentation frameworks. We develop a formal model for representing such dialogues, and introduce FO A -ATL, a first-order extension of alternating-time logic, for expressing the interplay of strategic and argumentation-theoretic properties. This setting is investigated with respect to the model checking problem, by means of a suitable notion of bisimulation. This notion of bisimulation is also used to shed light on how static properties of argumentation frameworks influence their dynamic behaviour.

We develop a methodology to model and verify Regarding the second limitation, proposals have been put open multi-agent systems (OMAS), where agents forward to consider a set of objects that vary at design time; may join in or leave at run time. Further, we specify the set of agents is normally considered to be finite in each properties of interest on OMAS in a variant of firstorder system run. This is a sensible assumption in many scenarios, temporal-epistemic logic, whose characterising but there are applications of MAS (e.g., e-commerce, smart features include epistemic modalities indexed grids) where an unbounded number of agents may freely enter to individual terms, interpreted on agents appearing and leave the system at run time. There is, therefore, at a given state. This formalism notably allows a need to account for the unbounded and possibly infinite to express group knowledge dynamically. We study agents joining in or leaving an open MAS. In this setting it the verification problem of these systems and show is still of interest to reason about their evolution and what that, under specific conditions, finite bisimilar abstractions they know individually and collectively. For example, in an can be obtained.