
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Monitoring Temporal Properties Using Interval Analysis
Daisuke ISHII Naoki YONEZAKI Alexandre GOLDSZTEJN
Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Vol.E99A
No.2
pp.442453 Publication Date: 2016/02/01
Online ISSN: 17451337
DOI: 10.1587/transfun.E99.A.442
Type of Manuscript: INVITED PAPER (Special Section on Mathematical Systems Science and its Applications) Category: Keyword: continuoustime dynamical systems, interval analysis, linear temporal logic, falsification method,
Full Text: PDF(1.1MB) >>Buy this Article
Summary:
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 continuoustime 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.

