CONFEST 2026

The 9th International Workshop on Symbolic and Numerical Reasoning about games (SNR)

Games are a fundamental framework for modelling interaction and strategic behaviour in verification, synthesis and logic. Reasoning about games often requires a combination of symbolic methods, such as strategy improvement, fixpoint computation, automata-theoretic techniques, and logical encodings, with numerical methods, such as value iteration, policy iteration, approximation, and quantitative optimisation.

The goal of the SNR (Symbolic and Numerical Reasoning about games) workshop is to provide a platform for exploring symbolic and numerical techniques for reasoning about games, with applications in verification, synthesis, reactive systems, probabilistic models, and related areas.

SNR will be held on Saturday 5 September 2026.

Call for submissions

SNR solicits submissions for contributed talks in the form of extended abstracts (LIPIcs style, upto 2 pages without reference). We encourage submissions of ongoing works and new results as well as works published elsewhere. All submissions will undergo a lightweight peer-reviewing process. Authors of selected submissions presenting original unpublished work will subsequently be invited to submit a full version of their work for publication in formal proceedings, to be published by EPTCS.

Submissions are judged on the expected interest and relevance to the theme of the workshop. The topics include (but are not limited to) :

Submissions should be made via EasyChair https://easychair.org/conferences/?conf=snr26.

Program Committee

K. S. Thejaswini (Université Libre de Bruxelles)
Mickael Randour (FRS - FNRS and UMONS - Université de Mons)
Suman Sadhukhan (TU Clausthal)
Aline Goeminne (ENS Rennes, IRISA)
Sven Schewe (University of Liverpool)
Ashutosh Trivedi (University of Colorado, Boulder) (PC Chair)
Dominik Wojtczak (University of Liverpool)
Anirban Majumdar (TIFR, Mumbai)

Invited Talks

Munyque Mittelmann, CNRS, LIPN, Université Sorbonne-Paris-Nord

Can We Change the Game? Reasoning about Dynamic Multi-Agent Systems

Abstract Most research on logics for strategic reasoning in Multi-Agent Systems (MAS) has traditionally focused on static models, such as concurrent game structures, which represent a fixed set of system configurations and the transitions between them. Such models are unable to capture scenarios where the system’s structure undergoes dynamic changes, whether triggered by agent actions or caused by an external factor.  As MAS increasingly operate in dynamic and unpredictable settings, their design and maintenance require reasoning about how structural changes affect system behavior. When existing models fail to produce desirable outcomes or are incorrect, computing repairs offers an alternative to complete redesigns. This talk explores recent advances in logic-based methods for dynamic MAS, including reasoning about model modifications and repairing flawed games.

Prince Mathew, Université Libre de Bruxelles (ULB)

Active Learning for the Synthesis of POMDP Policies

Abstract Partially Observable Markov Decision Processes (POMDPs) are a fundamental model for decision-making under uncertainty, with applications ranging from robotics and autonomous systems to planning and verification. However, synthesising correct policies for POMDPs is, in general, undecidable. Existing approaches face a fundamental trade-off. Sampling-based techniques, such as reinforcement learning and Monte Carlo methods, scale well to large problems but provide no formal correctness guarantees, making them unsuitable for safety-critical applications. In contrast, formal synthesis techniques offer correctness-by-construction but often struggle to scale. In this talk, I will present a synthesis framework that combines automata learning, model checking, and policy-generation techniques to bridge this gap. Inspired by Angluin's L* algorithm, the framework views policy generation as a membership oracle and model checking as an equivalence oracle to actively learn finite-state controllers. The membership oracle can be instantiated by any algorithm capable of suggesting a suitable action for a given action-observation history. I will present the theoretical foundations of the framework and show that it is relatively complete: whenever the policy induced by the membership oracle is regular, the algorithm is guaranteed to synthesise a correct finite-state controller. Finally, I will present experimental results demonstrating that the proposed method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. This work illustrates how active learning provides a principled bridge between scalable policy-generation techniques and formal methods, opening a promising new direction for POMDP policy synthesis.

Organisers

Sougata Bose
Soumyajit Paul
Ashutosh Trivedi
Dominik Wojtczak

Previous Editions