Property Pattern Mappings for RAFMC

This page describes mappings for property patterns in regular alternation-free mu-calculus (RAFMC). For other information about the patterns click on the pattern links.

These pattern mappings can be used with the EVALUATOR 3.5 model-checker of CADP.

Information about the entire pattern system is available at the Specification Patterns Home Page.


Pattern Mappings

The patterns written in RAFMC are adequate for action-based systems (the symbols P, Q, R, etc. denote action predicates). For simplicity, we assume there is no clash between action predicates, i.e., every action of the system satisfies at most one predicate P, Q, R, etc. This restriction can be removed by changing the pattern mappings appropriately.

Absence

P is false:
Globally [true*. P] false
Before R [(not R)*. P. (not R)*. R] false
After Q [(not Q)*. Q. true*. P] false
Between Q and R [true*. Q. (not R)*. P. (not R)*. R] false
After Q until R [true*. Q. (not R)*. P] false

Existence

P occurs:
Globally mu X. <true> true and [not P] X
Before R [(not P)*. R] false
After Q [(not Q)*. Q] mu X. <true> true and [not P] X
Between Q and R [true*. Q. (not (P or R))*. R] false
After Q until R [true*. Q] mu X. <true> true and [R] false and [not P] X

Bounded Existence

In these mappings we illustrate one instance of the bounded existence pattern, where the bound is at most 2 designated actions. Other bounds can be specified by variations on this mapping.
P occurs at most 2 times:
Globally [(not P)*. P. (not P)*. P. (not P)*. P] false
Before R [(not R)*. P. (not R)*. P. (not R)*. P. (not R)*. R] false
After Q [(not Q)*. Q. (not P)*. P. (not P)*. P. (not P)*. P] false
Between Q and R [true*. Q. (not R)*. P. (not R)*. P. (not R)*. P. (not R)*. R] false
After Q until R [true*. Q. (not R)*. P. (not R)*. P. (not R)*. P] false

Universality

P is true:
Globally [true*. not P] false
Before R [(not R)*. not (P or R). (not R)*. R] false
After Q [(not Q)*. Q. true*. not P] false
Between Q and R [true*. Q. (not R)*. not (P or R). (not R)*. R] false
After Q until R [true*. Q. (not R)*. not (P or R)] false

Precedence

S precedes P:
Globally [(not S)*. P] false
Before R [(not (S or R))*. P. (not R)*. R] false
After Q [(not Q)*. Q. (not S)*. P] false
Between Q and R [true*. Q. (not (S or R))*. P. (not R)*. R] false
After Q until R [true*. Q. (not (S or R))*. P] false

Response

S responds to P:
Globally [true*. P] mu X. <true> true and [not S] X
Before R [(not R)*. P. (not (S or R))*. R] false
After Q [(not Q)*. Q. true*. P] mu X. <true> true and [not S] X
Between Q and R [true*. Q. (not R)*. P. (not (S or R))*. R] false
After Q until R [true*. Q. (not R)*. P] mu X. <true> true and [R] false and [not S] X

Precedence Chain

This is the 2 cause-1 effect mapping.

S, T precede P:

Globally [(not S)*. (nil | (S. (not T)*)). P] false
Before R [(not (S or R))*. (nil | (S. (not (T or R))*)). P. (not R)*. R] false
After Q [(not Q)*. Q. (not S)*. (nil | (S. (not T)*)). P] false
Between Q and R [true*. Q. (not (S or R))*. (nil | (S. (not (T or R))*)). P.
(not R)*. R] false
After Q until R [true*. Q. (not (S or R))*. (nil | (S. (not (T or R))*)). P] false

This is the 1 cause-2 effect mapping.

P precedes S, T:

Globally [(not P)*. S. (not T)*. T] false
Before R [(not (P or R))*. S. (not (T or R))*. T. (not R)*. R] false
After Q [(not Q)*. Q. (not P)*. S. (not T)*. T] false
Between Q and R [true*. Q. (not (P or R))*. S. (not (T or R))*. T. (not R)*. R] false
After Q until R [true*. Q. (not (P or R))*. S. (not (T or R))*. T] false

Response Chain

This is the 2 stimulus-1 response mapping.

P responds to S, T:

Globally [true*. S. (not T)*. T] mu X. <true> true and [not P] X
Before R [true*. S. (not T)*. T. (not P)*. R] false
After Q [(not Q)*. Q. true*. S. (not T)*. T] mu X. <true> true and [not P] X
Between Q and R [true*. Q. (not (S or R))*. S. (not (T or R))*. T.
(not (P or R))*. R] false
After Q until R [true*. Q. (not (S or R))*. S. (not (T or R))*. T]
mu X. <true> true and [R] false and [not P] X

This is the 1 stimulus-2 response mapping.

S, T respond to P:

Globally [true*. P] mu X. <true> true and [S] mu Y. (<true> true and [not T] Y)
and [not S] X
Before R [(not R)*. P. (not (S or R))*. (nil | (S. (not (T or R))*)). R] false
After Q [(not Q)*. Q. true*. P] mu X. <true> true and
[S] mu Y. (<true> true and [not T] Y) and [not S] X
Between Q and R [true*. Q. (not R)*. P. (not (S or R))*.
(nil | (S. (not (T or R))*)). R] false
After Q until R [true*. Q. (not R)*. P] mu X. <true> true and [R] false and
[S] mu Y. (<true> true and [R] false and [not T] Y) and [not S] X

Constrained Chain Patterns

This is the 1-2 response chain constrained with a single event.

S, T without Z respond to P:

Globally [true*. P] mu X . <true> true and
[S] mu Y. (<true> true and [Z] false and [not T] Y) and [not S] X
Before R [(not R)*. P. (not (S or R))*.
(nil | (S. (nil | ((not (T or R))*. Z)). (not (T or R))*)). R] false
After Q [(not Q)*. Q. true*. P] mu X. <true> true and
[S] mu Y. (<true> true and [Z] false and [not T] Y) and [not S] X
Between Q and R [true*. Q. (not R)*. P. (not (S or R))*.
(nil | (S. (nil | ((not (T or R))*. Z)). (not (T or R))*)). R] false
After Q until R [true*. Q. (not R)*. P] mu X. <true> true and [R] false and
[S] mu Y. (<true> true and [Z or R] false and [not T] Y) and [not S] X

Author: Radu Mateescu (INRIA/VASY team). Last updated 2011/11/24 14:42:56.