Co-termination

Description of the Case Study

This property asks whether two different programs agree on termination, which can be formalized using a \(∀∀\) HyperLTL formula:

\[\forall \pi_A.\forall \pi_B.\ \Diamond(\mathrm{term}_{\pi_A}) \leftrightarrow \Diamond(\mathrm{term}_{\pi_B}).\]

We consider two simple programs from [UTK21]. In this case, depends on their initial conditions, the programs might either diverge or agree on termination. Co-termination is a non-safety formula; however, our bounded semantics (in particular, opt), is able to give a meaningful verdict even though this is not a finitely-refutable property.

Benchmarks

The Model(s)

-- CO-TERMINATION
-- (adopted from: Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Computer Aided Verification: 33rd International Conference, CAV 2021)

MODULE main

-- 0	while (x>0){
-- 1		x = x - y
-- 2	}
	VAR
		x:-5..100;
		t: 0..1;
		location: 0..2;
		y: 0..5;

	-- FROZENVAR
		-- y: 0..5;

	ASSIGN
		init(location) := 1;
		init(x) := 100;
		init(t) := 0;
  		init(y) := 2;
		next(y) := y;

		next(location) :=
		case
			((location = 1) & (x > 0)): 1;
      ((location = 1) & (x <= 0)) : 2;
      TRUE: location ;
    esac;

    next(x) :=
		case
			((location = 1) & (x > 0)): x - y;
      ((location = 1) & (x <= 0)) : x;
      TRUE : x;
    esac;

    next(t) :=
		case
      (location = 1): 0;
			(location = 2): 1;
      TRUE : t;
    esac;

    DEFINE
			halt := location = 2 ;

Formula

forall A. forall B.
(F(halt[A]))<->(F(halt[B]))