The seminar of the Formal Methods and Verification group at the Université Libre de Bruxelles usually takes place on Friday from 11:00 to 12:00 in the room «NO.8.Rotule», campus Plaine (show route), and can be accessed remotely via Zoom.

To get informed of current and future seminar via our mailing list (and get the Zoom link), please contact debraj chakraborty ulb ac be or subscribe here, or to our seminar calendar.

Talks in 2022-23

17/10/202311hWojtek Jamroga, University of Luxembourg and Polish Academy of SciencesComputationally Feasible StrategiesReal-life agents seldom have unlimited reasoning power. In this paper,
we propose and study a new formal notion of computationally bounded
strategic ability in multi-agent systems. The notion characterizes the
ability of a set of agents to synthesize an executable strategy in the
form of a Turing machine within a given complexity class, that ensures
the satisfaction of a temporal objective in a parameterized game arena.
We show that the new concept induces a proper hierarchy of strategic
abilities - in particular, polynomial-time abilities are strictly weaker
than the exponential-time ones. We also propose an "adaptive" variant of
computational ability, and show that the two notions do not coincide.
Finally, we define and study the model-checking problem for
computational strategies. We show that the problem is undecidable even
for severely restricted inputs, and present our first steps towards
decidable fragments.
26/05/202311hLeon BohnLearning algorithms for ω-automataThis talk is about the identification of ω-automata from sets of positive and negative ultimately periodic example words. We'll recap the core mechanisms underlying learning algorithms for deterministic finite automata, then illustrate the difficulties one faces in extending these approaches to deterministic ω-automata and finally, we'll discuss a polynomial time algorithm for constructing a deterministic parity automata (DPA) from a given set of positive and negative ultimately periodic example words. This is joint work with Christof Löding. The talk is aimed at a general computer science audience.
16/05/202311hP.2NO9.06Raphaël ReynouardJajapy: a learning library for stochastic modelsStorm and Prism are model checkers that offer different
methods to analyse stochastic models. For some application domains,

the model is not directly available and must be learned from partially-
observable executions of the system under analysis.

We present Jajapy, a python learning library that learns stochastic mod-
els from partially-observable executions of systems. Currently, Jajapy

supports discrete and continuous-time Markov chains, as well as Markov
decision processes. The tool offers different learning techniques, either
based on Expectation-Maximization or state-merging methods, which
have been adapted to the different modelling formats. One key feature
of Jajapy consists in its compatibility with Storm and Prism.
In this work, we briefly present Jajapy’s functionalities and provide an

empirical evaluation of its performance. We conclude with an experimen-
tal comparison of Jajapy against AALpy, which is the current state-
of-the-art Python library for learning automata. Jajapy and AALpy

