Assistant Professor. Research: multi-agent systems, formal verification, runtime verification, distributed systems. Core contributor to VITAMIN; teaching experience in software methods, algorithms, and distributed systems.
Half-day tutorial · In-person · AAMAS 2026
Don’t Trust Your Agents, Verify Them Strategic Verification with VITAMIN
Strategic properties talk about abilities, coalitions, and adversaries — not just how systems evolve over time. This tutorial gives you a practical workflow with VITAMIN: modelling choices, strategic specifications, and model checking tasks.
ATL / CTL basics
Concurrent game structures
Coalitional abilities
Model checking workflows
Abstract
Context. Many properties of interest in multi-agent systems concern not only how systems evolve over time, but also what agents (or coalitions) can achieve by choosing their actions strategically — e.g., coordination guarantees, enforceability of norms, robustness against misbehaviour, or the ability of a coalition to achieve goals despite adversarial behaviour.
Approach. This tutorial introduces VITAMIN (VerIficaTion of A MulTI-Agent system), a compositional and extensible framework designed to make strategic verification more accessible and practically usable. VITAMIN supports expressive temporal and strategic logics, heterogeneous agent models, and flexible verification workflows, with guided steps that help users construct models, specify properties, and execute verification tasks.
Detailed outline
Half-day in-person tutorial · approx. 3.5 hours technical content.
30 min
Introduction and motivation
Why strategic verification for MAS? From temporal properties to strategic abilities. Domains and challenges.
45 min
Background: strategic logics and agent models
CTL/ATL intuition, concurrent game structures, strategies & coalitions, modelling assumptions and limits.
45 min
Strategic verification in VITAMIN
Architecture & components. Supported logics and tasks. Verification workflows.
60 min
Hands-on modelling and verification
Build a model, write strategic specifications, execute tasks, analyse and discuss results.
30 min
Discussion and outlook
Open research challenges, industrial relevance, Q&A.
Target audience
Researchers, PhD students, and practitioners working on multi-agent systems, formal methods, and autonomous systems. Advanced MSc students with a background in AI or distributed systems may also benefit.
Prerequisites
- Basic knowledge of multi-agent systems.
- Familiarity with temporal logic is helpful but not required.
- No prior experience with strategic logics or VITAMIN is expected.
Presenters
Contact details for questions, collaboration, and tutorial logistics.
Associate Professor. Research: multi-agent systems, formal specification and verification, temporal and strategic logics, game-theoretic reasoning. Active contributor to the VITAMIN framework.