Abstract

Runtime verification checks the behaviour of a running system against a formal specification. In autonomous and multi-agent systems, however, a monitor may lack relevant observations, face limited sensing or communication resources, or depend on information held by other agents. Even with complete observations, some properties cannot be conclusively assessed from a finite execution prefix. This talk presents two complementary research lines addressing these limitations. The first concerns partial monitoring: recognising when a conclusive verdict has become unreachable and identifying events that no longer contribute to the monitoring task. The second concerns runtime verification under imperfect information, where indistinguishability relations make observational limitations explicit, allowing monitors to distinguish missing information from negative evidence while preserving the soundness of definitive verdicts. Building on this foundation, I will discuss rational monitors that select affordable observations according to the property being checked and revise these choices as execution progresses. I will then turn to rational multi-monitors, where information acquisition becomes a strategic interaction: monitors with their own objectives and resource bounds establish agreements to exchange relevant information. Examples from robotic inspection and smart homes will illustrate this progression, connecting runtime verification with resource-bounded strategic reasoning. The central question throughout is how a monitor can determine when to stop, what to observe, and whom to ask.

Abstract

We introduce a new notion of deterministic stable solution for non-cooperative games, termed subsidized equilibrium. It assumes that an amount of money can be used as a pool of subsidies to stabilize a strategy profile that otherwise would not be accepted by (some of) the players. Roughly speaking, for a given amount of money, a strategy profile is a subsidized equilibrium if the total payoff loss incurred by players not playing best-responses does not exceed that amount, i.e., there is enough money to refund all players experiencing a regret. With respect to many other solution concepts in the literature, the notion of subsidized equilibrium has important advantages. Specifically, for a sufficiently high amount of money, a subsidized equilibrium always exists and can even be computed in polynomial time; also, existence of an efficient subsidized equilibrium can be guaranteed. Thus, determining for which amounts existence, polynomial time computability and efficiency can or cannot be achieved becomes an intriguing question. We provide initial results towards this direction for some widely studied classes of games.