In this work, we propose the use of symbolic automata as formal specifications for reinforcement learning agents. The use of symbolic automata serves as a generalization of both bounded-time temporal logic-based specifications and deterministic finite automata, allowing us to describe input alphabets over metric spaces. Furthermore, our use of symbolic automata allows us to define non-sparse potential-based rewards which empirically shape the reward surface, leading to better convergence during RL. We also show that our potential-based rewarding strategy still allows us to obtain the policy that maximizes the satisfaction of the given specification.

In cyber-physical systems (CPS), physical behaviors are typically controlled by digital hardware. As a consequence, continuous behaviors are discretized by sampling and quantization prior to their processing. Quantifying the similarity between CPS behaviors and their specification is an important ingredient in evaluating correctness and quality of such systems. We propose a novel procedure for measuring robustness between digitized CPS signals and signal temporal logic (STL) specifications. We first equip STL with quantitative semantics based on the weighted edit distance , a metric that quantifies both space and time mismatches between digitized CPS behaviors. We then develop a dynamic programming algorithm for computing the robustness degree between digitized signals and STL specifications. In order to promote hardware-based monitors we implemented our approach in FPGA. We evaluated it on automotive benchmarks defined by research community, and also on realistic data obtained from magnetic sensor used in modern cars.

Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPSs). Modern RV tools also allow to measure the distance of a CPS behavior from a given formal requirement, thus, to quantify the robustness of a CPS with respect to perturbations caused by the physical environment. In this paper, we propose algebraic RV (ARV), a general, semantic framework for correctness and robustness monitoring. ARV implements an abstract monitoring procedure, in which the specification language (STL) can be instantiated with various qualitative and quantitative semantics. This allows us to expose the core aspects of RV, by separating the monitoring algorithm from the concrete choice of the STL and its semantics. We demonstrate the effectiveness of our framework on two examples from the automotive domain.

Due to the heterogeneity and complexity of systems-of-systems (SoS), their simulation is becoming very time consuming, expensive and hence impractical. As a result, design simulation is increasingly being complemented with more efficient design emulation. Runtime monitoring of emulated designs would provide a precious support in the verification activities of such complex systems. We propose novel algorithms for translating signal temporal logic (STL) assertions to hardware runtime monitors implemented in field programmable gate array (FPGA). In order to accommodate to this hardware specific setting, we restrict ourselves to past and bounded future temporal operators interpreted over discrete time. We evaluate our approach on two examples: the mixed signal bounded stabilization property and the serial peripheral interface (SPI) communication protocol. These case studies demonstrate the suitability of our approach for runtime monitoring of both digital and mixed signal systems.