Papers for

automotive control developers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Efficient methods to combine timed system contracts for safety design

Computing GR(1) Assume-Guarantee Contracts

Abstract: Assume-guarantee contracts provide a set of algebraic operations that enable the efficient compositional design and analysis of complex engineering systems. The explicit computation of these operations at component interfaces is currently supported only for some logics lacking a notion of time. This paper develops theory and algorithms to compute these operations when the contracts are expressed in the GR(1) modulo theory. The key challenge is the computation of two quantifier elimination problems for temporal formulas. We develop context-aided variable elimination procedures on GR(1)-modulo formulas, establish their soundness, characterize subproblem-wise optimal solutions within an admissible class of formulas, and use the procedures to compute contract operations, including composition and quotient. We implement the resulting framework in Pacti, automating compositional reasoning over GR(1) contracts. Finally, we demonstrate the framework on an automated emergency-braking case study, where we compute system-level contracts and expose compatibility conditions arising from the interaction of component specifications. Experiments on synthetic families show that the cost is governed by the number of eliminated variables and liveness conjuncts, and a comparison with exact automata-based elimination shows complementary scaling.

Tue 27 OctLogic in Computer Science
The gist
Designing complex systems often means combining lots of rules about how components assume things about each other and guarantee behaviors. Existing methods only worked well when time wasn’t considered. The authors developed new math and algorithms to handle these assume-and-guarantee contracts when time matters, specifically using a type of logic called GR(1). They built tools that automatically work out how different parts fit together and tested this on emergency braking systems, showing how to spot if parts will work safely together.
Open → 2610.37534v1

Warmstarting cuts verification time for neural networks

Exploring Solver-Level Warmstarting for Neural Network Verification

Abstract: Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, we explore the application of solver-level warmstarting for neural network verification to exploit information from previous solutions. We study the effect on running time as several properties are modified, including perturbation radii, input data and the networks themselves, using a pipeline that is generalisable and potentially adaptable to state-of-the-art verifiers. Our results show that warmstarting can significantly reduce verification time in most cases. Moreover, warmstarting enables the successful verification of instances that could not be solved from scratch within the given time limit.

Tue 22 SeptMachine Learning
The gist
Checking that neural networks behave correctly can be very slow or even impossible when done from scratch. The authors studied a way to speed up these checks by starting the verification process using hints from previous runs. They tested this idea with different changes to the network and inputs. Their experiments showed that warmstarting often makes the verification faster and sometimes even solves problems that were too hard before.
Open → 2609.25962v1