Checking Temporal Properties of Presburger Counter Systems using Reachability Analysis

TL;DR

This paper introduces semi-decision techniques for verifying liveness and CTL properties in Presburger counter systems, leveraging reachability analysis as a black box to achieve precise and approximate results.

Contribution

It presents novel semi-decision methods for checking temporal properties of counter systems using reachability analysis, enabling wider applicability and incremental approximation.

Findings

Techniques compute exact reachable states satisfying liveness properties.

Methods allow iterative expansion or contraction for approximate solutions.

Experimental results demonstrate effectiveness on standard benchmarks.

Abstract

Counter systems are a well-known and powerful modeling notation for specifying infinite-state systems. In this paper we target the problem of checking temporal properties of counter systems. We first focus on checking liveness properties only, and propose two semi decision techniques for these properties. Both these techniques return a formula that encodes the set of reachable states of a given system that satisfy a given liveness property. A novel aspect of our techniques is that they use reachability analysis techniques, which are well studied in the literature, as black boxes, and are hence able to compute precise answers on a much wider class of systems than previous approaches for the same problem. Secondly, they compute their results by iterative expansion or contraction, and hence permit an approximate solution to be obtained at any point. We state the formal properties of our techniques, and also provide experimental results using standard benchmarks to show the usefulness of our approaches. Finally, we provide a technique for checking arbitrary CTL temporal properties, which use the liveness property checking techniques mentioned above as black boxes.