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

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

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

(11)

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

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)