Due to the considerable data amount produced by the vehicle’s perception sensors, there is the need to investigate techniques to reduce the datarate, e.g. for camera, well established lossy compression techniques can be explored and evaluated. These techniques must be analysed in combination with the consumer of the data, which will most likely be a perception algorithm based on deep neural networks (DNNs). This work shows that compression tuned DNNs have enhanced performance with respect to traditionally trained DNNs, and the performance is higher when evaluating not only compressed data, but also uncompressed data. Overall, the DNN performance is steady when transmitting data with increasing lossy compression rate (up to~130:1), but above this value there is a performance decrease. The results presented in this work demonstrate that compression can be used in automotive sensors, particularly leveraging the hereby proposed and optimised compression-tuned DNNs. The full paper is available at DOI: 10.1109/TITS.2023.3308344.

Situational awareness based on the data collected by the vehicle perception sensors (i.e. LiDAR, RADAR, camera and ultrasonic sensors) is key for achieving assisted and automated driving functions in a safe and reliable way. However, the data rates generated by the sensor suite are difficult to support over traditional wired data communication networks on the vehicle, hence there is an interest in techniques that reduce the amount of sensor data to be transmitted without losing key information or introducing unacceptable delays. These techniques must be analysed in combination with the consumer of the data, which will most likely be a machine learning algorithm based on deep neural networks (DNNs). In this paper we demonstrate that by compression tuning the DNNs (i.e. transfer learning by re-training with compressed data) the DNN average precision and recall can significantly improve when uncompressed and compressed data are transmitted. This improvement is achieved independently from the compression standard used for compression-training (i.e. AVC and HEVC), and also when training and transmitted data use the same compression standard or different compression standards. Furthermore, the performance of the DNNs is stable when transmitting data with increasing lossy compression rate, up to a compression ratio of approximately 160:1; above this value the performance starts to degrade. This work paves the way for the use of compressed sensor data in automated driving in combination with the optimisation of compression-tuned DNNs.

We have developed a new approximate probabilistic model-checking method for untimed properties in probabilistic systems, expressed in a probabilistic temporal logic (PCTL, CSL). This method, in contrast to the existing ones, does not require the untimed until properties to be bounded a priori, where the bound refers to the number of discrete steps in the system required to verify the until property. The method consists of two phases. In the first phase, a suitable system- and property-dependent bound k 0 is obtained automatically. In the second phase, the probability of satisfying the k 0 -bounded until property is computed as the estimate of the probability of satisfying the original unbounded until property. Both phases require only verification of bounded until properties, which can be effectively performed by simulation-based methods. We prove the correctness of the proposed two-phase method and present its optimized implementation in the widely used PRISM model-checking engine. We compare this implementation with sampling-based model-checking techniques implemented in two tools: PRISM and MRMC. We show that for several models these existing tools fail to compute the result, while the two-phase method successfully computes the result efficiently with respect to time and space.

We study the problem of statistical model checking of probabilistic systems for PCTL unbounded until property PJoinp(Æ1UÆ2) (where Join |X| {<, d, >, e}) using the computation of P d 0(Æ1UÆ2). The approach is first proposed by Sen et al. in CAV'05 but their approach suffers from two drawbacks. Firstly, the computation of Pd0Æ1UÆ2) requires for its validity, a user-specified input parameter ´2 which the user is unlikely to correctly provide. Secondly, the validity of computation of Pd0Æ1UÆ2) is limited only to probabilistic models that do not contain loops. We present a new technique which addresses both problems described above. Essentially our technique transforms the hypothesis test for the unbounded until property in the original model into a new equivalent hypothesis test for bounded until property in our modified model. We empirically show the effectiveness of our technique and compare our results with those using the method proposed by Sen et al.