Model Checking: A Remedy for State Explosion

Proof Script Generationfrom Proof Scores (2)Kazuhiro Ogata (JAIST, Japan)
i628e information processing theory

FY2019i628e information processing theory

2

Motivation
Proof tree

A proof can be regarded as a tree.
Goal (theorem to prove)

An instance of a proof rule
✔

✔

✔ ✔

For example,
✔

✔

0

∀ :

⇒
∀ :

1

FY2019i628e information processing theory

3

Motivation
Proof assistantA sequence of commands (or tactics),
or a proof script
Pros : it guarantees that once a proof
is done, it is correct.

✔

✔

✔

✔ ✔

✔

Pros : less flexible

FY2019i628e information processing theory

Motivation
Proof scores

Proofs (or proof plans) written in an alg. spec. lang.

Pros : flexible, can be written as
programs, etc.
Cons : subject to human errors

Only consisting of the leaf nodes ofa proof tree

4

FY2019i628e information processing theory

5

Motivation
Would like to check if proof scores are correct
One possible way to do so is to construct (or infer) proof
scripts from proof scores

✔

✔

✔

FY2019✔ ✔

✔

i628e information processing theory

Outline
1. Review of lecture 1
2. CiMPA – CafeInMaude Proof Assistant
3. CiMPG – CafeInMaude Proof Generator
4. Summary & future directions

6

FY2019i628e information processing theory

7

Review of lecture 1
A mutual exclusion protocol called Qlock, an abstract
version of the Dijkstra binary semaphore.
Pseudo code for process p:
Loop “Remainder Section”
rs: enqueue(queue,p);
ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);
Each process p is located at rs, ws or cs.
Initially, p is located at rs & queue is empty.

FY2019i628e information processing theory

Review of lecture 1
Treating states as black boxes but possible to observe
values from them. Given a state & a process ID ,queue

the content ofpc ,the location where process is locatedused in Qlock

queue & pc are called observer functions.
Let init be an arbitrary initial state.
empty .
eq queue init
eq pc init,
rs .

8

FY2019i628e information processing theory

9

Review of lecture 1
ceq pc(want(S,I),J)= (if I = J then ws else pc(S,J) fi)
if c-want(S,I) .
ceq queue(want(S,I)) = enq(queue(S),I) if c-want(S,I) .
ceq want(S,I)=S
if not c-want(S,I) .
where c-want(S,I) = (pc(S,I) = rs)spc(s,i)) = rs
Loop “Remainder Section”
rs: enqueue(queue);ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);

FY2019s' = want(s,i)

pc(s',i)) = ws
pc(s',j) = pc(s,j) if i jqueue(s') = enq(queue(s),i)want is called a transition functions.

i628e information processing theory

10

Review of lecture 1
ceq pc(try(S,I),J)= (if I = J then cs else pc(S,J) fi)
eq queue(try(S,I)) = queue(S) .
ceq try(S,I)=S

if c-try(S,I) .
if not c-try(S,I) .

where c-try(S,I) = (pc(S,I) = ws) and top(queue(S)) = I)ss' = try(s,i)
pc(s,i)) = ws
top(queue(s)) = i
Loop “Remainder Section”
rs: enqueue(queue);ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);pc(s',i)) = cs
pc(s',j) = pc(s,j) if iqueue(s') = queue(s)try is called a transition functions.

jFY2019i628e information processing theory

11

Review of lecture 1
ceq pc(exit(S,I),J)= (if I = J then rs else pc(S,J) fi)
if c-exit(S,I) .
ceq queue(exit(S,I)) = deq(queue(S)) if c-exit(S,I) .
ceq exit(S,I)=S
if not c-exit(S,I) .
where c-exit(S,I) = (pc(S,I) = cs)spc(s,i)) = cs
Loop “Remainder Section”
rs: enqueue(queue);ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);

