Logic-based specification and verification of homogeneous dynamic multi-agent systems
- PDF / 5,928,904 Bytes
- 34 Pages / 439.37 x 666.142 pts Page_size
- 71 Downloads / 205 Views
(2020) 34:34
Logic‑based specification and verification of homogeneous dynamic multi‑agent systems Riccardo De Masellis1 · Valentin Goranko1,2
© The Author(s) 2020
Abstract We develop a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems. Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. The state transitions are therefore determined only by the vector of numbers of agents performing each action and are specified symbolically, by means of conditions on these numbers definable in Presburger arithmetic. The agents are divided into controllable (by the system supervisor/controller) and uncontrollable, representing the environment or adversary. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a language for formal specification we use a suitably extended version of Alternating-time Temporal Logic, where one can specify properties of the type “a coalition of (at least) n controllable agents can ensure against (at most) m uncontrollable agents that any possible evolution of the system satisfies a given objective 𝛾 ″, where 𝛾 is specified again as a formula of that language and each of n and m is either a fixed number or a variable that can be quantified over. We provide formal semantics to our logic LHDMAS and define normal form of its formulae. We then prove that every formula in LHDMAS is equivalent in the finite to one in a normal form and develop an algorithm for global model checking of formulae in normal form in finite HDMAS models, which invokes model checking truth of Presburger formulae. We establish worst case complexity estimates for the model checking algorithm and illustrate it on a running example. Keywords Dynamic multi-agent systems · Logics for multi-agent systems · Logics for strategic reasoning · Model-checking
* Riccardo De Masellis [email protected] Valentin Goranko [email protected] 1
Stockholm University, Stockholm, Sweden
2
University of Johannesburg (Visiting Professorship), Johannesburg, South Africa
13
Vol.:(0123456789)
34
Page 2 of 34
Autonomous Agents and Multi-Agent Systems
(2020) 34:34
1 Introduction 1.1 The framework We consider discrete concurrent multi-agent transition systems, i.e. multi-agent systems (MAS) in which the transitions take place in a discrete succession of steps, as a result of a simultaneous (or, at least mutually independent) actions performed by all agents. Such MAS are typically modelled as concurrent game models (cf [1] or [6]). Here we focus on a special type of concurrent MAS, which are homogeneous and dynamic, in a sense explained below. The homogeneity means that all agents are essentially indistinguishable from each other, as their possible behaviours are determined by the same protocol. In particular, t
Data Loading...
