首页    期刊浏览 2025年07月17日 星期四
登录注册

文章基本信息

  • 标题:Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker
  • 本地全文:下载
  • 作者:Geatti, Luca ; Gigante, Nicola ; Montanari, Angelo
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2021
  • 卷号:206
  • DOI:10.4230/LIPIcs.TIME.2021.8
  • 语种:English
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.
  • 关键词:SAT;LTL;LTL+Past;Tableaux
国家哲学社会科学文献中心版权所有