Communicating finite-state machines (CFMs) are a Turing powerful model of
asynchronous message-passing distributed systems. In weakly synchronous
systems, processes communicate through phases in which messages are first sent
and then received, for each process. Such systems enjoy a limited form of
synchronization, and for some communication models, this restriction is enough
to make the reachability problem decidable. In particular, we explore the
intriguing case of p2p (FIFO) communication, for which the reachability problem
is known to be undecidable for four processes, but decidable for two. We show
that the configuration reachability problem for weakly synchronous systems of
three processes is undecidable. This result is heavily inspired by our study on
the treewidth of the Message Sequence Charts (MSCs) that might be generated by
such systems. In this sense, the main contribution of this work is a weakly
synchronous system with three processes that generates MSCs of arbitrarily
large treewidth.

在弱同步系统中，我们研究了有限状态机和异步消息传递分布式系统，特别是对于 p2p (FIFO) 通信，我们证明了三个进程的弱同步系统的配置可达性问题是不可判定的，并且其生成的消息序列图具有任意大的树宽。

三台弱同步系统的图灵能力

Weakly synchronous systems with three machines are Turing powerful

Verifying correctness of deep neural networks (DNNs) is challenging. We study
a generic reachability problem for feed-forward DNNs which, for a given set of
inputs to the network and a Lipschitz-continuous function over its outputs,
computes the lower and upper bound on the function values. Because the network
and the function are Lipschitz continuous, all values in the interval between
the lower and upper bound are reachable. We show how to obtain the safety
verification problem, the output range analysis problem and a robustness
measure by instantiating the reachability problem. We present a novel algorithm
based on adaptive nested optimisation to solve the reachability problem. The
technique has been implemented and evaluated on a range of DNNs, demonstrating
its efficiency, scalability and ability to handle a broader class of networks
than state-of-the-art verification approaches.

本文研究针对前馈深度神经网络的通用可达性问题，通过计算输出函数值的下限和上限，得到区间范围内的可达值，从而得出安全性验证问题、输出范围分析问题和鲁棒性度量，并通过自适应嵌套优化的新算法，有效地解决了可达性问题。

使用可证明保证的方式对深度神经网络进行可达性分析

Reachability Analysis of Deep Neural Networks with Provable Guarantees

We study the reachability problem for systems implemented as feed-forward
neural networks whose activation function is implemented via ReLU functions. We
draw a correspondence between establishing whether some arbitrary output can
ever be outputed by a neural system and linear problems characterising a neural
system of interest. We present a methodology to solve cases of practical
interest by means of a state-of-the-art linear programs solver. We evaluate the
technique presented by discussing the experimental results obtained by
analysing reachability properties for a number of benchmarks in the literature.

研究使用 ReLU 函数实现激活函数的前馈神经网络系统的可达性问题，并通过线性问题对其进行表征，并提出了一种基于最先进的线性规划求解器解决实际问题的方法。通过分析文献中的多个基准测试来评估所提出技术的性能。