complement each other, and the selection of the learning library should
be determined by the specific context in which it will be used.
18/04/202311hRotuleLê Thành Dũng (Tito) NguyễnTransducers beyond linear growth: old and newTransducers are finite-state devices that can produce outputs, typically to compute string-to-string functions. The naive way to do so is to add outputs on the transitions of a finite-state automaton, but this results in machines that can only compute functions of linear growth, i.e. |output| = O(|input|). But there are known ways of capturing much larger function classes that still enjoy nice properties (e.g. preserving regular languages by inverse image). Among those, this talk will briefly present:
* the composition hierarchy of macro tree transducers (MTTs), studied by Engelfriet & Vogler in the 1980s, with hyperexponential growth;
* the more recent polyregular functions, with polynomial growth, advocated by Bojańczyk since 2018 as the canonical finite-state counterpart of polynomial-time computation.
We shall then illustrate a connection between the two: the fact that polyregular functions of quadratic growth require an unbounded number of pebbles, first proved by Bojańczyk in a rather technical way, can be easily reduced to old results of Engelfriet & Maneth on MTTs. (This last part is joint work with Sandra Kiefer and Cécilia Pradic, see section 4.)
27/01/202311hRotuleWen-Chi Yang (KULeuven)Safe Reinforcement Learning via Probabilistic Logic ShieldsSafe Reinforcement learning (Safe RL) aims at learning optimal policies while staying safe. A popular solution to Safe RL is shielding, which uses a logical safety specification to prevent an RL agent from taking unsafe actions. However, traditional shielding techniquesare difficult to integrate with continuous, end-to-end deep RL methods. To this end, we introduce Probabilistic Logic Policy Gradient (PLPG). PLPG is a model-based Safe RL technique that uses probabilistic logic programming to model logical safety constraints as differentiable functions. Therefore, PLPG can be seamlessly applied to any policy gradient algorithm while still providing the same convergence guarantees. In our experiments, we show that PLPG learns safer and more rewarding policies compared to other state-of-the-art shielding techniques.
08/12/202211hRotuleLouise Sadoine (UMONS)Towards decentralized Models for day-ahead scheduling of energy resources in Renewable Energy CommunitiesRenewable energy communities (RECs) are one of the driving factors for ensuring the energy transition. These consist in decentralized market mechanisms enabling local electricity exchanges among end-users, and bypass the traditional wholesale/retail market structure. In this configuration, local consumers and prosumers (i.e., consumers who also produce electricity) join together in collectives, known as communities. They can either cooperate or compete to achieve a (possibly common) goal, which may be economic, environmental, or social. We address electricity consumption scheduling on a day-ahead basis within a community of prosumers that own renewable generation. To this end, we mobilize prosumer flexibility to optimize energy exchanges based on the desired objective (e.g. the electricity bill).

First, we establish a typology of community market designs that enable virtuous coordination between members. Among them, we design different centralized and decentralized schemes. In the former, a centralized planner globally optimizes the common objective, while in the latter, each member optimizes its consumption based on its energy preferences. We, therefore, place particular emphasis on modeling strategic behavior. The natural interdependence between members sharing a common network, reflected by an aggregate network tariff component, leads to the formulation of non-cooperative games. In addition, excess rooftop solar power production can be valued inside or outside the community.

We analyze the existence, uniqueness, and computation of Nash equilibria. We use distributed algorithms that ensure confidentiality and do not require third-party intervention. For all different models, we evaluate the efficiency of the results and provide insight into their respective incentives.
25 / 11 / 202211hRotuleLéonard Brice (ULB)To appearTo appear
10 / 11 / 202211hRotuleMrudula Balachander (ULB)LTL Reactive Synthesis with a Few HintsWe study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against a hostile environment. In the variant studied here, the user provides the high level LTL specification φ of the system to design, and a set E of examples of executions that the solution must produce. Our synthesis algorithm works in two phases. First, it generalizes the decisions taken along the examples E using tailored extensions of automata learning algorithms. This phase generalizes the user-provided examples in E while preserving realizability of φ. Second, the algorithm turns the (usually) incomplete Mealy machine obtained by the learning phase into a complete Mealy machine that realizes φ. The examples are used to guide the synthesis procedure. We provide a completness result that shows that our procedure can learn any Mealy machine M that realizes φ with a small (polynomial) set of examples. We also show that our problem, that generalizes the classical LTL synthesis problem (i.e. when E = ∅), matches its worst-case complexity. The additional cost of learning from E is even polynomial in the size of E and in the size of a symbolic representation of solutions that realize φ. This symbolic representation is computed by the synthesis algorithm implemented in Acacia-Bonzai when solving the plain LTL synthesis problem. We illustrate the practical interest of our approach on a set of examples.
14/10/202211hRotulePierre Vandenhove (UMONS)Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite GraphsWe consider zero-sum games on infinite graphs, with objectives specified as sets of infinite words over some alphabet of colors. A well-studied class of objectives is the one of ω-regular objectives, due to its relation to many natural problems in theoretical computer science. We focus on the strategy complexity question: given an objective, how much memory does each player require to play as well as possible? A classical result is that finite-memory strategies suffice for both players when the objective is ω-regular. We show a reciprocal of that statement: when both players can play optimally with a chromatic finite-memory structure (i.e., whose updates can only observe colors) in all infinite game graphs, then the objective must be ω-regular. This provides a game-theoretic characterization of ω-regular objectives, and this characterization can help in obtaining memory bounds. Moreover, a by-product of our characterization is a new one-to-two-player lift: to show that chromatic finite-memory structures suffice to play optimally in two-player games on infinite graphs, it suffices to show it in the simpler case of one-player games on infinite graphs. We illustrate our results with the family of discounted-sum objectives, for which ω-regularity depends on the value of some parameters.
21/10/202211hRotuleGaëtan Staquet (UMONS)Learning Realtime One-Counter AutomataWe present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin's L* algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.
30/09/202211hRotuleAntonio Paolillo (Huawei)Enabling Performance on Concurrent Modern Hardware with Practical Verification Modern commodity hardware is very diverse.
On many-core servers, different core pairs within the same processor may communicate with different speeds due to deep memory hierarchies (caches, NUMA memory, etc.).
On embedded systems, groups of cores can have different processing and energy consumption specifications (e.g. big.LITTLE architectures).
Moreover, on some architectures, memory operations can be reordered in a multitude of ways.

