Symbolic Semantics for the Link Calculus

NEW: A web-based version of SiLVer (Symbolic links verifier ) is available here.

General Information

The link-calculus is a model for concurrency that extends the point-to-point communication discipline of Milner's CCS with multiparty interactions. Links are used to build chains describing how information flow among the different agents participating in a multiparty interaction. The inherent non-determinism in deciding both, the number of participants in an interaction and how they synchronize, makes difficult to devise efficient verification techniques for it. We propose a symbolic semantics for the link-calculus which is more amenable to automating reasoning. Unlike the operational semantics of the link-calculus, the symbolic semantics is finitely branching and it represents, compactly, a possibly infinite number of transitions. See [BO16] for further details.

This tool offers mechanisms to both generate traces of a given process and build the transition graph of a process (if it is finite).

Requirements

The code was implemented in Maude and tested in the version 2.7.

Files

Take a look on the header of the files for further details and examples. Download.

Examples

For further examples, please take a look on file examples.maude.

Generating Traces

First invoke the interpreter of Maude: 

maude examples.maude
The following command allows for generating traces from a given process: 

search buildTrace(call('A) | call('B) @ 'A =d= 'a \ 'b . call('A) & 'B =d= 'c \ 'd . call('B), 3) =>! T .
where: One of the solutions found by Maude is: 

< call('A) | call('B),'a \ 'b ; 'c \ 'd >

< call('A) | call('B),'c \ 'd >

< call('A) | call('B),'a \ 'b ; 'c \ 'd >

< call('A) | call('B),end >}
Each tuple (P , L) denotes that the process P can perform a transition labelled with the symbolic configuration L.

Building the LTS

The following command builds the LTS associated to a process: 

search [1] buildGraph(call('A) | call('B) @ 'A =d= 'a \ 'b . call('A) & 'B =d= 'c \ 'd . call('B) )  =>! G:GraphExec .
Again, the code before (resp. after) @ is the process (resp. process definition). The output, in this example is 

