# 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.
• processes.maude: Syntax of processes and process definitions.
• sym-semantics.maude: Definition of the symbolic semantics.
• examples.maude : Examples of use.
• ex_dining_philosophers.maude: Solution for the dinning philosophers problem
• ex_counterCCS.maude: Encoding of a counter (as in CCS)

## 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:
• The process to be executed is placed before the `@` symbol, in this case, `call('A) | call('B)`
• After the `@` symbol, we have the processes definitions of A and B: `'A =d= 'a \ 'b . call('A) & 'B =d= 'c \ 'd . call('B)`
• The 3 in the end of the line indicates that only sequences of up to 3 transitions will be generated.
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)