Model Synthesis and Satisfiability Checking for STCTL, ATL, and SL with Simple Goals
Across Alliance — e-Campus
Description
Model synthesis and satisfiability checking are fundamental problems in the design and verification of multi-agent systems. In this talk, we present a unified perspective on recent advances in satisfiability checking and synthesis for strategic logics, focusing on STCTL, ATL, and Strategy Logic with simple goals (SL[SG]).
We discuss novel methods based on SAT Modulo Monotonic Theories (SMMT) and SMT solving, enabling efficient reasoning about complex temporal and strategic specifications under both perfect and imperfect information. The presented approaches are implemented in tools such as MsATL, SGSAT, and SMT4STECTL, which extend existing model checking techniques with satisfiability checking and automatic synthesis capabilities.
These tools allow not only to verify whether a given specification is consistent, but also to automatically construct models and strategies satisfying it. Experimental results demonstrate that the proposed methods scale well and can handle problems beyond the reach of existing approaches. Applications include controller synthesis, automated planning, and prototyping of real-time multi-agent systems under strategic and timing constraints.
Details
| Type | Atomic Learning Unit |
| Modality | Hybrid |
| Language(s) | EN |
| Teacher(s) | Magdalena Kacprzak |
| University | Bialystok University of Technology |
Schedule
- Timezone: Europe/Berlin
- Start date: 2026-04-17
- End date: 2026-04-20
- Repeat frequency: Once
- Time slots: 11:30 - 13:30
Registration
Registration has closed (2026-04-20 12:30)