Monitoring Temporal Properties Using Interval Analysis

Daisuke ISHII; Naoki YONEZAKI; Alexandre GOLDSZTEJN

doi:10.1587/transfun.E99.A.442

Monitoring Temporal Properties Using Interval Analysis

Daisuke ISHII, Naoki YONEZAKI, Alexandre GOLDSZTEJN

Full Text Views

0

Share
Cite this

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 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.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E99-A No.2 pp.442-453

Publication Date: 2016/02/01

Publicized

Online ISSN: 1745-1337

DOI: 10.1587/transfun.E99.A.442

Type of Manuscript: Special Section INVITED PAPER (Special Section on Mathematical Systems Science and its Applications)

Category

Authors

Daisuke ISHII
  Tokyo Institute of Technology
Naoki YONEZAKI
  Tokyo Institute of Technology
Alexandre GOLDSZTEJN
  CNRS/IRCCyN

Keyword

continuous-time dynamical systems, interval analysis, linear temporal logic, falsification method

Cite this

Copy

Daisuke ISHII, Naoki YONEZAKI, Alexandre GOLDSZTEJN, "Monitoring Temporal Properties Using Interval Analysis" in IEICE TRANSACTIONS on Fundamentals, vol. E99-A, no. 2, pp. 442-453, February 2016, doi: 10.1587/transfun.E99.A.442.
Abstract: 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.
URL: https://globals.ieice.org/en_transactions/fundamentals/10.1587/transfun.E99.A.442/_p

Copy

@ARTICLE{e99-a_2_442,
author={Daisuke ISHII, Naoki YONEZAKI, Alexandre GOLDSZTEJN, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Monitoring Temporal Properties Using Interval Analysis},
year={2016},
volume={E99-A},
number={2},
pages={442-453},
abstract={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.},
keywords={},
doi={10.1587/transfun.E99.A.442},
ISSN={1745-1337},
month={February},}

Copy

TY - JOUR
TI - Monitoring Temporal Properties Using Interval Analysis
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 442
EP - 453
AU - Daisuke ISHII
AU - Naoki YONEZAKI
AU - Alexandre GOLDSZTEJN
PY - 2016
DO - 10.1587/transfun.E99.A.442
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E99-A
IS - 2
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - February 2016
AB - 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.
ER -