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

用于大规模优化的学习、逼近和最小化流自动机

• 批准号: EP/T018313/1
• 负责人: Laure Daviaud
• 金额: $ 31.79万
• 依托单位: City, University of London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FT018313%2F1
• 关键词: Learning; Approximating; Minimising; Streaming; Automata

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.

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

项目成果

When are emptiness and containment decidable for probabilistic automata?

概率自动机什么时候可以判定空性和包含性？

• DOI: 10.1016/j.jcss.2021.01.006
• 发表时间: 2021
• 期刊: Journal of Computer and System Sciences
• 影响因子: 1.1
• 作者: Daviaud L

The Big-O Problem for Max-Plus Automata is Decidable (PSPACE-Complete)

Max-Plus 自动机的 Big-O 问题是可判定的（PSPACE-Complete）

• DOI: 10.1109/lics56636.2023.10175798
• 发表时间: 2023
• 作者: Daviaud L

Formal and Empirical Studies of Counting Behaviour in ReLU RNNs

• 发表时间: 2023
• 作者: Nadine El-Naggar;Andrew Ryzhikov;Laure Daviaud;P. Madhyastha;Tillman Weyde;François Coste;Faissal Ouardi;Guillaume Rabusseau

Feasability of Learning Weighted Automata on a Semiring

• DOI: 10.48550/arxiv.2309.07806
• 发表时间: 2023-09
• 期刊: ArXiv
• 作者: Laure Daviaud;Marianne Johnson