Rewriting Logic Semantics of P Systems

[...home [...implementation] [...examples [...1] [...@] [...3] ] ]

Generating numbers of the form n² using the faithful implementation

  1. The description of the P system
  2. The Maude modules describing the P system
  3. Examples of rewriting
  4. Searching at non-intermediate configurations
  5. Model checking

  The description of the P system

We consider the system: Π2 = (O, μ, w1, w2, w3, (R1, ρ1), (R2, ρ2), (R3, ρ3), 1), with the following components:

The initial configuration of the system is given below:


The initial configuration of the P system

No objects are present in regions 1 and 2, hence no rule can be applied in this regions. The only possibility is to start in membrane 3, by using the single copies of objects a and f.

Using the rules a → ab and f → ff in parallel for all occurrences of a and f currently available, after n steps, n ≥ 0, we get n occurrences of b and 2 n occurrences of f. This way we always have only one copy of a. In any moment, we can use the rule a → bδ instead of a → ab. At that moment we get n+1 occurrences of b and 2n+1 occurrences of f and the membrane 3 is dissolved. This way the region 3 disappears and all the occurrences of objects from region 3 become occurrences of objects present in region 2. The rules of the membrane 3 are lost and now the rules of membrane 2 are active. Due to the priority relation, we have to use the rule ff → f as much as possible. In one step, we pass from bn+1 to d n+1, while the number of occurrences of f is halved. In the next step, each occurrence of d introduces one occurrence of e, so we get n+1 occurrences of e and n+1 occurences of d. At the same time, the number of occurrences of f is halved again. The priority relation ensures that this step must be iterated n times, each time producing n+1 occurences of e, and then, when only one copy of f will be present, the rule f → δ must be used. The membrane 2 is dissolved, the rules of region 2 are removed and the objects present here become objects of the skin region, which contains no rules. At this moment no further step is possible and so the computation stops.

Therefore, in the end we have (n+1)(n+1) copies of the object e, for some n≥ 0, present in the skin region. Hence this systems generates numbers of the form n2, for n≥ 1.


  The Maude module describing the P system

The P system has the following Maude specification: 

mod NSQUARE is
  inc PSYSTEM .

  ops r1 r2 : -> Priority .
  ops M1 M2 M3 : -> Label .
  ops a b d f e : -> Obj .

  op init : -> CConfiguration .
  eq init = { < M1 | empty ; < M2 | empty ; < M3 | a f > > > } .

  eq rules(M3) = (a -> a b), (a -> b delta), (f -> f f) .
  eq freeDeltaRules(M3) = (a -> a b), (f -> f f) .
  eq rho(M3) = empty .

  eq rules(M2) = (b -> d), (d -> d e), (r1 : f f -> f), (r2 : f -> delta) .
  eq freeDeltaRules(M2) = (b -> d), (d -> d e), (r1 : f f -> f) .
  eq rho(M2) = (r1 > r2) .

  eq rules(M1) = none .
  eq freeDeltaRules(M1) = none .
  eq rho(M1) = empty .

  eq maxSize = 15 .
endm

  Examples of rewriting

After loading the the modules PCONFIGURATION, PSYSTEM, and NSQUARE, we can use the command rew to see the intermediat configurations obtained after 25 and 45 steps of rewritings: 

Maude> rew [25] init .
rewrite [25] in NSQUARE : init .
rewrites: 310 in 10ms cpu (4ms real) (31000 rewrites/second)
result Configuration?: {< M1 | green(empty) ; < M2 | green(d) blue(M2, r1 r2, f
    f, false) > >}
Maude> rew [45] init .
rewrite [45] in NSQUARE : init .
rewrites: 791 in 10ms cpu (30ms real) (79100 rewrites/second)
result Configuration?: {< M1 | green(empty) ; < M2 | red(delta d e) > >}

  Searching configurations in the state space

The following command gives the subspace of reachable configurations (containing at most maxSize objects) starting from the initial configuration: 
Maude> search init =>+ C:Configuration .
search in NSQUARE : init =>+ C:Configuration .

Solution 1 (state 44)
states: 45  rewrites: 1443 in 20ms cpu (31ms real) (72150 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | empty ; < M3 | a b f f > > >}

Solution 2 (state 60)
states: 61  rewrites: 1511 in 30ms cpu (35ms real) (50366 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | b f f > >}

Solution 3 (state 142)
states: 143  rewrites: 5388 in 70ms cpu (114ms real) (76971 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | d f > >}

