Abstract
The two big recent trends in formal verification are verifying multi-agent systems (as opposed to two-agent systems) and using finite-horizon goals (as opposed to infinite-horizon goals). Combining these two settings results in a framework with an interesting motivation and interesting mathematical properties. In this talk, I will present complexity-theoretic results that provide insight into the driving forces of complexity when multiple agents interact -- a mathematical model that appears everywhere, from game theory to the analysis of distributed systems. I will also discuss some interesting use cases and interactions that arise when finite-horizon goals are considered. Finally, I will talk about the problem of representation, which lies at the heart of any complexity-theoretic result on multi-agent systems.