<p>In this paper we study monitoring of real-time systems with respect to properties given by a pair of Timed Büchi Automata, one for the property and one for its complement. This includes properties expressible in temporal logics that are closed under complementation and can be translated into Timed Büchi Automata, e.g., Metric Interval Temporal Logic. We introduce efficient symbolic online monitoring algorithms in a number of settings, using difference bound matrices representing zones. Our contributions include a principled treatment of time divergence and monitoring under timing uncertainty. Our online monitoring procedure is implemented in the tool <span>MoniTAal</span>, and shown to effectively monitor properties over long traces.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Efficient monitoring of timed properties

  • Thomas Møller Grosen,
  • Sean Kauffman,
  • Kim Guldstrand Larsen,
  • Martin Zimmermann

摘要

In this paper we study monitoring of real-time systems with respect to properties given by a pair of Timed Büchi Automata, one for the property and one for its complement. This includes properties expressible in temporal logics that are closed under complementation and can be translated into Timed Büchi Automata, e.g., Metric Interval Temporal Logic. We introduce efficient symbolic online monitoring algorithms in a number of settings, using difference bound matrices representing zones. Our contributions include a principled treatment of time divergence and monitoring under timing uncertainty. Our online monitoring procedure is implemented in the tool MoniTAal, and shown to effectively monitor properties over long traces.