Solution 4 (state 147)
states: 148  rewrites: 5393 in 70ms cpu (116ms real) (77042 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | empty ; < M3 | a b b f f f f > > >}

Solution 5 (state 173)
states: 174  rewrites: 5556 in 70ms cpu (123ms real) (79371 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | b b f f f f > >}

Solution 6 (state 279)
states: 280  rewrites: 11877 in 120ms cpu (209ms real) (98975 rewrites/second)
C:Configuration --> {< M1 | d e >}

Solution 7 (state 309)
states: 310  rewrites: 14467 in 130ms cpu (226ms real) (111284 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | d d f f > >}

Solution 8 (state 314)
states: 315  rewrites: 14472 in 130ms cpu (227ms real) (111323 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | empty ; < M3 | a b b b f f f f f f f
    f > > >}

Solution 9 (state 340)
states: 341  rewrites: 14663 in 130ms cpu (230ms real) (112792 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | b b b f f f f f f f f > >}

Solution 10 (state 430)
states: 431  rewrites: 20338 in 150ms cpu (284ms real) (135586 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | d d f e e > >}

Solution 11 (state 562)
states: 563  rewrites: 35299 in 210ms cpu (381ms real) (168090 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | d d d f f f f > >}

Solution 12 (state 573)
states: 574  rewrites: 35535 in 220ms cpu (386ms real) (161522 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | empty ; < M3 | a b b b b f f f f f f
    f f f f f f f f f f > > >}

Solution 13 (state 583)
states: 584  rewrites: 35662 in 220ms cpu (389ms real) (162100 rewrites/second)
C:Configuration --> idle

Solution 14 (state 598)
states: 599  rewrites: 35716 in 220ms cpu (391ms real) (162345 rewrites/second)
C:Configuration --> {< M1 | d d e e e e >}

Solution 15 (state 605)
states: 606  rewrites: 36060 in 220ms cpu (395ms real) (163909 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | b b b b f f f f f f f f f f f f f f
    f f > >}

Solution 16 (state 651)
states: 652  rewrites: 41405 in 240ms cpu (444ms real) (172520 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | d d d f f e e e > >}

Solution 17 (state 681)
states: 682  rewrites: 44864 in 250ms cpu (462ms real) (179456 rewrites/second)
C:Configuration --> {< M1 | empty ; < M2 | d d d f e e e e e e > >}

Solution 18 (state 715)
states: 716  rewrites: 47389 in 270ms cpu (491ms real) (175514 rewrites/second)
C:Configuration --> {< M1 | d d d e e e e e e e e e >}

No more solutions.
states: 720  rewrites: 47479 in 270ms cpu (494ms real) (175848 rewrites/second)
However, we are interested only in the halting configurations, especially in the output membranes from the halting configurations. The command below filters the subspace of reachable committed configurations searching only the halting configurations: 
Maude> search init =>+ { < M1 | S:Soup > } .
search in NSQUARE : init =>+ {< M1 | S:Soup >} .

Solution 1 (state 279)
states: 280  rewrites: 11877 in 130ms cpu (164ms real) (91361 rewrites/second)
S:Soup --> d e

Solution 2 (state 598)
states: 599  rewrites: 35716 in 260ms cpu (344ms real) (137369 rewrites/second)
S:Soup --> d d e e e e

Solution 3 (state 715)
states: 716  rewrites: 47389 in 330ms cpu (425ms real) (143603 rewrites/second)
S:Soup --> d d d e e e e e e e e e

No more solutions.
states: 720  rewrites: 47479 in 330ms cpu (427ms real) (143875 rewrites/second)
Therefore there are only three halting configurations in the subspace considered, and they give the result for the computation of n^2 for n=1,2,3.

  Model checking

We want to check that the number of the occurences of e is the square of the number of the occurrences of b for all final states with the size less than or equal to the given value.

  Source code

We illustrate the use of LTL model checker by verifying two atomic propositions:
  1. isHalting, satisfied by a configuration if it is a committed configuration, and it consists of the skin as an elementary membrane (it must be an elementary membrane because the skin is the output membrane);
  2. isSquare, satisfied by a configuration if the number of objects e is the square of the number of objects d. 
mod N2-PREDS is
  including NSQUARE .
  including SATISFACTION .
  subsort Configuration? < State .
  ops isHalting isSquare : -> Prop .
  var C : Configuration? . 
  ceq C |= isHalting = true 
	if C :: Configuration 
	/\ { < M1 | S:Soup > } := C .

  ceq C |= isSquare = true 
	if #(C, d) * #(C, d) == #(C, e) .
endm

