Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans
Cyber-Physical Systems (CPSs) are systems with both physical and software components, for example cars and industrial robots. Since these systems exhibit both discrete and continuous dynamics, they are complex and it is thus difficult to verify that they behave as expected. Falsification of temporal logic properties is an approach to find counterexamples to CPSs by means of simulation. In this paper, we propose two additions to enhance the capability of falsification and make it more viable in a large-scale industrial setting. The first addition is a framework for transforming specifications from a signal-based model into Signal Temporal Logic. The second addition is the use of Valued Booleans and an additive robust semantics in the falsification process. We evaluate the performance of the additive robust semantics on a set of benchmark models, and we can see that which semantics are preferable depend both on the model and on the specification.
Code (0)
등록된 구현이 없습니다.
Tasks
Industrial RobotsSimilar Papers 제목 키워드 기반
Falsification-Based Robust Adversarial Reinforcement Learning
Reinforcement learning (RL) has achieved enormous progress in solving various sequential decision-making problems, such as control tasks in robotics. Since policies are overfitted to training environments, RL methods hav…
Autonomous VehiclesDecision Makingreinforcement-learningReinforcement Learning+2Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
Cyber-physical systems (CPS), such as automotive systems, are starting to include sophisticated machine learning (ML) components. Their correctness, therefore, depends on properties of the inner ML modules. While learnin…
BIG-bench Machine LearningFalsification-driven reinforcement learning for maritime motion planning
Compliance with maritime traffic rules is essential for the safe operation of autonomous vessels, yet training reinforcement learning (RL) agents to adhere to them is challenging. The behavior of RL agents is shaped by t…
Reinforcement LearningMotion PlanningExploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals
In this paper, we consider an analysis of temporal properties of hybrid systems based on simulations, so-called falsification of requirements. We present a novel exploration-based algorithm for falsification of black-box…
Motion PlanningNExG: Provable and Guided State Space Exploration of Neural Network Control Systems using Sensitivity Approximation
We propose a new technique for performing state space exploration of closed loop control systems with neural network feedback controllers. Our approach involves approximating the sensitivity of the trajectories of the cl…
Sensitivity