An explainable assistant for multiuser privacy

Multiuser Privacy (MP) concerns the protection of personal information in situations where such information is co-owned by multiple users. MP is particularly problematic in collaborative platforms such as online social networks (OSN). In fact, too often OSN users experience privacy violations due to conflicts generated by other users sharing content that involves them without their permission. Previous studies show that in most cases MP conflicts could be avoided, and are mainly due to the difficulty for the uploader to select appropriate sharing policies. For this reason, we present ELVIRA, the first fully explainable personal assistant that collaborates with other ELVIRA agents to identify the optimal sharing policy for a collectively owned content. An extensive evaluation of this agent through software simulations and two user studies suggests that ELVIRA, thanks to its properties of being role-agnostic, adaptive, explainable and both utility- and value-driven, would be more successful at supporting MP than other approaches presented in the literature in terms of (i) trade-off between generated utility and promotion of moral values, and (ii) users’ satisfaction of the explained recommended output.

Fair allocation of conflicting items

We study fair allocation of indivisible items, where the items are furnished with a set of conflicts, and agents are not permitted to receive conflicting items. This kind of constraint captures, for example, participating in events that overlap in time, or taking on roles in the presence of conflicting interests. We demonstrate, both theoretically and experimentally, that fairness characterizations such as EF1, MMS and MNW still are applicable and useful under item conflicts. Among other existence, non-existence and computability results, we show that a $$1/\Delta $$ 1 / Δ -approximate MMS allocation for n agents may be found in polynomial time when $$n>\Delta >2$$ n > Δ > 2 , for any conflict graph with maximum degree $$\Delta$$ Δ , and that, if $$n > \Delta $$ n > Δ , a 1/3-approximate MMS allocation always exists.

Formal verification of neural agents in non-deterministic environments

We introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in coNExpTime and PSpace-hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.

Combining quantitative and qualitative reasoning in concurrent multi-player games

We propose a general framework for modelling and formal reasoning about multi-agent systems and, in particular, multi-stage games where both quantitative and qualitative objectives and constraints are involved. Our models enrich concurrent game models with payoffs and guards on actions associated with each state of the model and propose a quantitative extension of the logic $${\textsf {ATL}}^{*}$$ ATL ∗ that enables the combination of quantitative and qualitative reasoning. We illustrate the framework with some detailed examples. Finally, we consider the model-checking problems arising in our framework and establish some general undecidability and decidability results for them.