Scholarlink

<p>We introduce a novel lattice-theoretic verification algorithm inspired by Bradley’s property directed reachability. For finding safe invariants or counterexamples, the algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use a second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.</p>

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

Adjointness in property directed reachability analysis

  • 期刊论文

  • 发表日期：

    2026年7月7日

查看全文
  • Mayuko Kori,
  • Flavio Ascari,
  • Filippo Bonchi,
  • Roberto Bruni,
  • Roberta Gori,
  • Ichiro Hasuo

摘要

We introduce a novel lattice-theoretic verification algorithm inspired by Bradley’s property directed reachability. For finding safe invariants or counterexamples, the algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use a second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.