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.
STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version)
ENS de Lyon(里昂高等师范学院);National Institute of Informatics(国立情报学研究所);SOKENDAI (The Graduate University for Advanced Studies)(综合研究大学院大学);Institute of Software, Chinese Academy of Sciences(中国科学院软件研究所);Kyushu University(九州大学);Imiron Co., Ltd.(Imiron有限公司)
Control Synthesis for Multi-Agent Systems under Metric Interval Temporal Logic Specifications
ACCESS Linnaeus Center, School of Electrical Engineering and KTH Center for Autonomous Systems, KTH Royal Institute of Technology(林奈 ACCESS 中心、电气工程学院及 KTH 自主系统中心,KTH 皇家理工学院)
Learning Linear Temporal Specifications from Demonstrations with Uncertainty
The Pennsylvania State University(宾夕法尼亚州立大学);School of Electrical Engineering and Computer Science at The Pennsylvania State University(宾夕法尼亚州立大学电气工程与计算机科学学院)
Quantitative Monitoring of Signal First-Order Logic
Zeroth Research(零次研究);Institute of Science and Technology Austria(奥地利科学技术研究所);CISPA Helmholtz Center for Information Security(CISPA赫尔姆霍兹信息安全中心);Leiden University(莱顿大学)
Signal Temporal Logic Motion Planning via Graphs of Convex Sets
School of Automation & Intelligent Sensing, Shanghai Jiao Tong University(自动化与智能感知学院,上海交通大学);Institute of Artificial Intelligence, Xiamen University(人工智能研究院,厦门大学)