Exploiting Adjoints in
Property Directed ReachabilityAnalysis.
Mayuko Kowi"YRoberta Gori,Flavio Ascar:"

Filippo Bouch: Roberto Bruni

1,2

Ichiro Hasuoof Informatics
University for Advanced Studies (SOKENDAI)

1. National Institute2.

The Graduate

3.

Universita di Pisain

CAV'23

Property Directed ReachabilityAnalysis (PAR)Model checking Algorithm for Safety->·problems of State transition systems.

original: IC3/PAR (Bradley, VMCAI'll], [Eent, FMCAD'll]
active researches:

GPER CHoderaBjquner,SAT), fdPAR (Senfert scholl, PATE'18,19], A-PCAR sFeldmant, POPLaLSHGPAR [Suenaga&Ishizana, UMCA[2], Pr IC3 [Batz+, CAV'cOS,a-lattice theoretic generalization:LT- PAR [Kovit, Cavius-

positive side
search forinvariant

Negative side
helpeach other--search forcounterexample

verifil safetyproblem Irefute1Problem Setting:General Safety Problem
ug= P

monotonein

1.

whereL:complete lattice, g: L-L,PEL

frame (i=S,6:S PS)
e.g.1 safety problem for Kripke+initialMi)??Yoein4S&

↳

e.g.

max
...

IBa

reachable States2I->

reachabilityproblem for MAP 1"=S, 8: SxA &S+1)+Pr (teachingbadIS) < X for given x- (0.1)

mg = ip,in C0.13S

Idefined byBellman operator~&-> SoG.
->

Ii aO
2

Contribution 1. Adjoint PAR
generalization of PAR
We assume mg<"4 satisfies
g fri,=Positive side

search forinvariantin Lf forward
anL

I--

L

alois-..

Econnection
C↓ backward

Negative side
helpeach other--fold works wellsearch forcounterexamplein L

verifie mg="pin L k refute~safety problem for Kripke frameX
maxreachabilityproblem for MAP

3

Contribution 2. Adjoint PARYfor mgsipwithout f-d,Positive side

invariantin LnV

We recover adjoints with lower sets (4search forlift

8G L>-LI-L↓DEq↓↓--14

Negative side
helpeach othersearch for

89I works wellcounterexample

-↓

-1

↓

in L

verifie mg="pin L I refute~max reachability
problem->-for MAP

Mathematically simple PAR by adjoints.
Abstract theory helps devising heuristics

4Outline
1.

Adjoint PAR

2.

AdjointPARY

3.

Experiments--

generalization of CAR
extension ofAdjoint PARTarget Problem of Adjoint PAR

mg=" P (with g:fvi,Yeft(f,g:1 -1,2,peL)

inadjoint.

f (forward (andLL-L+...

forward/backward adjointb (backward(e.g. safetyproblem for aKripke frame (S,i=$,8: S+4S).

M()) vi) ="pin4S
left adjoint

USA forwardwithn-I
PS 4S[S18s=(-1] backward5

Forward/Backward form of mg="p withg fri,=Target prob.
=Mg P

inL->

KTE)

u(fri) P=Ex.ffavi
Px =Eforward↳,LWf (forward)-↳LLb (backward)

CKT:Kuaster Tarskithm)-Ex.[fx=xc =i=Pze.? cp
EkT

Ex.!

=idep
-Dv(dv4)=backward>

6f (forward)

How to solve?

yeg?"4 backward form:↑1, forward

II~form:

ByKleene thm,

initial chain

Lb (backward)

12>

final chain?

u(fri)."Pirfic...
7

i =v(d-p)-inI-ir(b 14)i =ByKleene them,converge

L-2.

ulfvi) "ptoL.

.

.

-6p-p=4 =T
S-ulfrilconverge to r(b -p)

AdjointPDR.
2 i,negative

se4.

VI

j

14 =...

VI↓ =11. ...
positivechain=Y-...

9-En-1over-approx.
↑Papproximation
under-approx.
↳accelerates[An-2?CurSVI

I=TVI

VIVfic.

VIover-approx.

Ithe algorithm.

7

Adjoint PDRsolves mg pin (with g= fvi, f-b.

positive chain

Do[2, ... [C(n-1negative seq
Ye, ..., Jn-1

extendchain
positive

Constructnegative sea.

refine approximationIshrink overly-inflated

users

needtopositivechainC

specify heuristics.

1,

how to constructnegative sep. 1.

2,

how to shrink overly-inflated positive chain. 2.

8Propertyof Adjoint P.DR
The. Soundness

If AdjointPAR returns true/false then u(fri) <p(ulfri) *p.
Thm. ProgressionIn

any run, there'snoloop.

Thm. Negative Termination

If e (fri) IPandJn-1) is finite,y=(40,Yat1."

AdjointPAR terminates - This holds
whenorLis finite

whenever we use canonical choicep..mainI (pr=9Outline
1.

Adjoint PAR

2.

AdjointPARY

3.

Experiments--

generalization of CAR
extension ofAdjoint PAR

ug=? 4 without f- de.g.

max

Bellmanreachabilityproblem for MDP (A.S," ES, 8: SxA S+1)+f(d: Soperator =[0.13) S4max2sds'. SIS, a,s')-=-bada->if SEL[!

i Sri aO

otherwise

then m(fri) SHPrCreachingso&bad=& IS froms) in [0.1]S[0,13PrCreaching & from So) < "x in?

I=u(fri)=So A
--1

S

inso,

13

have
I
rightadjoint... any left adjointpreserve joins.
abut
so thisproblem

isf(divdz) + f(d,) vf(d)).

of scope of AdjointPAR.

out10

adjoints with lower
Recovering

sets9921283-V
w-contiq((L,)-LI-:

grIL,E)D I\y19y=(-3I always have( ) [xk= (- 3-=

Target prob.

pinh->tmay↓

But Lis too↓in↓L.

neecan solve.

solve

large=- Adjoint PAR

AdjointPAR
notn(g) 14) i4-

toof positive chain
convergencegetAdjointPARYuses positive chain x

sonegative sepin L

Sacceleration.
A set ofIin L4.
sep. yin LYnegativeme EofAdjoint PAR.

11

Adjoint PARtsolves

mg.p inL.

almostthe same as

AdjointPCR

exceptfor negative sea.

positivechainDoICIC...

[An-negative Se4.
Yes,... Yn-1inL

specify heuristics.

users

need1,

how to2,

how to shrink

toinL

constructnegative sep. Y.

overly-inflated positive chain. 2.

12

of Adjoint PDR
FryThe. Soundness↓

If AdjoutPAR returns true/false then Mg=p/mg AP.
Thm. ProgressionIn

any run, there's

noloop.

-Thm. Negative termination(YE, YEt1...., Yuri) is finite,
Y:↓
This holds
terminates.
AdjointPAR

If mgup

andwhenever

we usecanonical choice

Y (gtt..., grpt, gipt, p")=<Final chain13

AdjointPARY for MAPs
reachabilityproblem for MDP (S04S, 8: S xA S+1)
some bad states
Pr (reaching& IS)?"X for given x-(0.1)
+max
...

LFP problem w.r.t.Bellman operator#Ids'. S/S, a,s')
s max
at AS

Canonical heuristics based on final chain.

Yar

↓

=

[d- [0.13d(S0) x3,=x], Yu-3, Yana....
Yn-2 EdmaxIds'. SCSo,a.S1) ==at A Sx

negativenatullarly get

Our heuristics:

Bychoosinga"eMscheduler,Ye can be expresseddtermination

holds.

-by inequality.

⑧⑳

Yaof

itshrink() by taking meetof erors

D~ for-&shrinking>52

I'll show itgives practical performance in experiments.
14

Outline
1.

Adjoint PAR

2.

AdjointPARY

3.

Experiments--

generalization of CAR
extension of

Adjoint PAR

Experiment
We implementedain
Haskell.
forPAR"
Adjoint
generic template

By specifying heuristics, users get->aninstance.

(e.g. instance for Kripke frame, MDP, ...)
We comparedtoan instance

LT-PARI

Skorit.cAv22s

PrIC3of

AdjointPAR for MAPs

PAR algorithms for MAPs.

[Batz+, CAV20]

Storm

I non-PAR algorithm for MAPs.

(Dehnert+,CA VII]

machine:Ubuntu 18.04. 4CPUs, 16GB memory, up to 3.0 GHz

Intel Scalable Processor.

15

Results Comparison to LT-PDR, PrIC3 (PARalgorithms ([Kowit,[BatzCAV22]+,CAV20]

P Pr) reaching bad states)?"X=

Adjoint PARY outperformed

LT-PAR.

Adjoint PAR outperformed PrIC3 exceptwhen polynomial and hybrid in PrIC3

potential improvement:use polynomialorhybrid template.

perform well.
16

ResultsComparisonStormtoC non-PAR algorithm)(Dehnert +, cAv'I]

P Pr) reaching bad states)?"X=sp. -num.:Value iteration alg.
itmay

while

return a wrong answer

AdjintPDR is precise.

sp.-rat:exact model
sp. -Sd.:sound model

Dchecking-↑↓

sparcity may imcrove

Storm waschecking

return wrong

4(=0.5)faster than AdjointPARin many benchmarks.

/

well with Storm ina couple of benchmarks.
compared
AdjointPAR
although↓potential improvement:use space representation.

17Conclusions
Two PAR algorithms got byadjoints.
exploiting
f1.
2.

AdjointPAR for mg="pwith g fr i,·Recover f+bThe->

with lower sets.

We successfully derived↳

L+-bAdjoint PARfor mg="4--L=cgGSforward)I->(backward)

L gtigr↓-tpracticalperformance for MAPs

isheuristics

from canonical one.

encouraging.

Mathematically simple PAR by adjoints.
Abstract theory helps devising heuristics
18