Co-termination (NuSMV)

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: 0..100;
		t: 0..1;
		location: 0..2;
		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]))

References