| Summary: | <p>Rational verification asks whether certain temporal properties hold within the equilibria of multi-agent systems. Typically, the literature considers games where the agents traverse some concurrent game structure (or some succinct representation of it), with player goals and specifications given by LTL formulae. Whilst this is an effective framework for reasoning about a variety of different systems, it has two clear shortcomings --- it assumes that agents are unrestricted in choosing their actions, and it only allows two possible player preferences over outcomes: a satisfied temporal goal and an unsatisfied one. Whilst this is sufficient for verifying binary properties (such as safety, fairness and liveness) of a system where agents can act arbitrarily, this framework lacks the ability to differentiate between non-functional behaviours of resource-constrained systems.</p>
<p>For an agent in a system, there may be multiple ways of having it achieve its goal, but these may have different resource requirements (such as energy usage or time expended). As such, it is natural to ask questions like \enquote{does this fleet of autonomous cars have enough power to safely get from point A to point B?} or \enquote{how can these industrial robots perform their respective functions, whilst collectively expending the least amount of battery power?}. These are real world problems which also invoke rich questions in theoretical computer science.</p>
<p>In this thesis, we introduce quantitative aspects to the framework of rational verification. We build on the existing literature by extending the traditional temporal goals of players with mean-payoff rewards; we constrain our agents by making their available actions contingent on resources they possess; and we will look at how quantitative aspects can introduce non-determinism to the rational verification setting.</p>
<p>As such, this will give us games with a greater strategic interest than previously analysed, bringing the theory closer to understanding real-world systems.</p>
|
|---|