Academic Year 23-24
Automatic synthesis of reactive systems with registers
Promotor: Emmanuel Filiot (efiliot@ulb.be)
Objective: The goal of synthesis is to automatically generate a program from specifications of the properties the program must fulfil, instead of how it must satisfy them. This allows to obtain programs which are correct *by construction*. In this master thesis, the goal is to implement a synthesis algorithm for programs which can be represented as register automata, i.e. automata with registers which can store input data, and compare incoming data to those stored in the registers. Such automata can model reactive systems, which are non-terminating systems in interaction with the environment in which they are executed. The internship will consider specifications both expressed as automata and logical formulas.
The work will be based on research papers such as
Léo Exibard, Emmanuel Filiot, Ayrat Khalimov: A Generic Solution to Register-Bounded Synthesis with an Application to Discrete Orders. ICALP 2022: 122:1-122:19
Please contact the promotor for more details.
Learning algorithm for register automata.
Promotor: Emmanuel Filiot (efiliot@ulb.be)
Objective: learning algorithms for regular languages have been investigated for long. The goal of this thesis is to lift some of those algorithms to regular languages of *data words*. Data words are words over an infinite alphabet of data (integers, reals, etc.). Regular languages of data words are for instance defined as languages recognizable by register automata, i.e. automata with registers which can store input data, and compare incoming data to those stored in the registers. The first goal of the thesis will be to understand a standard algorithm in passive learning of regular languages, called RPNI, and to work on its extension to data word languages.
Please contact the promotor for more details.
Factorization forests and applications
Promotor: Emmanuel Filiot (efiliot@ulb.be)
Objective: Factorization forests are a powerful mathematical abstraction in automata theory, at the heart of important theoretical results. Factorization theorems can be seen as fine-grained pumping lemmas, and intuitively provide a useful description of the structure of cycles in runs of automata.
The goal of this thesis is first to understand the theory behind factorization forests and the proof of the seminal factorization forest of Simon. Then, the thesis will seek for new factorizations theorems in non-standard automata models, and/or new applications of existing factorization theorems.
One of the starting research paper is https://www.mimuw.edu.pl/~bojan/papers/forests-dlt.pdf
Please contact the promotor for more details.
Implementation of a forward algorithm for reactive synthesis
Promotor: Emmanuel Filiot (efiliot@ulb.be)
Objective: The goal of synthesis is to automatically generate a program from specifications of the properties the program must fulfil, instead of how it must satisfy them. This allows to obtain programs which are correct *by construction*. In this master thesis, the goal is to implement a synthesis algorithm for programs which can be represented as Mealy machines, within the tool Acacia-Bonzai. Many of the sub-procedures which are necessary to implement this algorithm are already implemented in Acacia-Bonzai. In the preparatory step, the goal is to understand the theory behind this algorithm. A participation to the synthesis competition SYNTCOMP will be considered if the implementation is efficient.
Reference paper: Emmanuel Filiot, Naiyong Jin, Jean-François Raskin: Antichains and compositional algorithms for LTL synthesis. Formal Methods Syst. Des. 39(3): 261-296 (2011)
Reference on Acacia-bonzai: https://arxiv.org/pdf/2204.06079.pdf
Please contact the promotor for more details.
Reactive synthesis from LTL specification and examples
Promotor: Jean-Francois Raskin (jraskin@ulb.ac.be)
Objective: The goal of this project is to synthesize Mealy machines that enforce LTL specifications against all possible behaviours of the environment including hostile ones. In the variant studied here, the user provides the high level LTL specification {\phi} of the system to design, and a set E of examples of executions that the solution must produce. The 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 {\phi}. Second, the algorithm turns the (usually) incomplete Mealy machine obtained by the learning phase into a complete Mealy machine that realizes {\phi}. The examples are used to guide the synthesis procedure. The goal of the Master thesis is to extend the existing tool with a notion of symbolic example where the examples are giving as Boolean formulas. The synthesis tool is then expected to synthesise symbolic Mealy Machines instead of plain Mealy machines.
Reference: https://arxiv.org/abs/2301.10485
Please contact the promotor for more details.
Mixing formal methods and deep learning
Promotor: Jean-Francois Raskin (jraskin@ulb.ac.be)
Objective: In previous works (see below), we have studied how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce high-
quality receding horizon policies in large Markov Decision processes (MDPs). In particular, we use model-checking techniques to guide the MCTS algorithm in order to generate offline samples of high-quality decisions on a representative set of states of the MDP. Those samples can then be used to train a neural network that imitates the policy used to generate them. This neural network can either be used as a guide on a lower-latency MCTS online search, or alternatively be used as a full-fledged policy when minimal latency is required. We use statistical model checking to detect when additional samples are needed and to focus those additional samples on configurations where the learnt neural network policy differs
from the (computationally-expensive) offline policy. We illustrate the use of our method on MDPs that model the Frozen Lake and Pac-Man environments — two popular benchmarks to evaluate reinforcement-learning algorithms.
The master thesis will consist in applying those new techniques to a challenging new case study.
References:
- https://doi.org/10.1007/978-3-030-85172-9_13
- https://drops.dagstuhl.de/opus/volltexte/2020/12852/
- https://www.dropbox.com/s/b5id4ils4o442hb/StormMCTS.pdf?dl=0
Please contact the promotor for more details.
Using random tree forests to guide MCTS for solving large MDPs
Supervisors: Prof. Gianluca Bontempi and Jean-François Raskin
In previous research efforts (refer to the references below), we have explored the effective integration of formal methods, Monte Carlo Tree Search (MCTS), and deep learning to craft high-quality receding horizon policies for handling large Markov Decision Processes (MDPs). Specifically, we leverage model-checking techniques to steer the MCTS algorithm, enabling the generation of offline samples that embody high-quality decisions across a representative subset of the MDP’s states. These generated samples subsequently serve as the foundation for training a neural network that emulates the policy used in their creation.
This neural network assumes a dual role: it can function as a guiding agent for a lower-latency MCTS online search, or it can operate independently as a comprehensive policy when minimizing latency is a critical requirement. We employ statistical model checking as a means to identify situations where additional samples are necessary and to focus these supplementary samples on configurations where the learned neural network policy diverges from the computationally-intensive offline policy.
To exemplify the applicability of our approach, we conduct experiments on MDPs that simulate environments like Frozen Lake and Pac-Man—two well-established benchmarks for assessing reinforcement-learning algorithms.
The subject of this master thesis is to evaluate the replacement of neural networks by random forests of decision trees. In particular, we would like to compare their accuracy in predicting safe actions in the applications mentioned above. We aim also at comparing the number of sample that random forests need in comparison with neural networks for generalising the decision taken by the MCTS algorithm augmented with the model-checking algorithms.
Elements of bibliography:
https://doi.org/10.1007/978-3-030-85172-9_13
https://drops.dagstuhl.de/opus/volltexte/2020/12852/
https://www.dropbox.com/s/b5id4ils4o442hb/StormMCTS.pdf?dl=0
Please contact the promotor for more details.
Generating data for learning a neural network to solve instances of the Robbins’ problem
Supervisors: Prof. Jean-François Raskin
In the field of probability theory, the problem of optimal stopping, known as Robbins’ problem in honor of Herbert Robbins, is a variation of the secretary problem. It falls under the broader category of problems related to minimizing the expected stoping rank when full information is available.
Consider a sequence of independent and identically distributed random variables, denoted as X1, X2, …, Xn, with each variable uniformly distributed in the interval [0, 1]. Our objective is to sequentially observe these variables and select exactly one of them to stop the process. The key question is: What stopping rule should be employed to minimize the expected rank of the chosen observation, and what is the corresponding value of this rule?
It is worth noting that a general solution to this problem of minimizing the expected rank with full information remains elusive.
Within the scope of this thesis, the primary focus will be dedicated to the following objectives:
1) Investigating the methodologies for generating data to be used in supervised learning in order to train of a neural network for solving the Robbins’ problem.
2) Delving into the determination of an optimal network architecture that is apt for learning effective strategies to tackle the problem at hand.
3) Investigating methods to extend these approaches for handling larger values of n, and assessing the network’s performance in relation to the known theoretical results on this problem.
Elements of bibliography:
https://web.archive.org/web/20060830123936id_/http://www.math.ucla.edu/~tom/papers/exprank.pdf
This subject will be realised in collaboration with with Prof. Thomas Bruss (from the math department at ULB) who is a central contributor to the theoretical study of this problem.
Please contact the promotor for more details.
Using model-checking algorithms and Monte Carlo tree search algorithms for search near optimal strategies in the Robbins’ problem
Supervisor : Prof. Jean-François Raskin
In the field of probability theory, the problem of optimal stopping, known as Robbins’ problem in honor of Herbert Robbins, is a variation of the secretary problem. It falls under the broader category of problems related to minimizing the expected rank when full information is available.
Consider a sequence of independent and identically distributed random variables, denoted as X1, X2, …, Xn, with each variable uniformly distributed in the interval [0, 1]. Our objective is to sequentially observe these variables and select exactly one of them to stop the process. The key question is: What stopping rule should be employed to minimize the expected rank of the chosen observation, and what is the corresponding value of this rule?
It is worth noting that a general solution to this problem of minimizing the expected rank with full information remains elusive.
The focus of this master’s thesis is to explore and apply precise computational methods alongside sampling techniques to determine optimal strategies for instances of the Robbins’ problem where the exact optimal value is currently unknown. This research will encompass the utilization of model-checking algorithms and the implementation of the Monte Carlo tree search algorithm. These computational tools will be harnessed to compute optimal or nearly optimal strategies for this intriguing problem. Consequently, this work will largely revolve around the adaptation and implementation of advanced search algorithms, which have not yet been fully leveraged in the context of this challenging problem.
Elements of bibliography:
https://web.archive.org/web/20060830123936id_/http://www.math.ucla.edu/~tom/papers/exprank.pdf
This subject will be realised in close collaration with Prof. Thomas Bruss (from the math department at ULB) who is a central contributor to the theoretical study of this problem.