To build efficient systems, software designers cannot treat cores as homogeneous, freely exchangable processing units.
Algorithms, specially concurrent algorithms, have to be aware of the hardware heterogeneity to be able to exploit it.
Unfortunately, awareness has an intrinsic cost: complexity.

In this talk, we argue that some level of formal verification is a requisite for system builders willing to take the next step in the design of concurrent algorithms.
Without that, systems are doomed to fail in the most unpredictable and unreproducible ways.
We review and connect a few of our success stories and draw a path for the future work."
02/09/202211hRotuleFrank Cassez (ConsenSys Software R&D)Deductive Verification of Smart Contracts with DafnyWe present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary reentrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to EVM bytecode, the results we obtain on the Dafny code can reasonably be assumed to hold on Solidity code: the translation of the Dafny code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.

Joint work with Joanne Fuller and Horacio Mijail Ant´on Quiles
Link to paper:

Past Talks

Edwin Hamel-De le Court (ULB)

Two-Player Boundedness Counter Games

Ayrat Khalimov (ULB)

Recent Developments in Register-Bounded Synthesis

Benedikt Maderbacher (IAIK, TU Graz)

Reactive Synthesis modulo Theories

Amazigh Amrane (Rouen Normandy University)

Logic and Rational Languages of Scattered and Countable Series-Parallel Posets

Sayan Mukherjee (Chennai Mathematical Institute)

Reachability in Timed Automata with Diagonal Constraints and Updates

Anirban Majumdar (LSV & INRIA Rennes)

Parameterized Concurrent Games

Chana Weil-Kennedy (TU Munich)

Verification of Immediate Observation Petri Nets

Léo Henry (IRISA)

Active learning of timed automata with unobservable resets

Edwin Hamel (IRIF)

An algebraic theory for state complexity

Clément Tamines (University of Mons)

Stackelberg-Pareto Synthesis

Léonard Brice (ULB)

Subgame-perfect equilibria in mean-payoff games

Sarah Winter (ULB)

Synthesizing computable functions from synchronous specifications

Satya Prakash Nayak (Chennai Mathematical Institute)

Robust Linear Temporal Logics

Debraj Chakraborty (ULB)

Monte Carlo Tree Search guided by Symbolic Advice for MDPs

Raphaël Berthon (ULB & University of Antwerp)

Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes

Léo Exibard (ULB & Aix-Marseille Université)

Computability and Continuity of Data Word Functions Defined by Transducers

Ayrat Khalimov (ULB)

Church Synthesis on Register Automata over Infinite Ordered Domains

Older archives