Author name cluster

Marcelo Forets

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 2022 Journal Article

Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version)

Sergiy Bogomolov
Marcelo Forets
Goran Frehse
Andreas Podelski
Christian Schilling

Approximating the set of reachable states of a dynamical system is an algorithmic way to rigorously reason about its safety. Despite progress on efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in practice. While modern linear algebra packages are efficient for matrices with tens of thousands of dimensions, set-based image computations are limited to a few hundred. We propose to decompose reach-set computations such that set operations are performed in low dimensions, while matrix operations are performed in the full dimension. Our method is applicable in both dense- and discrete-time settings. For a set of standard benchmarks, we show a speed-up of up to two orders of magnitude compared to the respective state-of-the-art tools, with only modest loss in accuracy. For the dense-time case, we show an experiment with more than 10, 000 variables, roughly two orders of magnitude higher than possible before.

Details DOI

AAAI Conference 2022 Conference Paper

Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes

Christian Schilling
Marcelo Forets
Sebastián Guadalupe

We study the verification problem for closed-loop dynamical systems with neural-network controllers (NNCS). This problem is commonly reduced to computing the set of reachable states. When considering dynamical systems and neural networks in isolation, there exist precise approaches for that task based on set representations respectively called Taylor models and zonotopes. However, the combination of these approaches to NNCS is non-trivial because, when converting between the set representations, dependency information gets lost in each control cycle and the accumulated approximation error quickly renders the result useless. We present an algorithm to chain approaches based on Taylor models and zonotopes, yielding a precise reachability algorithm for NNCS. Because the algorithm only acts at the interface of the isolated approaches, it is applicable to general dynamical systems and neural networks and can benefit from future advances in these areas. Our implementation delivers stateof-the-art performance and is the first to successfully analyze all benchmark problems of an annual reachability competition for NNCS.

PDF Details