Neural networks as a machine learning technique are increasingly deployed in various domains. Despite their performance and their continuous improvement, the deployment of neural networks in safety-critical systems, in particular for autonomous mobility, remains restricted. This is mainly due to the lack of (formal) specifications and verification methods and tools that allow for having sufficient confidence in the behavior of the neural-network-based functions. Recent years have seen neural network verification getting more attention; many verification methods were proposed, yet the practical applicability of these methods to real-world neural network models remains limited. The main challenge of neural network verification methods is related to the computational complexity and the large size of neural networks pertaining to complex functions. As a consequence, applying abstraction methods for neural network verification purposes is seen as a promising mean to cope with such issues. The aim of abstraction is to build an abstract model by omitting some irrelevant details or some details that are not highly impacting w.r.t some considered features. Thus, the verification process is made faster and easier while preserving, to some extent, the relevant behavior regarding the properties to be examined on the original model. In this article, we review both the abstraction techniques for activation functions and model size reduction approaches, with a particular focus on the latter. The review primarily discusses the application of abstraction techniques on feed-forward neural networks and explores the potential for applying abstraction to other types of neural networks. Throughout the article, we present the main idea of each approach and then discuss its respective advantages and limitations in detail. Finally, we provide some insights and guidelines to improve the discussed methods.

Neural networks (NNs) have witnessed widespread deployment across various domains, including some safetycritical applications. In this regard, the demand for verifying means of such artificial intelligence techniques is more and more pressing. Nowadays, the development of evaluation approaches for NNs is a hot topic that is attracting considerable interest, and a number of verification methods have been proposed. Yet, a challenging issue for NN verification is pertaining to the scalability when some NNs of practical interest have to be evaluated. This work aims to present INNAbstract, an abstraction method to reduce the size of NNs, which leads to improving the scalability of NN verification and reachability analysis methods. This is achieved by merging neurons while ensuring that the obtained model (i.e., abstract model) overapproximates the original one. INNAbstract supports networks with numerous activation functions. In addition, we propose a heuristic for nodes' selection to build more precise abstract models, in the sense that the outputs are closer to those of the original network. The experimental results illustrate the efficiency of the proposed approach compared to the existing relevant abstraction techniques. Furthermore, they demonstrate that INNAbstract can help the existing verification tools to be applied on larger networks while considering various activation functions.

Diagnosability of faults in discrete event systems modeled with Petri nets can be assessed either via graph-based techniques (also called diagnoser, verifier/twin-plant based techniques), or via the solution of optimization problems. The approaches that belong to the former class are based on the analysis of the net reachability or coverability graphs (or of a more compact version of them). The latter approach exploits the mathematical representation of the net itself to specify and solve optimization problems, which are usually expressed as integer linear programming (ILP) problems. In this paper we exploit the railway Petri net model originally proposed in [16], and extended in [14] to be used as a benchmark for diagnosability analysis, to assess the efficiency of the approach based on the solution of ILP problems proposed in [3]. In order to show the effectiveness of the proposed technique, a comparison with a graph-based approach for analyzing diagnosability is also presented.

This paper deals with a benchmark-based experimental comparison of three diagnoser-based approaches for fault diagnosis of discrete event systems modeled by Petri nets: the MBRG/BRD approach, the FMG/FMSG approach and the SSD approach. The experiments are performed on a level crossing benchmark, using the respective software tools integrating the approaches. Different features are shown in terms of state-space building (exhaustive or partial), procedure for analyzing diagnosability (based on complete or on-the-fly built state-space) and state-space representation (concrete or symbolic). Based on the obtained experimental results, a comparative discussion is provided particularly regarding memory and time consumption for analyzing diagnosability of the three techniques.