Proving Non-Termination by Acceleration Driven Clause Learning (Short WST Version)

TL;DR

This paper introduces an adaptation of the Acceleration Driven Clause Learning calculus to disprove termination of transition systems, demonstrating its effectiveness through implementation and comparison with existing methods.

Contribution

It extends ADCL to analyze non-termination of transition systems and evaluates its performance in a new tool against current state-of-the-art techniques.

Findings

ADCL effectively disproves termination in transition systems

The implementation outperforms existing methods in certain benchmarks

The approach provides a new way to analyze non-termination

Abstract

We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to disprove termination of transition systems, and we evaluate its implementation in our tool LoAT against the state of the art.