Existence Property Pattern

Untimed existence

The Existence Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found on Untimed version.

Time-constrained version

Pattern Name and Classification
Time-constrained Existence: Real-time Occurrence Specification Pattern
Structured English Specification
description …
Pattern Intent
This pattern aims at describing a portion of a system's execution bounded by a time interval that contains an instance of certain events or states.
Temporal Logic Mappings
MTL Globally: $<> \;<c \;(P)$
Before R: $!R \; W \; (P \& !R)$
After Q: $[\;](!Q) \; | <>(Q & <><c \;P))$
Between Q and R: $[\;](Q \& !R -> (!R \; W (P \& !R)))$
After Q until R: $[\;](Q \& !R -> (!R \cup (P \& !R)))$
TCTL Globally: $AF \; <c\;(P)$
Before R: $A[!R \; W \; (P \& !R)]$
After Q: $A[!Q \; W \; (Q \& AF\;<c\;(P))]$
Between Q and R: $AG(Q \& !R -> A[!R \; W \; (P \& !R)])$
After Q until R: $AG(Q \& !R -> A[!R \cup (P \& !R)])$
Example and Known Uses
description …
This pattern is the extension of the Existence pattern introduced by Dwyer in [1]. This pattern can be considered the dual of the Time-constrained Absence pattern.
Additional notes
description …

Probabilistic version

The Existence Property Pattern has been proposed by Dwyer in [2] and it can be found on Probabilistic version.

1. Matthew B. Dwyer ; George S. Avrunin ; James C. Corbett Patterns in Property Specifications for Finite-State Verification. pp. 411-420, ICSE 1999.
2. Lars Grunske Specification patterns for probabilistic quality properties. ICSE 2008: 31-40

Home page

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License