Monitoring Bounded LTL Properties Using Interval Analysis

详细信息    查看全文

• 作者：Daisuke Ishii ^{dsksh@acm.org" class="auth_mail" title="E-mail the corresponding author} ; Naoki Yonezaki ^{yonezaki@cs.titech.ac.jp" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Hybrid systems ; interval analysis ; linear temporal logic ; bounded model checking
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2015
• 出版时间：18 November 2015
• 年：2015
• 卷：317
• 期：Complete
• 页码：85-100
• 全文大小：341 K

文摘

Verification of temporal logic properties plays a crucial role in proving the desired behaviors of hybrid systems. In this paper, we propose an interval method for verifying the properties described by a bounded linear temporal logic. We relax the problem to allow outputting an inconclusive result when verification process cannot succeed with a prescribed precision, and present an efficient and rigorous monitoring algorithm that demonstrates that the problem is decidable. This algorithm performs a forward simulation of a hybrid automaton, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. A continuous state at a certain time computed in each step is enclosed by an interval vector that is proven to contain a unique solution. In the experiments, we show that the proposed method provides a useful tool for formal analysis of nonlinear and complex hybrid systems.