mod PROOF is
  including N2-PREDS .
  including MODEL-CHECKER .
  including LTL-SIMPLIFIER .
endm

  Output

We check the temporal formula [] (isHalting -> isSquare) by giving the following command: 
Maude> red modelCheck(init, [](isHalting -> isSquare)) .
reduce in PROOF : modelCheck(init, [](isHalting -> isSquare)) .
rewrites: 48374 in 310ms cpu (373ms real) (156045 rewrites/second)
result Bool: true

  A counter-example

If we slightly modify the isSquare atomic proposition: 
  ceq C |= isSquare = true
      if #(C, d) * #(C, d) == #(C, e) + 1 .
then we get a counter-example: 
Maude> red modelCheck(init, [](isHalting -> isSquare)) .
reduce in PROOF : modelCheck(init, [](isHalting -> isSquare)) .
rewrites: 821 in 10ms cpu (16ms real) (82100 rewrites/second)
result ModelCheckResult: counterexample({{< M1 | empty ; < M2 | empty ; < M3 |
    a f > > >},'1} {{blue(< M1 | empty ; < M2 | empty ; < M3 | a f > > >)},'3}
    {{< M1 | blue(M1, empty) ; blue(< M2 | empty ; < M3 | a f > >) >},'7} {{<
    M1 | green(empty) ; blue(< M2 | empty ; < M3 | a f > >) >},'3} {{< M1 |
    green(empty) ; < M2 | blue(M2, r1 r2, empty, false) ; blue(< M3 | a f >) >
    >},'9'} {{< M1 | green(empty) ; < M2 | green(empty) ; blue(< M3 | a f >) >
    >},'4} {{< M1 | green(empty) ; < M2 | green(empty) ; < M3 | blue(M3, a f,
    false) > > >},'6'} {{< M1 | green(empty) ; < M2 | green(empty) ; < M3 |
    green(delta b) blue(M3, f, true) > > >},'6'} {{< M1 | green(empty) ; < M2 |
    green(empty) ; < M3 | green(delta b f f) blue(M3, (empty).Soup, true) > >
    >},'7'} {{green(< M1 | empty ; < M2 | empty ; < M3 | delta b f f > > >)},
    unlabeled} {{pink(< M1 | empty ; < M2 | empty ; < M3 | delta b f f > > >)},
    unlabeled} {{< M1 | empty ; pink(< M2 | empty ; < M3 | delta b f f > >) >},
    unlabeled} {{< M1 | empty ; < M2 | empty ; pink(< M3 | delta b f f >) > >},
    unlabeled} {{< M1 | empty ; < M2 | b f f > >},'1} {{blue(< M1 | empty ; <
    M2 | b f f > >)},'3} {{< M1 | blue(M1, empty) ; blue(< M2 | b f f >) >},'7}
    {{< M1 | green(empty) ; blue(< M2 | b f f >) >},'4} {{< M1 | green(empty) ;
    < M2 | blue(M2, r1 r2, b f f, false) > >},'8'} {{< M1 | green(empty) ; < M2
    | green(d) blue(M2, r1 r2, f f, false) > >},'8'} {{< M1 | green(empty) ; <
    M2 | green(d f) blue(M2, r1, empty, false) > >},'9'} {{green(< M1 | empty ;
    < M2 | d f > >)},unlabeled} {{pink(< M1 | empty ; < M2 | d f > >)},
    unlabeled} {{< M1 | empty ; pink(< M2 | d f >) >},unlabeled} {{< M1 | empty
    ; < M2 | d f > >},'1} {{blue(< M1 | empty ; < M2 | d f > >)},'3} {{< M1 |
    blue(M1, empty) ; blue(< M2 | d f >) >},'7} {{< M1 | green(empty) ; blue(<
    M2 | d f >) >},'4} {{< M1 | green(empty) ; < M2 | blue(M2, r1 r2, d f,
    false) > >},'8'} {{< M1 | green(empty) ; < M2 | green(d e) blue(M2, r1 r2,
    f, false) > >},'8'} {{< M1 | green(empty) ; < M2 | green(delta d e) blue(
    M2, r1 r2, empty, true) > >},'9'} {{green(< M1 | empty ; < M2 | delta d e >
    >)},unlabeled} {{pink(< M1 | empty ; < M2 | delta d e > >)},unlabeled} {{<
    M1 | empty ; pink(< M2 | delta d e >) >},unlabeled}, {{< M1 | d e >},'1} {{
    blue(< M1 | d e >)},'4} {{< M1 | blue(M1, d e) >},'7})
Maude>
  Back to top