IEICE TRANSACTIONS on Fundamentals
Monitoring Temporal Properties Using Interval Analysis
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
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
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://global.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 -
English
