Time robustness in MTL and expressivity in hybrid system falsification

DOI10.1007/978-3-319-21668-3_21MaRDI QIDQ1702902zbMATH OpenOpenAlexFDO

Authors Takumi Akazaki, Ichiro Hasuo

Publication date 1 March 2018

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

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)

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.

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

Cited in

(10)

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

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)