FY2019s' = exit(s,i)
pc(s',i)) = rspc(s',j) = pc(s,j) if i jqueue(s') = deq(queue(s))

exit is called a transition functions.

i628e information processing theory

Review of lecture 1
Mutual exclusion property: there is always at most one
process in the critical section.
eq inv1(S:Sys,I:Pid,J:Pid)= (((pc(S,I) = cs) and pc(S,J) = cs) implies I = J) .
To prove ∀ ∶ Sys ∀i, j: Pid inv1 s, i, j , we need
eq inv2(S:Sys,I:Pid) = (pc(S,I) = cs implies top(queue(S)) = I) .

∀ ∶ Sys ∀i, j: Pid inv1 , , &∀ ∶ Sys ∀i: Pid inv2 , are proved bysimultaneous (structural) induction on .

12

FY2019i628e information processing theory

13

Review of lecture 1✔
open QLOCK .
ops i j : -> Sys .
red inv1(init,i,j) .
close

Base case for inv1
Induction case in which want is taken
into account for inv1

open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq (pc(s,k) = rs) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

FY2019i628e information processing theory

Review of lecture 1
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq i = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq (i = k) = false . eq j = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

14

FY2019i628e information processing theory

15

Review of lecture 1
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq (i = k) = false . eq (j = k) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

FY2019i628e information processing theory

16

CiMPA – CafeInMaude Proof Assistant:goal{
eq [inv1 :nonexec] : inv2(S:Sys,P:Pid) = true .
eq [inv11 :nonexec] : inv1(S:Sys,P:Pid,P0:Pid) = true .
:ind on (S:Sys):apply(si)…
:apply(tc):apply (rd):apply (rd)…

}FY2019i628e information processing theory

17

CiMPA – CafeInMaude Proof Assistant:apply(tc):def csb17 = :ctf {eq pc(S#Sys,P#Pid) = rs .}:apply(csb17):def csb18 = :ctf {eq P@Pid = P#Pid .}:apply(csb18):imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}:apply (rd):def csb19 = :ctf {eq P0@Pid = P#Pid .}:apply(csb19):imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}FY2019i628e information processing theory

CiMPA – CafeInMaude Proof Assistant:apply (rd):imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}:apply (rd):imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}:apply (rd):def csb20 = :ctf {eq pc(S#Sys,P#Pid) = rs .}:apply(csb20):def csb21 = :ctf {eq P@Pid = P#Pid .}:apply(csb21):imp [inv1] by {P:Pid <- P@Pid ;}:apply (rd)18

FY2019i628e information processing theory

19

CiMPA – CafeInMaude Proof Assistant:def csb22 = :ctf [queue(S#Sys) .]:apply(csb22):imp [inv1] by {P:Pid <- P@Pid ;}:apply (rd):imp [inv1] by {P:Pid <- P@Pid ;}:apply (rd):imp [inv1] by {P:Pid <- P@Pid ;}:apply (rd)

FY2019i628e information processing theory

20

CiMPA – CafeInMaude Proof Assistant:goal{
eq [inv1 :nonexec] : inv2(S:Sys,P:Pid) = true .
eq [inv11 :nonexec] : inv1(S:Sys,P:Pid,P0:Pid) = true .
:ind on (S:Sys):apply(si)}∀ ∶ Sys ∀i, j: Pid inv1 , , &∀ ∶ Sys ∀i: Pid inv2 , are proved by simultaneous(structural) induction on .

FY2019i628e information processing theory

21

CiMPA – CafeInMaude Proof Assistant
open QLOCK .
red inv1(init,P:Pid,P0:Pid) .
red inv2(init,P:Pid) .
close:apply(tc)open QLOCK .
ops P@Pid P0@Pid : -> Pid .
red inv1(init,P@Pid,P0@Pid) .
close

open QLOCK .
ops P@Pid P0@Pid : -> Pid .
red inv2(init,P@Pid) .
close:apply(rd):apply(rd)FY2019i628e information processing theory

CiMPA – CafeInMaude Proof Assistant
open QLOCK .
op S#Sys : -> Sys . ops P@Pid P0@Pid P#Pid : -> Pid .
eq [inv1 :nonexec] : inv2(S#Pid,P:Pid) = true .
eq [inv11 :nonexec] : inv1(S:Sys,P:Pid,P0:Pid) = true .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:def csb17 = :ctf {eq pc(S#Sys,P#Pid) = rs .}:apply(csb17)
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close
open QLOCK . …
eq (pc(S#Sys,P#Pid) = rs) = false .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close

22

FY2019i628e information processing theory

23

CiMPA – CafeInMaude Proof Assistant
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:def csb18 = :ctf {eq P@Pid = P#Pid .}:apply(csb18)
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs .
eq P@Pid = P#Pid .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs .
eq (P@Pid = P#Pid) = false .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close

FY2019i628e information processing theory

CiMPA – CafeInMaude Proof Assistant
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs .
eq P@Pid = P#Pid .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}open QLOCK . …
eq pc(S#Sys,P#Pid) = rs .
eq P@Pid = P#Pid .
red inv1(S#Sys,P@Pid,P0@Pid) implies
inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:apply (rd)24

FY2019i628e information processing theory

25

CiMPA – CafeInMaude Proof Assistant
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs . eq (P@Pid = P#Pid) = false .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:def csb19 = :ctf {eq P0@Pid = P#Pid .}:apply(csb19)
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs . eq (P@Pid = P#Pid) = false .
eq P0@Pid = P#Pid .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs . eq (P@Pid = P#Pid) = false .
eq (P0@Pid = P#Pid) = false .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close

FY2019i628e information processing theory

CiMPA – CafeInMaude Proof Assistant
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs . eq (P@Pid = P#Pid) = false .
eq P0@Pid = P#Pid .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}open QLOCK . …
eq pc(S#Sys,P#Pid) = rs . eq (P@Pid = P#Pid) = false .
eq P0@Pid = P#Pid .
red inv1(S#Sys,P@Pid,P0@Pid) implies
inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:apply (rd)26

FY2019i628e information processing theory

27

CiMPA – CafeInMaude Proof Assistant
open QLOCK . …
eq pc(S#Sys,P#Pid) = rs . eq (P@Pid = P#Pid) = false .
eq (P0@Pid = P#Pid) = false .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}open QLOCK . …
eq pc(S#Sys,P#Pid) = rs . eq (P@Pid = P#Pid) = false .
eq (P0@Pid = P#Pid) = false .
red inv1(S#Sys,P@Pid,P0@Pid) implies
inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:apply (rd)

FY2019i628e information processing theory

CiMPA – CafeInMaude Proof Assistant
open QLOCK . …
eq (pc(S#Sys,P#Pid) = rs) = false .
red inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}open QLOCK . …
eq (pc(S#Sys,P#Pid) = rs) = false .
red inv1(S#Sys,P@Pid,P0@Pid) implies
inv1(want(S#Sys,P#Pid),P@Pid,P0@Pid) .
close:apply (rd)28

FY2019i628e information processing theory

29

CiMPA – CafeInMaude Proof AssistantIf some commands (or tactics) in a proof script are
missing, CiMPA complains.
Therefore, CiMPA can avoid human errors.

FY2019i628e information processing theory

CiMPG – CafeInMaude Proof Generator
Input: proof score
open QLOCK .
ops i j : -> Sys .
red inv1(init,i,j) .
close

…

Output: proof script

CiMPG

open QLOCK .
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq (pc(s,k) = rs) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

…

:goal{
eq [inv1 :nonexec] : inv2(S:Sys,P:Pid) = true .
eq [inv11 :nonexec] : inv1(S:Sys,P:Pid,P0:Pid) = true . }:ind on (S:Sys):apply(si)…
:apply(tc):def csb17 = :ctf {eq pc(S#Sys,P#Pid) = rs .}:apply(csb17):def csb18 = :ctf {eq P@Pid = P#Pid .}:apply(csb18):imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}:apply (rd):def csb19 = :ctf {eq P0@Pid = P#Pid .}:apply(csb19):imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}…

30

FY2019i628e information processing theory

31

CiMPG – CafeInMaude Proof Generator
Necessary to have the directive :id(inv1) in each open‐close fragment
and one special open-close fragment that has the directive :proof(inv1).
open QLOCK .
:id(inv1)
ops i j : -> Sys .
red inv1(init,i,j) .
close…

open QLOCK .
:id(inv1)
op s : -> Sys . ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq (pc(s,k) = rs) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close…
open QLOCK .
:proof(inv1)
close

FY2019i628e information processing theory

32

CiMPG – CafeInMaude Proof Generator
Looking at all open‐close fragments in which :id(inv1) is written andone special open-close fragment in which :proof(inv1) is written,
CiMPG recognizes what to prove.
More concretely, it looks at terms to reduce except for implications:
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
red inv2(s,j) implies inv1(s,i,j) implies inv1(try(s,k),i,j) .
red inv1(s,i,k) implies inv2(s,i) implies inv2(exit(s,k),i) .
Then, it generates the following::goal{
eq [inv1 :nonexec] : inv2(S:Sys,P:Pid) = true .
eq [inv11 :nonexec] : inv1(S:Sys,P:Pid,P0:Pid) = true .
:ind on (S:Sys):apply(si)}FY2019i628e information processing theory

33

CiMPG – CafeInMaude Proof Generator
For each constructor of Sys, such as wait, and each state predicate totackle, such as inv1, it looks at all open-close fragments in which wait isconsidered.
open QLOCK .
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq (i = k) = false . eq j = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close
It looks at the equations used for case splitting.

FY2019i628e information processing theory

34

CiMPG – CafeInMaude Proof Generator
From the four open-close fragments
open QLOCK .

…

open QLOCK .

…

eq pc(s,k) = rs . eq i = k .

eq pc(s,k) = rs . eq (i = k) = false .

red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

eq j = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

open QLOCK .

…

eq pc(s,k) = rs . eq (i = k) = false .
eq (j = k) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

open QLOCK .

…

eq (pc(s,k) = rs) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

FY2019i628e information processing theory

35

CiMPG – CafeInMaude Proof Generator
it generates the following::def csb17 = :ctf {eq pc(S#Sys,P#Pid) = rs .}:apply(csb17)
From the three open-close fragments
open QLOCK . …
eq pc(s,k) = rs . eq i = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close
open QLOCK . …
eq pc(s,k) = rs . eq (i = k) = false .
eq (j = k) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

FY2019open QLOCK . …
eq pc(s,k) = rs . eq (i = k) = false .
eq j = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

i628e information processing theory

CiMPG – CafeInMaude Proof Generator
it generates the following::def csb18 = :ctf {eq P@Pid = P#Pid .}:apply(csb18)
From the one open-close fragment
open QLOCK . …
eq pc(s,k) = rs . eq i = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

because the two equations used for case splitting have been alreadygenerated

36

FY2019i628e information processing theory

37

CiMPG – CafeInMaude Proof Generator
it generates the following::imp [inv11] by {P0:Pid <- P0@Pid ; P:Pid <- P@Pid ;}From the one open-close fragment
open QLOCK . …
eq pc(s,k) = rs . eq i = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

because this open-close fragment has been already generated
it generates the following::apply (rd)

FY2019i628e information processing theory

38

CiMPG – CafeInMaude Proof Generator
If some open‐close fragments are missing, CiMPG informs users that
there are some missing open‐close fragments.

If CiMPG successfully generates a proof script from a proof score, thenthe proof score is correct because the proof script is checked by CiMPA
at the same time.

FY2019i628e information processing theory

39

CiMPG – CafeInMaude Proof Generator

Why it took much time for ABP is because associativity is used.

@

FY2019@@@i628e information processing theory

Summary and future directions
Summary
Qlock has been used as an example to describe CiMPA andCiMPG.
Publications
For CiMPA & CiMPG,
Adrián Riesco, Kazuhiro Ogata: Prove it! Inferring Formal Proof Scripts from
CafeOBJ Proof Scores. ACM Trans. Softw. Eng. Methodol. 27(2): 6:1‐6:32(2018)For CafeInMaude,
Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi: A Maude environment for
CafeOBJ. Formal Asp. Comput. 29(2): 309‐334 (2017)40

FY2019i628e information processing theory

Summary and future directions
Future directions
Extending CiMPG so that it can fix incomplete proof scores
given
Extending CiMPG so that it can construct proof scripts even
if any proof scores are not given
Integrating some human interactions into an extension of
CiMPG
Integrating (semi‐)automatic lemma conjecture mechanism
into an extension of CiMPG

41