Papers

Peer-reviewed Lead author Corresponding author Open access International coauthorship
2016

Monitoring Temporal Properties Using Interval Analysis.

IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
  • Daisuke Ishii
  • ,
  • Naoki Yonezaki
  • ,
  • Alexandre Goldsztejn

Volume
99-A
Number
2
First page
442
Last page
453
Language
English
Publishing type
Research paper (scientific journal)
DOI
10.1587/transfun.E99.A.442
Publisher
IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG

Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by an efficient and rigorous monitoring algorithm. This algorithm performs a forward simulation of a continuous-time dynamical system, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. In each step, the continuous state at a certain time is enclosed by an interval vector that is proven to contain a unique solution. We experimentally demonstrate the utility of the proposed method in formal analysis of nonlinear and complex continuous systems.

Link information
DOI
https://doi.org/10.1587/transfun.E99.A.442
DBLP
https://dblp.uni-trier.de/rec/journals/ieicet/IshiiYG16
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000376162600002&DestApp=WOS_CPL
URL
https://arxiv.org/abs/1602.02387 Open access
ID information
  • DOI : 10.1587/transfun.E99.A.442
  • ISSN : 1745-1337
  • DBLP ID : journals/ieicet/IshiiYG16
  • Web of Science ID : WOS:000376162600002

Export
BibTeX RIS