Property Pattern Mappings for ACTL

This page describes mappings for property patterns in ACTL (Action Computation Tree Logic). 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, whose input specification language allows to encode the operators of ACTL.

## Pattern Mappings

The patterns written in ACTL 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 AG{true} [P] false Before R AG{not R} [P] AG{not R} [R] false After Q AG{not Q} [Q] AG{true} [P] false Between Q and R AG{true} [Q] AG{not R} [P] AG{not R} [R] false After Q until R AG{true} [Q] AG{not R} [P] false

## Existence

P occurs:
 Globally A [true{true} U{P} true] Before R AG{not P} [R] false After Q AG{not Q} [Q] A [true{true} U{P} true] Between Q and R AG{true} [Q] AG{not (P or R)} [R] false After Q until R AG{true} [Q] A [true{not R} U{P} true]

## 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 AG{not P} [P] AG{not P} [P] AG{not P} [P] false Before R AG{not R} [P] AG{not R} [P] AG{not R} [P] AG{not R} [R] false After Q AG{not Q} [Q] AG{not P} [P] AG{not P} [P] AG{not P} [P] false Between Q and R AG{true} [Q] AG{not R} [P] AG{not R} [P] AG{not R} [P] AG{not R} [R] false After Q until R AG{true} [Q] AG{not R} [P] AG{not R} [P] AG{not R} [P] false

## Universality

P is true:
 Globally AG{true} [not P] false Before R AG{not R} [not (P or R)] AG{not R} [R] false After Q AG{not Q} [Q] AG{true} [not P] false Between Q and R AG{true} [Q] AG{not R} [not (P or R)] AG{not R} [R] false After Q until R AG{true} [Q] AG{not R} [not (P or R)] false

## Precedence

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

## Response

S responds to P:
 Globally AG{true} [P] A [true{true} U{S} true] Before R AG{not R} [P] AG{not (S or R)} [R] false After Q AG{not Q} [Q] AG{true} [P] A [true{true} U{S} true] Between Q and R AG{true} [Q] AG{not R} [P] AG{not (S or R)} [R] false After Q until R AG{true} [Q] AG{not R} [P] A [true{not R} U{S} true]

## Precedence Chain

This is the 2 cause-1 effect mapping.

S, T precede P:

 Globally AG{not S} ([P] false and [S] AG{not T} [P] false) Before R AG{not (S or R)} ([P] AG{not R} [R] false and [S] AG{not (T or R)} [P] AG{not R} [R] false) After Q AG{not Q} [Q] AG{not S} ([P] false and [S] AG{not T} [P] false) Between Q and R AG{true} [Q] AG{not (S or R)} ([P] AG{not R} [R] false and [S] AG{not (T or R)} [P] AG{not R} [R] false) After Q until R AG{true} [Q] AG{not (S or R)} ([P] false and [S] AG{not (T or R)} [P] false)

This is the 1 cause-2 effect mapping.

P precedes S, T:

 Globally AG{not P} [S] AG{not T} [T] false Before R AG{not (P or R)} [S] AG{not (T or R)} [T] AG{not R} [R] false After Q AG{not Q} [Q] AG{not P} [S] AG{not T} [T] false Between Q and R AG{true} [Q] AG{not (P or R)} [S] AG{not (T or R)} [T] AG{not R} [R] false After Q until R AG{true} [Q] AG{not (P or R)} [S] AG{not (T or R)} [T] false

## Response Chain

This is the 2 stimulus-1 response mapping.

P responds to S, T:

 Globally AG{true} [S] AG{not T} [T] A [true{true} U{P} true] Before R AG{true} [S] AG{not T} [T] AG{not P} [R] false After Q AG{not Q} [Q] AG{true} [S] AG{not T} [T] A [true{true} U{P} true] Between Q and R AG{true} [Q] AG{not (S or R)} [S] AG{not (T or R)} [T] AG{not (P or R)} [R] false After Q until R AG{true} [Q] AG{not (S or R)} [S] AG{not (T or R)} [T] A [true{not R} U{P} true]

This is the 1 stimulus-2 response mapping.

S, T respond to P:

 Globally AG{true} [P] A [true{true} U{S} A [true{true} U{T} true]] Before R AG{not R} [P] AG{not (S or R)} ([R] false and [S] AG{not (T or R)} [R] false) After Q AG{not Q} [Q] AG{true} [P] A [true{true} U{S} A [true{true} U{T} true]] Between Q and R AG{true} [Q] AG{not R} [P] AG{not (S or R)} ([R] false and [S] AG{not (T or R)} [R] false) After Q until R AG{true} [Q] AG{not R} [P] A [true{not R} U{S} A [true{not R} U{T} true]]

## Constrained Chain Patterns

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

S, T without Z respond to P:

 Globally AG{true} [P] A [true{true} U{S} A [true{not Z} U{T} true]] Before R AG{not R} [P] AG{not (S or R)} ([R] false and [S] (AG{not (T or R)} [R] false and AG{not (T or R)} [Z] AG{not (T or R)} [R] false)) After Q AG{not Q} [Q] AG{true} [P] A [true{true} U{S} A [true{not Z} U{T} true]] Between Q and R AG{true} [Q] AG{not R} [P] AG{not (S or R)} ([R] false and [S] (AG{not (T or R)} [R] false and AG{not (T or R)} [Z] AG{not (T or R)} [R] false)) After Q until R AG{true} [Q] AG{not R} [P] A [true{not R} U{S} A [true{not (Z or R)} U{T} true]]

Authors: Radu Mateescu and Mihaela Sighireanu (INRIA/VASY team). Last updated 2019/01/14 13:11:22.