Correct-by-Construction: Step I (HML formulas for CCS Processes)

golovach-ivan commented 5 years ago

This is issue for Step I of #835 general task.

source: golovach-ivan/Correct-by-Construction

General status

After 1 week of development

syntax ready 75%
logic ready 25% (CCS → LTS: 70%, HML checking: 0%)

Code examples for subprojects (LTS, CCS, HML)

// CM ≡ Coffee Machine
// CS ≡ Computer Scientist

LTS

1) Two different action syntaxes

import LTSLib._

val coinIn0 = ↑("coin")
val coinIn1 = "coin".↑

val coffeeOut0 = ↓("coffee")
val coffeeOut1 = "coffee".↓

2) possibility to assemble LTS manually

import LTSLib._

  val state0 = LTSState("CM", 0)
  val state1 = LTSState("CM", 1)
  val state2 = LTSState("CM", 2)
  val lts = LTS(
    ports = Set("coin", "coffee"),
    actions = Set("coin".↑, "coffee".↓),
    states = Set(state2, state1, state0),
    init = state2,
    edges = Set(
      Edge(state2, "coin".↑, state1), 
      Edge(state1, "coffee".↓, state0)))

  println(dump(lts))

>> ports:   {coin, coffee}
>> actions: {↑coin, ↓coffee}
>> start:   #CM_2
>> states:  {#CM_2, #CM_1, #CM_0}
>> edges:   
>>     (#CM_2 × ↑coin) → #CM_1
>>     (#CM_1 × ↓coffee) → #CM_0

CCS

1) Prefix and ∅ syntaxes with transformation to LTS

import LTSLib._
import CCSLib._

val CM = "coin".↑ :: "coffee".↓ :: ∅("CM")
println(dump(CM.toLTS()))

>> ports:   {coffee, coin}
>> actions: {↓coffee, ↑coin}
>> init:    #CM_2
>> states:  {#CM_0, #CM_1, #CM_2}
>> edges:   
>>     (#CM_1 × ↓coffee) → #CM_0
>>     (#CM_2 × ↑coin) → #CM_1

2) Loop/Recursion (⟲) syntax with transformation to LTS

import CCSLib._
import LTSLib._

val CM = "coin".↑ :: "coffee".↓ :: ⟲("CM")
println(dump(CM.toLTS()))

>> ports:   {coffee, coin}
>> actions: {↓coffee, ↑coin}
>> init:    #CM_1
>> states:  {#CM_0, #CM_1}
>> edges:   
>>     (#CM_0 × ↓coffee) → #CM_1
>>     (#CM_1 × ↑coin) → #CM_0

import CCSLib._
import LTSLib._

val LOOP = "coin".↑ :: "coffee".↓ :: ⟲("LOOP")
val CM = "initA".↑ :: (("initB".↑, "CM") |: LOOP)

println(dump(CM.toLTS()))

>> TBD

3) Alternative/Choise/Sum (+) syntax with transformation to LTS

import CCSLib._
import LTSLib._

val $ = "coin"
val ☕ = "coffee"
val ✉ = "pub"

val CS = ($.↓ :: ☕.↑ :: ✉.↓ :: ⟲("CS")) + (☕.↑ :: ✉.↓ :: ⟲("CS"))

println(dump(CS.toLTS()))

>> ports:   {pub, coffee, coin}
>> actions: {↓pub, ↑coffee, ↓coin}
>> init:    #CS_2
>> states:  {#CS_0, #CS_3, #CS_1, #CS_2}
>> edges:   
>>     (#CS_3 × ↓pub) → #CS_2
>>     (#CS_1 × ↑coffee) → #CS_0
>>     (#CS_2 × ↓coin) → #CS_1
>>     (#CS_0 × ↓pub) → #CS_2
>>     (#CS_2 × ↑coffee) → #CS_3

4) Parallel Composition (|) syntax with transformation to LTS

import CCSLib._
import LTSLib._

val $ = "coin"
val ☕ = "coffee"
val ✉ = "pub"

val CM = $.↑ :: ☕.↓ :: ⟲("CM")
val CS = $.↓ :: ☕.↑ :: ✉.↓ :: ⟲("CS")

println(dump((CM | CS).toLTS()))

>> ports:   {coffee, coin, pub}
>> actions: {↓pub, ↑coin, ↓coin, ↓coffee, ↑coffee}
>> init:    #(CM|CS)_5
>> states:  {#(CM|CS)_2, #(CM|CS)_5, #(CM|CS)_1, #(CM|CS)_0, #(CM|CS)_3, #(CM|CS)_4}
>> edges:   
>>     (#(CM|CS)_0 × ↓pub) → #(CM|CS)_2
>>     (#(CM|CS)_2 × ↓coin) → #(CM|CS)_1
>>     (#(CM|CS)_2 × ↓coffee) → #(CM|CS)_5
>>     (#(CM|CS)_5 × ↓coin) → #(CM|CS)_4
>>     (#(CM|CS)_1 × ↓coffee) → #(CM|CS)_4
>>     (#(CM|CS)_4 × ↑coin) → #(CM|CS)_1
>>     (#(CM|CS)_3 × ↓pub) → #(CM|CS)_5
>>     (#(CM|CS)_5 × ↑coin) → #(CM|CS)_2
>>     (#(CM|CS)_1 × ↑coffee) → #(CM|CS)_0
>>     (#(CM|CS)_4 × ↑coffee) → #(CM|CS)_3
>>     (#(CM|CS)_0 × ↓coffee) → #(CM|CS)_3
>>     (#(CM|CS)_3 × ↑coin) → #(CM|CS)_0

HML

1) Syntax for 6 productions (tt, ff, ∧, ∨, ◇, ⬜), syntax sugar (¬, Act) and recurion (↶)

import LTSLib._
import HMLLib._

val $ = "coin"
val ☕ = "coffee"

val α = ¬(¬(tt) ∧ ff)
val β = ◇($.↑){tt} ∧ ⬜($.↑){↶}
val γ = ◇($.↑, ☕.↓){tt} ∧ ⬜($.↑, ☕.↓){↶}
val δ = ◇(Act - τ){tt} ∧ ⬜(Act - ($.↑, ☕.↓)){↶}

2) Syntax for formula satisfaction (⊨)

import LTSLib._
import CCSLib._
import HMLLib._

val $ = "coin"
val ☕ = "coffee"

val CM = $.↑ :: ☕.↓ :: ∅("CM")
val φ = ◇($.↑){tt} ∧ ⬜($.↑){↶}

val hasProperty = CM ⊨ φ

golovach-ivan commented 5 years ago

Add sources Correct-by-Construction

David405 commented 5 years ago

@golovach-ivan kindly close this issue and report all updates on the task in #835, creating separates issues will make the work difficult to track, I find the objective quite interesting and would want to follow up on the task.

dckc commented 5 years ago

Thanks for the pointer to the scala source code.

@Jake-Gillberg were you aware of this work?

For reference, a nice sturdy, decentralized commit hash: : https://github.com/golovach-ivan/Correct-by-Construction/commit/c2e89d4f7ff8723842703175f6da375d585753a0 July 12.

@David405 I suggest we defer to the person doing the bulk of the work regarding how to organize it into issues. I do agree that fine-grain issues are sometimes awkward when it comes to budgeting and rewards. (IOU a pointer to specifics).

David405 commented 5 years ago

@dckc I closed this issue because I think it will be more effective to have one issue #835 in this repository that is used to give updates on each task while making pointers to a personal repository, that way, it will be far easier to keep track of the activity, don't you think so?

Also, have anyone been able to reach @golovach-ivan recently? I have tried contacting him but barely replies to his messages on discord( Personally, I would love to see more activity on the parent issue).

dckc commented 5 years ago

I think it's more important that it be easy to do the work than to track it. Giving advice is fine, but as I said: let's defer to the person doing most of the work to organize it into issues.

@golovach-ivan isn't obliged to respond quickly (or at all) on discord. For this sort of work, an update every week or two or three seems fine, to me.

dckc commented 5 years ago

@golovach-ivan Do you want to propose a budget and reward for the work you have done in July? Have you discussed it with anyone? Or do you want to wait on budget and such until you have had more chance to make more progress and discuss it with others?

golovach-ivan commented 5 years ago

Week 2 commit done

LTS (syntax and syntax processing)

1) Add type aliases

type ⌾ = LTSState
type ⒜ = LTSAction
type ➝ = Edge

2) Implicit Symbol -> LTSState conversion

val s0: ⌾ = 's0

3) Checking are there annihilated actions

val a_in = "a".↑
val a_out  = "a".↓
println(a_in ⇅ a_out)

>> true

4) Edge syntax

val e0 = Edge('s0, τ, 's1) // standard syntax
val e1 = 's0 × τ ➝ 's1    // syntax sugar

5) LTS definition

import LTSLib._ 

val $ = "$"
val ☕ = "☕"

val lts = LTS(
  ports = ($, ☕),
  actions = (↑($), ↓(☕)),
  states = ('s0, 's1),
  init = 's0,
  edges = Set(
    's0 × ↑($) ➝ 's1,
    's1 × ↓(☕) ➝ 's0
  ))

6) Weak/Strong Bisimulation syntax and Algorithm

import LTSLib._
import CCSLib._
import BisimulationLib._

val ltsA = toLTS("A".↑ :: "B".↓ :: ⟲)
val ltsB = toLTS("A".↑ :: "B".↓ :: "A".↑ :: "B".↓ :: ⟲)

println(ltsA ~ ltsB)
println(ltsA ≈ ltsB)

Partially implemented Kanellakis and Smolka algorithm (paper, code).

CCS (syntax and syntax processing finished )

7) Added Restriction (\) syntax and processing

import LTSLib._
import CCSLib._

val CM = ("$".↑ :: "☕".↓ :: ⟲) \ "$"
println(dump(toLTS(CM)))

>> ports:   {☕}
>> actions: {↓☕}
>> states:  {'s0, 's1}
>> init:    's1
>> edges:   
>>     's0 × ↓☕ → 's1

Or

val CM = ("$".↑ :: "☕".↓ :: ⟲) \ "$" \ "✉"

Or

val CM = ("$".↑ :: "☕".↓ :: ⟲) \ ("$", "✉")

8) Added Rename (∘) syntax and processing

import LTSLib._
import CCSLib._

val CM = ("$".↑ :: "☕".↓ :: ⟲) ∘ ("$" -> "A")
println(dump(toLTS(CM)))

>> ports:   {☕, A}
>> actions: {↓☕, ↑A}
>> states:  {'s0, 's1}
>> init:    's1
>> edges:   
>>     's0 × ↓☕ → 's1
>>     's1 × ↑A → 's0

Or

val CM = ("$".↑ :: "☕".↓ :: ⟲) ∘ ("$" -> "A", "☕" -> "B")

9) Added silent τ-action generation to Parallel Composition (|)**

import LTSLib._
import CCSLib._

val A_IN  = "A".↑ :: ⟲
val A_OUT = "A".↓ :: ⟲

println(dump(toLTS(A_IN | A_OUT)))

>> ports:   {A}
>> actions: {↑A, ↓A, τ}
>> states:  {'s0}
>> init:    's0
>> edges:   
>>     's0 × ↑A → 's0
>>     's0 × ↓A → 's0
>>     's0 × τ → 's0

10) Documentation**

github.com/Correct-by-Construction/README 400 lines

allancto commented 5 years ago

@dckc @David405 can you vote this in the Development label? Status: #836 = 30 story points = 4500$ done 2/3 = 20 story points = 3000$. Let me know if any questions. Thanks! -@allancto

dckc commented 5 years ago

I'm standing by to hear from @golovach-ivan on a budget / reward proposal. Perhaps I could / should have done more to be sure you understand how the process works... I count on ISSUE_TEMPLATE to give instructions, but I see you deleted those without filling in the budget blanks...

@allancto I don't think this issue is 2/3rds of #836, but one could argue that #836 is more than 30 story points, so I'm open to a range of budgets.

golovach-ivan commented 5 years ago

Implement strong/weak bisimulations for CCS/LTS (syntax and algorithm: Kanellakis and Smolka 1983/1990).

Strong / Weak Bisimulation

CCS Bisimulation syntax

import net.golovach.verification.LTSLib._
import net.golovach.verification.ccs.BisimulationLib._
import net.golovach.verification.ccs.CCSLib._

val A = "a".↓

val x = A :: ∅
val y = (A :: ∅) + (A :: ∅)

val isStrongBisimilar:    Boolean = x ~ y
val isNotStrongBisimilar: Boolean = x ≁ y
val isWeakBisimilar:      Boolean = x ≈ y
val isNotWeakBisimilar:   Boolean = x ≉ y

LTS Bisimulation syntax

import net.golovach.verification.LTSLib._
import net.golovach.verification.ccs.BisimulationLib._
import net.golovach.verification.ccs.CCSLib._

val A = "a".↓

val x = (A :: ∅).asLTS
val y = ((A :: ∅) + (A :: ∅)).asLTS

val isStrongBisimilar:    Boolean = x ~ y
val isNotStrongBisimilar: Boolean = x ≁ y
val isWeakBisimilar:      Boolean = x ≈ y
val isNotWeakBisimilar:   Boolean = x ≉ y

Example: University

Source code:

// CM ≡ Cofee Machine
// CSh ≡ Computer Scientist (honest)
// CSr ≡ Computer Scientist (real)
// Univ ≡ University (implementation)
// Spec ≡ Specification

// === impl
val CM = ↑($) :: ↓(☕) :: ⟲
val CSh = ↓($) :: ↑(☕) :: ↓(✉) :: ⟲
val CSr = (↓($) :: ↑(☕) :: ↓(✉) :: ⟲) + (↑(☕) :: ↓(✉) :: ⟲)
val Univ = (CSh | CM | CSr) \ ($, ☕)

// === spec
val Spec = ↓(✉) :: ⟲

println(Univ ~ Spec)
println(Univ ≈ Spec)

CONSOLE

``` >> false >> true ```

Strong Bisimulation algorithm

The algorithms for computing bisimilarity due to Kanellakis and Smolka, (without Paige and Tarjan optimizations), compute successive refinements of an initial partition π-init and converge to the largest strong bisimulation over the input finite labelled transition system. Algorithms that compute strong bisimilarity in this fashion are often called partition-refinement algorithms and reduce the problem of computing bisimilarity to that of solving the so-called relational coarsest partitioning problem.

The basic idea underlying the algorithm by Kanellakis and Smolka is to iterate the splitting of some block Bi by some block Bj with respect to some action a until no further refinement of the current partition is possible. The resulting partition is often called the coarsest stable partition and coincides with strong bisimilarity over the input labelled transition system when the initial partition π-init is chosen to be Proc.

Weak Bisimulation algorithm

The problem of checking weak bisimilarity (observational equivalence) over finite labelled transition systems can be reduced to that of checking strong bisimilarity using a technique called saturation.

dckc commented 5 years ago

Are you working with anyone on this stuff? Is anyone else reviewing it or following along?

On Fri, Sep 7, 2018, 9:17 AM golovach-ivan notifications@github.com wrote:

Implement strong/weak bisimulations for CCS/LTS (syntax and algorithm: Kanellakis and Smolka 1983/1990). Strong / Weak Bisimulation CCS Bisimulation syntax

import net.golovach.verification.LTSLib._import net.golovach.verification.ccs.BisimulationLib.import net.golovach.verification.ccs.CCSLib. val A = "a".↓ val x = A :: ∅val y = (A :: ∅) + (A :: ∅) val isStrongBisimilar: Boolean = x ~ yval isNotStrongBisimilar: Boolean = x ≁ yval isWeakBisimilar: Boolean = x ≈ yval isNotWeakBisimilar: Boolean = x ≉ y

LTS Bisimulation syntax

import net.golovach.verification.LTSLib._import net.golovach.verification.ccs.BisimulationLib.import net.golovach.verification.ccs.CCSLib. val A = "a".↓ val x = (A :: ∅).asLTSval y = ((A :: ∅) + (A :: ∅)).asLTS val isStrongBisimilar: Boolean = x ~ yval isNotStrongBisimilar: Boolean = x ≁ yval isWeakBisimilar: Boolean = x ≈ yval isNotWeakBisimilar: Boolean = x ≉ y

Example: University

Source code https://github.com/golovach-ivan/Correct-by-Construction/blob/master/src/test/scala/net/golovach/verification/ccs/BisimulationDemo0_university.scala :

// CM ≡ Cofee Machine// CSh ≡ Computer Scientist (honest)// CSr ≡ Computer Scientist (real)// Univ ≡ University (implementation)// Spec ≡ Specification // === implval CM = ↑($) :: ↓(☕) :: ⟲val CSh = ↓($) :: ↑(☕) :: ↓(✉) :: ⟲val CSr = (↓($) :: ↑(☕) :: ↓(✉) :: ⟲) + (↑(☕) :: ↓(✉) :: ⟲)val Univ = (CSh | CM | CSr) \ ($, ☕) // === specval Spec = ↓(✉) :: ⟲

println(Univ ~ Spec) println(Univ ≈ Spec)

CONSOLE

false true

Strong Bisimulation algorithm

The algorithms for computing bisimilarity due to Kanellakis and Smolka, (without Paige and Tarjan optimizations), compute successive refinements of an initial partition π-init and converge to the largest strong bisimulation over the input finite labelled transition system. Algorithms that compute strong bisimilarity in this fashion are often called partition-refinement algorithms and reduce the problem of computing bisimilarity to that of solving the so-called relational coarsest partitioning problem.

The basic idea underlying the algorithm by Kanellakis and Smolka is to iterate the splitting of some block Bi by some block Bj with respect to some action a until no further refinement of the current partition is possible. The resulting partition is often called the coarsest stable partition and coincides with strong bisimilarity over the input labelled transition system when the initial partition π-init is chosen to be Proc.

Kanellakis, Smolka, 1983/1990, "CCS expressions, finite state processes, and three problems of equivalence" https://www.sciencedirect.com/science/article/pii/089054019090025D

Robert Paige and Robert E. Tarjan, 1987, "Three Partition Refinement Algorithms" https://epubs.siam.org/doi/pdf/10.1137/0216062

Weak Bisimulation algorithm

The problem of checking weak bisimilarity (observational equivalence) over finite labelled transition systems can be reduced to that of checking strong bisimilarity using a technique called saturation.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/rchain/bounties/issues/836#issuecomment-419453819, or mute the thread https://github.com/notifications/unsubscribe-auth/AAJNyqYz3xim-GgMey5hmJ8Cj9Y0FUAGks5uYoAXgaJpZM4VNh5w .

golovach-ivan commented 5 years ago

There is no reviewer who would understand both scala and the calculation of processes and was interested. Now only I do this topic: Formal Verification for Rho-Calculi. Allanc interested. In Sep i want show results to Greg.

allancto commented 5 years ago

@dckc I reviewed at @golovach-ivan 's request. I would like confirmation from @Jake-Gillberg @JoshOrndorff @jbassiri @David405 @ddayan , yourself or anyone else who feels competent to speak to this issue.

Thanks all! -@allancto

dckc commented 5 years ago

Collaboration is pretty important... Nearly essential.

I'm not up to speed enough to read the code as it is without more documentation.

I mentioned this work to Mike Stay and he showed some interest.

I don't see any budget votes from you... Is that on purpose?

On Sat, Sep 8, 2018, 1:48 PM golovach-ivan notifications@github.com wrote:

There is no reviewer who would understand both scala and the calculation of processes and was interested. Now only I do this topic: Formal Verification for Rho-Calculi. Allanc interested. In Sep i want show results to Greg.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/rchain/bounties/issues/836#issuecomment-419664914, or mute the thread https://github.com/notifications/unsubscribe-auth/AAJNyrxmLwJftwBSITVQ5AOduMORXwbhks5uZBERgaJpZM4VNh5w .

David405 commented 5 years ago

@golovach-ivan perhaps it might be useful for you to do a code walkthrough or some sort of readme file to enable interested participants to catch up with you. Sometimes, it is difficult to get in touch with you.

David405 commented 5 years ago

I am about to vote on this but do not follow well enough to make an informed decision on the budget.

allancto commented 5 years ago

@dckc as I understand this issue has spanned two months and in August what Ivan did was weak/strong bisimilarity (10 functional point = 1500$).

@golovach-ivan @David405 and @dckc are correct, you should please communicate so that others may benefit. A typical way to communicate would be to offer a half hour or hour zoom in your "zoom room" or one sponsored by Colab. You may also consider holding a weekly "office hours", I can say personally that I've benefitted from all communications I've had with you and I believe the same will be true for anyone who attends your talks or walkthroughs.

Thanks @golovach-ivan for your contribution(s)! -@allancto

JoshOrndorff commented 5 years ago

@golovach-ivan This project looks super cool. I would like to see a tour or learn an overview. I understand process calculi and coding well enough that I could likely be of value. Please post when might be a good time.

dckc commented 5 years ago

On Sat, Sep 8, 2018, 4:51 PM allancto notifications@github.com wrote:

@dckc https://github.com/dckc as I understand this issue has spanned two months and in August what Ivan did was weak/strong bisimilarity (10 functional point = 1500$).

Bisimiarity between what and what?

10 story points would indicate significant end-user functionality. Tell me a story about how somebody makes use of this feature?

dckc commented 5 years ago

Taking another look, I do see stories in the docs... about a coffee machine and such. But the notation is too dense for me. How would one read these, in prose?

// === impl
val CM = ↑($) :: ↓(☕) :: ⟲
val CSh = ↓($) :: ↑(☕) :: ↓(✉) :: ⟲
val CSr = (↓($) :: ↑(☕) :: ↓(✉) :: ⟲) + (↑(☕) :: ↓(✉) :: ⟲)
val Univ = (CSh | CM | CSr) \ ($, ☕)

// === spec
val Spec = ↓(✉) :: ⟲

dckc commented 5 years ago

Reviewing the plan in #835, I see a big part of why I couldn't read the notation: it's not intended to be rho-calculus. Part 1 is just CCS.

@golovach-ivan in the coming weeks, please do find time to chat with @JoshOrndorff , @Jake-Gillberg , @pyrocto and/or others about helping them understand the documentation or perhaps refine it to the point where more people can understand it.

rchain / bounties