Scholarlink

<p>This paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic (<span>ltl</span>) with second-order quantifiers. Behavioral <span>qltl</span> is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other words, such functions must be “processes”&#xa0;(Abadi et al., Realizable and Unrealizable Specifications of Reactive Systems, <CitationRef CitationID="CR1">1989</CitationRef>) . This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and ltl synthesis are expressed in Behavioral <span>qltl</span> through formulas with a simple quantification alternation. As such alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original <span>qltl</span> (with non-behavioral semantics) and simpler forms of behavioral semantics.</p>

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

Behavioral QLTL

  • 期刊论文

  • 发表日期：

    2025年6月30日

查看全文
  • Giuseppe De Giacomo,
  • Giuseppe Perelli

摘要

This paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic (ltl) with second-order quantifiers. Behavioral qltl is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other words, such functions must be “processes” (Abadi et al., Realizable and Unrealizable Specifications of Reactive Systems, 1989) . This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and ltl synthesis are expressed in Behavioral qltl through formulas with a simple quantification alternation. As such alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original qltl (with non-behavioral semantics) and simpler forms of behavioral semantics.