Scholarlink

Linear Temporal Logic is a de facto standard for specification of properties of complex systems. Fundamental problems in formal verification include satisfiability checking and model checking. Extensions and variants of LTL have gained significant interest: with \(\textit{LTL}_f\) , the temporal formulas are interpreted over finite traces; with safety fragments of LTL, model checking can be reduced to search for finite trace counterexamples; in the context of Verification Modulo Theories, LTL includes first-order atoms interpreted over background theories. In this paper we propose a symbolic, automata-theoretic approach for these variants of LTL in a general and comprehensive framework, show the correctness of the reduction to liveness and invariant checking, and present a library of open benchmarks and support tools.

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

Another Look at LTL Modulo Theory over Finite and Infinite Traces

  • 章节

  • 发表日期：

    2025年

查看全文
  • Alberto Bombardelli,
  • Alessandro Cimatti,
  • Alberto Griggio,
  • Stefano Tonetta

摘要

Linear Temporal Logic is a de facto standard for specification of properties of complex systems. Fundamental problems in formal verification include satisfiability checking and model checking. Extensions and variants of LTL have gained significant interest: with \(\textit{LTL}_f\) , the temporal formulas are interpreted over finite traces; with safety fragments of LTL, model checking can be reduced to search for finite trace counterexamples; in the context of Verification Modulo Theories, LTL includes first-order atoms interpreted over background theories. In this paper we propose a symbolic, automata-theoretic approach for these variants of LTL in a general and comprehensive framework, show the correctness of the reduction to liveness and invariant checking, and present a library of open benchmarks and support tools.