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
| Date | Time | Room | Speaker | Title | Abstract |
|---|---|---|---|---|---|
| 17/10/2023 | 11h | Wojtek Jamroga, University of Luxembourg and Polish Academy of Sciences | Computationally Feasible Strategies | Real-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/2023 | 11h | Leon Bohn | Learning algorithms for ω-automata | This 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/2023 | 11h | P.2NO9.06 | Raphaël Reynouard | Jajapy: a learning library for stochastic models | Storm 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/2023 | 11h | Rotule | Lê Thành Dũng (Tito) Nguyễn | Transducers beyond linear growth: old and new | Transducers 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 https://arxiv.org/pdf/2301.09234.pdf section 4.) |
| 27/01/2023 | 11h | Rotule | Wen-Chi Yang (KULeuven) | Safe Reinforcement Learning via Probabilistic Logic Shields | Safe 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/2022 | 11h | Rotule | Louise Sadoine (UMONS) | Towards decentralized Models for day-ahead scheduling of energy resources in Renewable Energy Communities | Renewable 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 / 2022 | 11h | Rotule | Léonard Brice (ULB) | To appear | To appear |
| 10 / 11 / 2022 | 11h | Rotule | Mrudula Balachander (ULB) | LTL Reactive Synthesis with a Few Hints | We 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/2022 | 11h | Rotule | Pierre Vandenhove (UMONS) | Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs | We 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/2022 | 11h | Rotule | Gaëtan Staquet (UMONS) | Learning Realtime One-Counter Automata | We 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/2022 | 11h | Rotule | Antonio 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/2022 | 11h | Rotule | Frank Cassez (ConsenSys Software R&D) | Deductive Verification of Smart Contracts with Dafny | We 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: https://arxiv.org/abs/2208.02920 |
Past Talks
| 10/06/2022 14:00 |
(ULB)
Two-Player Boundedness Counter Games |
| 20/05/2022 14:00 |
(ULB)
Recent Developments in Register-Bounded Synthesis |
| 23/02/2022 14:00 |
(IAIK, TU Graz)
Reactive Synthesis modulo Theories |
| 01/10/2021 14:00 |
(Rouen Normandy University)
Logic and Rational Languages of Scattered and Countable Series-Parallel Posets |
| 22/09/2021 10:00 |
(Chennai Mathematical Institute)
Reachability in Timed Automata with Diagonal Constraints and Updates |
| 15/09/2021 10:00 |
(LSV & INRIA Rennes)
Parameterized Concurrent Games |
| 07/07/2021 11:00 |
(TU Munich)
Verification of Immediate Observation Petri Nets |
| 26/05/2021 11:00 |
(IRISA)
Active learning of timed automata with unobservable resets |
| 28/04/2021 11:00 |
(IRIF)
An algebraic theory for state complexity |
| 24/03/2021 11:00 |
(University of Mons)
Stackelberg-Pareto Synthesis |
| 13/01/2021 & 20/01/2021 11:00 |
(ULB)
Subgame-perfect equilibria in mean-payoff games |
| 04/01/2021 14:00 |
(ULB)
Synthesizing computable functions from synchronous specifications |
| 16/12/2020 11:00 |
(Chennai Mathematical Institute)
Robust Linear Temporal Logics |
| 09/12/2020 11:00 |
(ULB)
Monte Carlo Tree Search guided by Symbolic Advice for MDPs |
| 02/12/2020 11:00 |
(ULB & University of Antwerp)
Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes |
| 30/11/2020 14:00 |
(ULB & Aix-Marseille Université)
Computability and Continuity of Data Word Functions Defined by Transducers |
| 18/11/2020 11:00 |
(ULB)
Church Synthesis on Register Automata over Infinite Ordered Domains |