< call('A) | call('B),'a \ 'b,call('A) | call('B) >
< call('A) | call('B),'c \ 'd,call('A) | call('B) >
< call('A) | call('B),'a \ 'b ; 'c \ 'd,call('A) | call('B) >}
Each triple (P , L ,P') indicates that P can move to P' with (symbolic) action L. All the transitions are found and added to the graph (set of (P , L ,P') triples) until a fixed point is reached.

Dinning Philosophers Problem

A more compelling example is given in the file ex_dining_philosophers.maude. 

maude ex_dining_philosophers.maude
search [1] buildGraph(DPhil(2))  =>! G:GraphExec .
The output is: 

< ['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0),tau \ 'think_0,['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0),tau \ 'think_1,['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0),['u_0,'u_1]'u_0 \ 'u_1 ; 'u_1 \ tau ; tau \ 'u_0,['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('eat_0) | tau \ 'd_0 . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0),['u_0,'u_1]'u_0 \ tau ; 'u_1 \ 'u_0 ; tau \ 'u_1,['d_0,'d_1,'u_0,'u_1]call('eat_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('eat_0) | tau \ 'd_0 . call('F_0),tau \ 'eat_0,['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('release_0) | tau \ 'd_0 . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('eat_0) | tau \ 'd_0 . call('F_0),tau \ 'think_1,['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('eat_0) | tau \ 'd_0 . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('release_0) | tau \ 'd_0 . call('F_0),tau \ 'think_1,['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('release_0) | tau \ 'd_0 . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('P_1) | 'd_1 \ tau . call('F_1) | call('release_0) | tau \ 'd_0 . call('F_0),['d_0,'d_1]'d_0 \ 'd_1 ; 'd_1 \ tau ; tau \ 'd_0,['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('eat_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0),tau \ 'eat_1,['d_0,'d_1,'u_0,'u_1]call('release_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('eat_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0),tau \ 'think_0,['d_0,'d_1,'u_0,'u_1]call('eat_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('release_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0),tau \ 'think_0,['d_0,'d_1,'u_0,'u_1]call('release_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0) >
< ['d_0,'d_1,'u_0,'u_1]call('release_1) | tau \ 'd_1 . call('F_1) | call('P_0) | 'd_0 \ tau . call('F_0),['d_0,'d_1]'d_0 \ tau ; 'd_1 \ 'd_0 ; tau \ 'd_1,['d_0,'d_1,'u_0,'u_1]call('P_1) | call('F_1) | call('P_0) | call('F_0) >
That corresponds to the following LTS:

Counters

The file ex_counterCCS.maude implements the definitions of a counter as in CCS. For instance, the following code: 

search  buildTrace( (['zero , 'dec, 'inc] call('C) | tau \ 'inc . tau \ 'dec .  tau \ 'inc . tau \ 'inc .  tau \ 'dec . tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0 ) @ countDef ,20 ) =>! T:TraceCtx .
Performs the following actions: inc . dec . inc .inc .dec . dec . zero . inc . dec. zero.

The final state is ['dec,'inc,'zero]['a]['a]['a]call('C) where all the operations (inc, dec and zero) synchronized as shown by the trace 


< ['dec,'inc,'zero]call('C) | tau \ 'inc . tau \ 'dec . tau \ 'inc . tau \ 'inc . tau \ 'dec . tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['inc]'inc \ tau ; tau \ 'inc >

< ['dec,'inc,'zero](['a]call('C2) | 'a \ tau . call('C)) | tau \ 'dec . tau \ 'inc . tau \ 'inc . tau \ 'dec . tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['dec]'dec \ tau ; tau \ 'dec >

< ['dec,'inc,'zero](['a]tau \ 'a . 0 | 'a \ tau . call('C)) | tau \ 'inc . tau \ 'inc . tau \ 'dec . tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['a]'a \ tau ; tau \ 'a >

< ['dec,'inc,'zero](['a]call('C)) | tau \ 'inc . tau \ 'inc . tau \ 'dec . tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['inc]'inc \ tau ; tau \ 'inc >

< ['dec,'inc,'zero](['a]['a]call('C2) | 'a \ tau . call('C)) | tau \ 'inc . tau \ 'dec . tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['inc]'inc \ tau ; tau \ 'inc >

< ['dec,'inc,'zero](['a]['a](['b]call('C3) | 'b \ tau . call('C2)) | 'a \ tau . call('C)) | tau \ 'dec . tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['dec]'dec \ tau ; tau \ 'dec >

< ['dec,'inc,'zero](['a]['a](['b]tau \ 'b . 0 | 'b \ tau . call('C2)) | 'a \ tau . call('C)) | tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['b]'b \ tau ; tau \ 'b >

< ['dec,'inc,'zero](['a]['a](['b]call('C2)) | 'a \ tau . call('C)) | tau \ 'dec . 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['dec]'dec \ tau ; tau \ 'dec >

< ['dec,'inc,'zero](['a]['a](['b]tau \ 'a . 0) | 'a \ tau . call('C)) | 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['a]'a \ tau ; tau \ 'a >

< ['dec,'inc,'zero](['a]['a]call('C)) | 'zero \ tau . tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['zero]'zero \ tau ; tau \ 'zero >

< ['dec,'inc,'zero](['a]['a]call('C)) | tau \ 'inc . tau \ 'dec . 'zero \ tau . 0,['inc]'inc \ tau ; tau \ 'inc >

< ['dec,'inc,'zero](['a]['a]['a]call('C2) | 'a \ tau . call('C)) | tau \ 'dec . 'zero \ tau . 0,['dec]'dec \ tau ; tau \ 'dec >

< ['dec,'inc,'zero](['a]['a]['a]tau \ 'a . 0 | 'a \ tau . call('C)) | 'zero \ tau . 0,['a]'a \ tau ; tau \ 'a >

< ['dec,'inc,'zero](['a]['a]['a]call('C)) | 'zero \ tau . 0,['zero]'zero \ tau ; tau \ 'zero >

< ['dec,'inc,'zero]['a]['a]['a]call('C),end >}

References

[BO16] L. Brodo and C. Olarte. Symbolic Semantics for Multiparty Interactions in the link-calculus Submitted to SOFSEM 2016. (PDF)

For further information, please contact Carlos Olarte.