Time robustness in MTL and expressivity in hybrid system falsification

DOI10.1007/978-3-319-21668-3_21zbMATH Open1381.68142arXiv1505.06307OpenAlexW2167799541MaRDI QIDQ1702902FDOQ1702902

Authors: Takumi Akazaki, Ichiro Hasuo 

Publication date: 1 March 2018

Abstract: Building on the work by Fainekos and Pappas and the one by Donze and Maler, we introduce AvSTL, an extension of metric interval temporal logic by averaged temporal operators. Its expressivity in capturing both space and time robustness helps solving falsification problems, (i.e. searching for a critical path in hybrid system models); it does so by communicating a designer's intention more faithfully to the stochastic optimization engine employed in a falsification solver. We also introduce a sliding window-like algorithm that keeps the cost of computing truth/robustness values tractable.

Full work available at URL: https://arxiv.org/abs/1505.06307

Recommendations

• S-TaLiRo: a tool for temporal logic falsification for hybrid systems
• scientific article; zbMATH DE number 1444348
• Falsification of hybrid systems using symbolic reachability and trajectory splicing
• Hybrid Systems: From Verification to Falsification
• Falsification of hybrid systems with symbolic reachability analysis and trajectory splicing
• Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness
• A Temporal Dynamic Logic for Verifying Hybrid System Invariants
• scientific article; zbMATH DE number 1696448
• Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic

Mathematics Subject Classification ID

Sensitivity (robustness) (93B35) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Temporal logic (03B44)

Cited In (10)

• Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness
• Robust control for signal temporal logic specifications using discrete average space robustness
• Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
• Title not available (Why is that?)
• Algebraic quantitative semantics for efficient online temporal monitoring
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• From LTL to rLTL monitoring: improved monitorability through robust semantics
• Quantitative monitoring of STL with edit distance
• On the Expressiveness of MTL Variants over Dense Time
• A few lessons learned in reinforcement learning for quadcopter attitude control

This page was built for publication: Time robustness in MTL and expressivity in hybrid system falsification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1702902)