Learning, Approximating and Minimising Streaming Automata for Large-scale Optimisation

这项研究位于验证和机器学习领域的交界处，两者之间的互动是目前备受关注的领域，对双方都有潜在的巨大好处。验证是计算机科学的一个领域，旨在检查和认证计算机系统。计算机系统越来越多地应用于社会和人们生活的各个层面，最重要的是验证它们的行为方式是否符合它们的设计和我们的期望(至关重要的例子包括用于飞机、自动驾驶或自动驾驶汽车的嵌入式软件)。不幸的是，复杂系统的验证遇到了限制：没有通用的全自动方法来验证每个系统，人们需要在时间、存储空间和精度的限制之间找到一个很好的权衡，这些限制往往很难克服。机器学习自50年代S以来一直在研究，最近随着语音识别、图像处理或游戏方面的突破重新引起了人们的关注。神经网络的发展(自60年代S以来一直研究)授予Hinton、LeCun和Bengio 2019年图灵奖，英国公司DeepMind利用深度学习开发了成功的AlphaGo和AlphaGo Zero，这是令人印象深刻的进步，并重申了机器学习的惊人潜力。该项目提出将学习技术应用于验证中，以提高一些验证计算机系统的算法的效率，并为真实系统计算快速准确的模型。自动机是验证中使用的数学工具之一，用于对计算机或现实系统建模。在这些系统上提供认证通常归结为在相应的自动机上运行一些算法。这种算法的效率通常取决于所考虑的自动机的大小。为了更快地验证大型计算机或真实系统，最小化自动机是验证中的一个重要问题。该建议旨在利用机器学习技术来研究一些定量自动机的流模型的最小化问题。我们将要关注的自动机是流模型，从这个意义上说，输入不是存储，而是作为数据流接收，并在运行中处理，因此特别适合处理大数据。它们还适合于处理优化问题，例如最小化系统的资源消耗或计算程序的最坏运行时间。最小化这类自动机具有很高的挑战性，并与确定最大+自动机的长期悬而未决的问题联系在一起。这一建议给出了几个研究方向，例如使用学习方法来解决它。

The proposed research lies at the interface of the areas of verification and machine learning, interactions of which are attracting a lot of attention currently and of potential huge benefits for both sides.Verification is this domain of computer science aiming at checking and certifying computer systems. Computer systems are increasingly used at all levels of society and peoples' lives and it is paramount to verify that they behave the way they are designed to and that we expect (examples of crucial importance, among many others, are embedded software for planes auto-pilot or self-driving cars). Unfortunately, the verification of complex systems encounters limits: there is no universal fully automated way to verify every system and one needs to find a good trade-off between the constraints of time, memory space and accuracy, which are often difficult to overcome.Machine learning has been studied since the 50's and regained much attention recently with breakthroughs in speech recognition, image processing or game playing. The development of neural networks (studied since the 60's) awarded Hinton, LeCun, and Bengio the Turing award 2019 and using deep learning, the British firm DeepMind developed its successful AlphaGo and AlphaGo Zero which were impressive steps forward and reaffirmed the amazing potential of machine learning. This project proposes to apply learning techniques in verification to improve the efficiency of some algorithms which certify computer systems and to compute fast accurate models for real-life systems.Automata are one of the mathematical tools used in verification to model computer or real-life systems. Giving certifications on these systems often boils down to running some algorithms on the corresponding automata. The efficiency of such algorithms usually depends on the size of the considered automaton. Minimising automata is thus a paramount problem in verification, as a way to verify large computer or real-life systems faster.This proposal aims at studying the minimisation of some streaming models of quantitative automata using machine learning techniques. The kind of automata we are going to focus on, are streaming models, in the sense that the input is not stored but received as a stream of data and dealt with on the fly, thus being particularly suitable for the treatment of big data. They are also suited to deal with optimisation problems such as minimising the resource consumption of a system or computing the worst-case running time of a program, for example.Minimising these kind of automata is highly challenging and linked with the long-standing open problem of the determinisation of max-plus automata. This proposal gives several directions of research, such as using learning methods to tackle it.