py‚wevse„syx exh †i‚spsge„syx yp €‚y€i‚„‰ ƒ€igspsge„syx
€e„„i‚xƒ
˜y
hmitriy fryndin

e „riƒsƒ
ƒu˜mitted
to wi™hig—n ƒt—te …niversity
in p—rti—l ful(llment of the requirements
for the degree of
weƒ„i‚ yp ƒgsixgi
gyw€…„i‚ ƒgsixgi
PHIH

ABSTRACT

py‚wevse„syx exh †i‚spsge„syx yp €‚y€i‚„‰ ƒ€igspsge„syx
€e„„i‚xƒ
˜y
hmitriy fryndin
piniteEst—te veri(™—tion @pƒ†A te™hniques —re intended for proving properties of softw—re
systemsF elthough signi(™—nt progress h—s ˜een m—de in the l—st de™—de —utom—ting pƒ†
te™hniquesD the —doption of these te™hniques ˜y softw—re developers is lowF „he ƒpe™i(™—tion
€—ttern ƒystem @ƒ€ƒA is intended to —ssist users in ™re—ting su™h spe™i(™—tionsF st identi(es
™ommon spe™i(™—tion p—tterns —nd indi™—tes how to tr—nsl—te the p—tterns into — v—riety of
di'erent spe™i(™—tion l—ngu—gesF roweverD the p—tterns in the ƒ€ƒ —re de(ned inform—lly
—nd their tr—nsl—tions —re not veri(edF „his work dis™usses the inform—l n—ture of these
de(nitionsD proposes — form—liz—tion for them —nd provides form—l proofs for the tr—nsl—tion
of p—tterns to vine—r „empor—l vogi™F

ACKNOWLEDGEMENTS

s w—nt to th—nk my ™ommittee mem˜ersX hrF v—ur— hillonD hrF iri™ „orng —nd hrF ‡illi—m
pF €un™hF „his thesis ™ould not h—ve ˜een written without their supportF s re—lly —ppre™i—te
their timeF ispe™i—llyD s w—nt to th—nk v—urie hillon for ˜eing p—tient —nd guiding me —ll
these ye—rsF

iii

TABLE OF CONTENTS

LIST OF TABLES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
LIST OF FIGURES

vi

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vii

CHAPTER 1 INTRODUCTION

. . . . . . . . . . . . . . . . . . . . . . . . . . .

1

ƒpe™i(™—tion €—ttern ƒystem F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F
vine—r „empor—l vogi™ F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F
ƒtru™ture of this work F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F

I
P
R

CHAPTER 2 INFORMAL DEFINITIONS . . . . . . . . . . . . . . . . . . . . .

5

IFI
IFP
IFQ
PFI
PFP
PFQ

snform—l he(nitions of €—tterns F F F F F F F F F F F F F F F F F F F F
snform—l he(nitions of ƒ™opes F F F F F F F F F F F F F F F F F F F F F
€ro˜lems with the snterpret—tion F F F F F F F F F F F F F F F F F F F
PFQFI wultiple delimiters in fefore —nd efter s™opes F F F F F
PFQFP wultiple delimiters in fetween —nd efterE…ntil s™opes
PFQFQ impty interv—ls F F F F F F F F F F F F F F F F F F F F F F F F F

F
F
F
F
F
F

F
F
F
F
F
F

F
F
F
F
F
F

F
F
F
F
F
F

F
F
F
F
F
F

F
F
F
F
F
F

F
F
F
F
F
F

F S
F S
F U
F V
F W
F IH

CHAPTER 3 PROPOSED FORMALIZATION . . . . . . . . . . . . . . . . . .

QFI
QFP
QFQ
QFR

porm—l he(nitions of ƒtrong ƒ™opes
porm—l he(nitions of ‡e—k ƒ™opes F
porm—l he(nitions of €—tterns F F F F
€—ttern w—ppings for v„v F F F F F F

F
F
F
F

F
F
F
F

F
F
F
F

F
F
F
F

F
F
F
F

F
F
F
F

IP
IQ
IR
IT

CHAPTER 4 RELATED WORK . . . . . . . . . . . . . . . . . . . . . . . . . . .

20

CHAPTER 5 CONCLUSIONS . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21

APPENDIX A ORIGINAL LTL FORMULAS . . . . . . . . . . . . . . . . . . .

23

APPENDIX B

. . . . . . . . . . . . . . . . . .

25

F
F
F
F
F
F
F
F
F
F
F

PT
PT
PT
PU
PV
PW
QI
QI
QI
QP
QQ

fFHFI e˜sen™e F F F F F F F F F F F F F
fFHFIFI qlo˜—lly F F F F F F F
fFHFIFP fefore R F F F F F F F
fFHFIFQ efter Q F F F F F F F
fFHFIFR fetween Q —nd R F
fFHFIFS efter Q until R F F F
fFHFP ixisten™e with ƒtrong ƒ™opes
fFHFPFI qlo˜—lly F F F F F F F
fFHFPFP fefore R F F F F F F F
fFHFPFQ efter Q F F F F F F F
fFHFPFR fetween Q —nd R F

iv

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F

12

F
F
F
F

PROOFS OF EQUIVALENCE

F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F

fFHFQ

fFHFR
fFHFS

fFHFT

fFHFU
fFHFV
fFHFW
fFHFIH

fFHFPFS efter Q until R F F F F F F F F F F
ƒtrong ixisten™e with ƒtrong ƒ™opes F F
fFHFQFI qlo˜—lly F F F F F F F F F F F F F F
fFHFQFP fefore R F F F F F F F F F F F F F F
fFHFQFQ efter Q F F F F F F F F F F F F F F
fFHFQFR fetween Q —nd R F F F F F F F F
fFHFQFS efter Q until R F F F F F F F F F F
…nivers—lity F F F F F F F F F F F F F F F F F F
ixisten™e with ‡e—k ƒ™opesD SW F F F F F
fFHFSFI @fefore RAW F F F F F F F F F F F
fFHFSFP @fetween Q —nd RAW F F F F F F
fFHFSFQ @efter Q until RAW F F F F F F F
ƒtrong ixisten™e with ‡e—k ƒ™opesD SW
fFHFTFI @fefore RAW F F F F F F F F F F F
fFHFTFP @fetween Q —nd RAW F F F F F F
fFHFTFQ @efter Q until RAW F F F F F F F
€re™eden™e F F F F F F F F F F F F F F F F F F
qlo˜—lly F F F F F F F F F F F F F F F F F F F F
‚esponse F F F F F F F F F F F F F F F F F F F
qlo˜—lly F F F F F F F F F F F F F F F F F F F F

APPENDIX C

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

PROOFS OF NON EQUIVALENCE

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F
F

QR
QT
QT
QU
QV
QV
QW
RH
RH
RH
RI
RP
RQ
RQ
RQ
RR
RR
RR
RS
RS

. . . . . . . . . . . . . .

46

gFI ixisten™e F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F RT
gFP ƒtrong ixisten™e F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F RT
BIBLIOGRAPHY

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

v

49

LIST OF TABLES

IFI

v„vD puture „empor—l yper—torsF F F F F F F F F F F F F F F F F F F F F F F F F F F F F F

Q

QFI

€roposed v„v formul—s vsF origin—l formul—s ˜y wFhwyer et —lF F F F F F F F F F F F IV

QFP

€roposed v„v formul—s for ‡e—k —nd ƒtrong s™opesF fold formul—s —re equiv—lent
to origin—l formul—s of wFhwyer et —lF F F F F F F F F F F F F F F F F F F F F F F F F F F IW

eFI v„v formul—s presented in ‘I“ F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F PR

vi

LIST OF FIGURES

PFI

gl—ssi(™—tion of p—tterns in terms of system ˜eh—viorsD —s it —ppe—rs in ‘I“ F F F F

S

PFP

gl—ssi(™—tion of p—tternsD —s it —ppe—rs in ‘I“ F F F F F F F F F F F F F F F F F F F F F F

S

PFQ

sntent of o™™urren™e p—tternsD —s it —ppe—rs in ‘I“ F F F F F F F F F F F F F F F F F F F F

T

PFR

sntent of order p—tternsD —s it —ppe—rs in ‘I“ F F F F F F F F F F F F F F F F F F F F F F F

T

PFS

„he illustr—tion of s™opesD —s it —ppe—rs in ‘I“ F F F F F F F F F F F F F F F F F F F F F F

U

PFT

„he de(nitions of s™opesD —s they —ppe—r in ‘I“ F F F F F F F F F F F F F F F F F F F F F

U

PFU

€ossi˜le interpret—tions of fetween Q —nd R s™opesF F F F F F F F F F F F F F F F F F

W

vii

Chapter 1
INTRODUCTION

€roperty spe™i(™—tions —re intended to ˜e used in softw—re development to des™ri˜e di'erent
p—rts of — system ˜eh—viorF „hey ™—n help to dete™t design )—ws in e—rly st—ges of developE
mentD serve —s — referen™e for progr—mmers in l—ter st—ges of softw—re developmentD —nd ˜e
used for the veri(™—tion of —n implement—tionF feing developed ˜y hum—nsD the initi—l spe™iE
(™—tions —re never form—l ‘IP“F hevelopers usu—lly represent initi—l spe™i(™—tions gr—phi™—lly
or using the n—tur—l l—ngu—ge ‘IQ“F €roperty spe™i(™—tions often st—y in this form for the
rest of the development pro™essF ‡hile still usefulD these inform—l spe™i(™—tions —re often
—m˜iguous —nd in™onsistent with the —™tu—l system9s ˜eh—vior —nd the ™ost of the rel—ted
errors is highD —s they —re usu—lly dete™ted on the l—ter st—ges of developmentF
‡hen property spe™i(™—tions —re form—lizedD developers o˜t—in pre™ise spe™i(™—tionsD
whi™h ™—n ˜e form—lly —n—lyzed for ™onsisten™yD ™ompletenessD —nd other desir—˜le @or —˜sen™e
of undesir—˜leA propertiesF „ools —utom—ting su™h —n—lysis typi™—lly require some spe™i—l
types of form—lismsD su™h —s tempor—l logi™ ‘R“F „he use of these form—lisms requires expertise
—nd signi(™—ntly limits —doption of pƒ† te™hniques ˜y the developersF

1.1 Specication Pattern System
wFhwyer et —lF in ‘TD U“ proposed —n —ppro—™h th—t helps developers in m—pping inform—l
property spe™i(™—tions to the form—lisms —™™epted ˜y — v—riety of —utom—ted veri(™—tion
toolsF ƒimil—rly to the ide— of hesign €—tterns ‘W“D wFhwyer et —lF ™—me up with — set
of p—r—meterized p—tterns th—t —re independent of the form—lisms used in the veri(™—tion
toolsF „hese p—tterns were o˜t—ined from — survey of ™ommonly o™™urring properties th—t
users verify with the (niteEst—te veri(™—tion toolsD su™h —s ƒ€sx ‘II“D ƒw† ‘IT“D g‡fExgD
sxge ‘S“ —nd pve†i‚ƒ ‘V“F
I

piniteEst—te veri(™—tion tools model — system exe™ution ˜y — @possi˜ly event drivenA
(niteEst—te m—™hineF e property p—ttern restri™ts some —spe™t of system ˜eh—viorD n—mely
the o™™urren™e of some st—teGevent or the order in whi™h multiple st—teGevents o™™ur in the
exe™utionF por ex—mpleD to s—y th—t — de—dlo™k never o™™ursD we use the e˜sen™e p—tternD or
to s—y th—t — thre—d h—s to eventu—lly rele—se memory th—t h—s ˜een dyn—mi™—lly —llo™—ted
to itD we use the ‚esponse p—tternF „hese p—tterns —re des™ri˜ed in gre—ter det—ils in
ƒe™tion PFIF
i—™h p—ttern is —sso™i—ted with — s™ope th—t des™ri˜es — sequen™e of st—tesGevents over
whi™h the restri™tions imposed ˜y the p—ttern —pplyF e s™ope ™—n de(ne the entire exe™ution
of — systemD — p—rt ˜etween the moment when — thre—d is ™re—ted —nd the moment when it
is termin—tedD et™F ƒ™opes —re des™ri˜ed in ƒe™tion PFPF
„he ™ru™i—l p—rt of the work done ˜y wFhwyer et —lF in ‘I“ is — tr—nsl—tion of p—irs
of p—tterns —nd s™opes to the following spe™i(™—tion form—lismsD whi™h —re used ˜y di'erE
ent veri(™—tion toolsX vine—r „empor—l vogi™ ‘IR“D gomput—tion „ree vogi™ ‘Q“D u—nti(ed
‚egul—r ixpressions ‘IW“ —nd sxge ueries ‘S“F yther rese—r™hers h—ve developed m—pE
pings forX e™tion gomput—tion „ree vogi™ ‘IV“D qr—phi™—l snterv—l vogi™ ‘PH“ —nd ‚egul—r
eltern—tionEpree wuEg—l™ulus ‘IS“F

1.2 Linear Temporal Logic
vine—r „empor—l vogi™ @v„vA ‘IR“ is ™ommonly used in softw—re veri(™—tion to spe™ify —nd
re—son —˜out ˜eh—viors th—t —re modeled —s line—r st—te sequen™esD with st—tes denoting
(nite sets of propositions @the propositions th—t —re trueAF „here —re sever—l model ™he™kers
—v—il—˜le th—t support v„vX ƒ€sx ‘II“D t—v— €—thpinder ‘PR“D xuƒw† ‘P“ —nd othersF
henote — set of —tomi™ propositions ˜y AF e state gives —n interpret—tion to propositions
in AF e state formula is — formul— in ordin—ry (rstEorder logi™ over the propositions in AF ‡e
use s ⊫ P to s—y th—t P holds on S or th—t s is — P Est—teF v„v extends ordin—ry predi™—te
logi™ with — set of tempor—l oper—tors presented in „—˜le IFIF
P

◻P
P
P UQ
P WQ
P

ren™eforth P
iventu—lly P
P …ntil Q
P ‡—itingEfor Q
xext P

„—˜le IFIX v„vD puture „empor—l yper—torsF
en LTL formula is de(ned —s
ˆ e—™h proposition in A is —n v„v formul—
ˆ if P —nd Q —re v„v formul—sD ¬P D P ∧ QD P ∨ QD P → QD P ↔ QD ◻P D

P WQD

P D P UQD

P —re —lso v„v formul—sF

sn v„v formul—s we use → to denote impli™—tion —nd ↔ to denote equiv—len™eD using the
more ™ommon

⇒ —nd ⇐⇒ —s met— not—tionF

v„v formul—s —re interpreted over — modelD whi™h is —n in(nite sequen™e of st—tesD

σ

s0 , s1 , . . .F ‡e write (σ, i) ⊧ P to s—y th—t P holds —t — position i ≥ 0 in σ D for —

given model σ —nd —n v„v formul— P F por — st—te formul— P D (σ, i) ⊧ P ⇐⇒ si ⊫ P F
por the v„v formul—s P —nd QX
ˆ (σ, i) ⊧ ¬P ⇐⇒ ¬(σ, i) ⊧ P F
ˆ (σ, i) ⊧ P ∨ Q ⇐⇒ (σ, i) ⊧ P ∨ (σ, i) ⊧ QD with ∧, → —nd ↔ de(ned simil—rlyF
ˆ (σ, i) ⊧ ◻P ⇐⇒ ∀k ≥ i (σ, k) ⊧ P F
ˆ (σ, i) ⊧

P ⇐⇒ ∃k ≥ i (σ, k) ⊧ P F

ˆ (σ, i) ⊧ P UQ ⇐⇒ ∃k ≥ i ((σ, k) ⊧ Q ∧ ∀j i ≤ j < k (σ, j) ⊧ P )F
ˆ (σ, i) ⊧ P WQ ⇐⇒ (σ, i) ⊧ P UQ ∨ (σ, i) ⊧ ◻P F
ˆ (σ, i) ⊧

P ⇐⇒ (σ, i + 1) ⊧ P F

Q

1.3 Structure of this work
sn this work we ™he™k for in™onsisten™ies ˜etween the inform—l de(nitions of p—tterns —nd
s™opes in the ƒpe™i(™—tion €—ttern ƒystem proposed in ‘TD U“ —nd their tr—nsl—tions to v„vD
presented in ‘I“F ‡e give — form—l interpret—tion for these de(nitionsD removing —ll in™onE
sisten™ies —nd —m˜iguitiesF pin—llyD the l—rgest p—rt of this work provides proofs of the
equiv—len™e ˜etween the p—tternGs™ope ™om˜in—tions —nd their tr—nsl—tions to v„vF fe™—use
this work only ™onsiders the tr—nsl—tion to v„vD we ™onsider only the st—teE˜—sed de(nitions
presented in ‘I“F
gh—pter P provides the de(nitions of p—tterns —nd s™opesD —s they —re given in ‘TD U“ —nd
highlights sever—l pro˜lems rel—ted to the inform—l n—ture of these de(nitionsF
sn gh—pter QD we form—lize the origin—l inform—l de(nitions of s™opes —nd p—tterns —nd
dis™uss their tr—nsl—tions to v„vF
eppendix e is the referen™e for the origin—l v„v formul—s in ‘I“F
eppendix f ™ont—ins —ll proofs for the tr—nsl—tions to v„vF
eppendix g provides ™ounterex—mples for the ™—ses when our proposed v„v formul—s —re
not equiv—lent to the origin—l formul—s in ‘I“F

R

Chapter 2
INFORMAL DEFINITIONS

2.1 Informal Denitions of Patterns
pigure PFI illustr—tes the hier—r™hy of p—tternsF pigure PFP provides the expl—n—tions for
the two m—jor groups of p—tternsD ™l—ssi(ed ˜y the system ˜eh—viorsF pigures PFQ —nd PFR
des™ri˜e the intent of —ll p—tternsF „he ™ontents of —ll (gures —re reprodu™ed from ‘I“F
Property Patterns

Occurrence

Absence

Order

Bounded
Existence

Universality

Precedence

Existence

Response

Chain
Precedence

Chain
Response

pigure PFIX gl—ssi(™—tion of p—tterns in terms of system ˜eh—viorsD —s it —ppe—rs in ‘I“

Occurrence

™utionF

€—tterns t—lk —˜out the o™™urren™e of — given eventGst—te during system exeE

Order Patterns

system exe™utionF

t—lk —˜out rel—tive order in whi™h multiple eventsGst—tes o™™ur during

pigure PFPX gl—ssi(™—tion of p—tternsD —s it —ppe—rs in ‘I“

2.2 Informal Denitions of Scopes
pigure PFS illustr—tes the de(nitions of s™opesD provided in pigure PFTF „he ™ontent of ˜oth
(gures is reprodu™ed ex—™tly —s in ‘I“F

S

Absence

„o des™ri˜e — portion of — system9s exe™ution th—t is free of ™ert—in events or st—tesF elso
known —s xeverF
Universality

„o des™ri˜e — portion of — system9s exe™ution whi™h ™ont—ins only st—tes th—t h—ve — desired
propertyF elso known —s ren™eforth —nd elw—ysF
Existence

„o des™ri˜e — portion of — system9s exe™ution th—t ™ont—ins —n inst—n™e of ™ert—in events or
st—tesF elso known —s iventu—lly
Bounded Existence

„o des™ri˜e — portion of — system9s exe™ution th—t ™ont—ins —t most — spe™i(ed num˜er of
inst—n™es of — design—ted st—te tr—nsition or eventF
pigure PFQX sntent of o™™urren™e p—tternsD —s it —ppe—rs in ‘I“
Precedence

„o des™ri˜e rel—tionships ˜etween — p—ir of eventsGst—tes where the o™™urren™e of the (rst is
— ne™ess—ry preE™ondition for —n o™™urren™e of the se™ondF ‡e s—y th—t —n o™™urren™e of the
se™ond is en—˜led ˜y —n o™™urren™e of the (rstF
Response

„o des™ri˜e ™—useEe'e™t rel—tionships ˜etween — p—ir of eventsGst—tesF en o™™urren™e of the
(rstD the ™—useD must ˜e followed ˜y —n o™™urren™e of the se™ondD the e'e™tF elso known —s
pollows —nd ve—dsEtoF
gh—in p—tterns —re used to express requirements rel—ted to ™omplex ™om˜in—tions of individE
u—l st—teGevent rel—tionshipsF „hese in™lude pre™eden™eGresponse rel—tionships ™onsisting of
sequen™es of individu—l st—tesGeventsF ‡e ™—ll these ™h—in p—tternsF
Chain Precedence

„his is — s™—l—˜le p—tternF ‡e des™ri˜e the I ™—use E P e'e™t version hereF
„o des™ri˜e — rel—tionship ˜etween —n eventGst—te € —nd — sequen™e of eventsGst—tes @ƒD „A in
whi™h the o™™urren™e of ƒ followed ˜y „ within the s™ope must ˜e pre™eded ˜y —n o™™urren™e
of the the sequen™e € within the s—me s™opeF sn st—teE˜—sed form—lismsD the ˜eginning of
the en—˜led sequen™e @ƒD „A m—y ˜e s—tis(ed ˜y the s—me st—te —s the en—˜ling ™ondition
@iFeFD € —nd ƒ m—y ˜e true in the s—me st—teAF
Chain Response

„his is — s™—l—˜le p—tternF ‡e des™ri˜e the intent of the I stimulus E P response version hereF
„o des™ri˜e — rel—tionship ˜etween — stimulus event @€A —nd — sequen™e of two response events
@ƒD„A in whi™h the o™™urren™e of the stimulus event must ˜e followed ˜y —n o™™urren™e of the
sequen™e of response events within the s™opeF sn st—teE˜—sed form—lismsD the st—tes s—tisfying
the response must ˜e distin™t @iFeFD ƒ —nd „ must ˜e true in di'erent st—tes to ™ount —s —
responseAD ˜ut the response m—y ˜e s—tis(ed ˜y the s—me st—te —s the stimulus @iFeFD € —nd
ƒ m—y ˜e true in the s—me st—teAF
pigure PFRX sntent of order p—tternsD —s it —ppe—rs in ‘I“

T

Global

Before R
R

R

After Q
Q

Q

Between Q and R
Q

Q

R

Q

RQ

After Q until R
Q

Q R

Q

pigure PFSX „he illustr—tion of s™opesD —s it —ppe—rs in ‘I“
i—™h p—ttern h—s — s™opeD whi™h is the extent of the progr—m exe™ution over whi™h the
p—ttern must holdF „here —re (ve ˜—si™ kinds of s™opesX glo˜—l @the entire progr—m
exe™utionAD ˜efore @the exe™ution up to — given st—teGeventAD —fter @the exe™ution —fter
— given st—teGeventAD ˜etween @—ny p—rt of the exe™ution from one given st—teGevent to
—nother given st—teGeventA —nd —fterEuntil @like ˜etween ˜ut the design—ted p—rt of the
exe™ution ™ontinues even if the se™ond st—teGevent does not o™™urAF „he s™ope is determined
˜y spe™ifying — st—rting —nd —n ending st—teGevent for the p—tternX the s™ope ™onsists of
—ll st—tesGevents ˜eginning with the st—rting st—teGevent —nd up to ˜ut not in™luding the
ending st—teGeventF
‡e note th—t — s™ope itself should ˜e interpreted —s option—lY if the s™ope delimiters —re not
present in —n exe™ution then the spe™i(™—tion will ˜e trueF
pigure PFTX „he de(nitions of s™opesD —s they —ppe—r in ‘I“

2.3 Problems with the Interpretation
„he se™tions PFI —nd PFP provide inform—l de(nitions of p—tterns —nd s™opesD —s they —re
presented in ‘I“F fut —re these de(nitions goodc e™™ording to ‘IP“D good de(nitions must
˜e ™onsistent —nd un—m˜iguousF …nfortun—telyD inform—l de(nitions tend to give rise to

U

—m˜iguity —nd in™onsisten™yF ‡e illustr—te some —m˜iguities in the inform—l de(nitions
provided for the p—ttern system —nd use the tr—nsl—tions to v„v presented in ‘I“ to motiv—te
more pre™ise de(nitionsD whi™h we then form—lize in gh—pter QF
‡e st—rt from the de(nitions of s™opesD listed in ƒe™tion PFPF

2.3.1

Multiple delimiters in Before and After scopes

„he (rst question —rises from the fefore R s™opeF prom it9s de(nitionD the given st—te R is
the right delimiter for this s™opeF st is not immedi—tely ™le—r whi™h REst—te is the delimiter
for this s™opeD in ™—se there —re sever—l REst—tes present in the exe™utionF „he illustr—tion
in pigure PFS suggests th—t the s™ope goes up to the (rst REst—teF „he ™onstru™tions in the
™orresponding v„v formul—s

. . . UR or . . . WR
suggest th—t this interpret—tion is ™orre™tF
„hereforeD we re(ne the inform—l de(nition of the fefore R s™ope to
Before:

from the ˜eginning of the exe™ution up to the (rst o™™urren™e of — given st—teF

‡e tre—t the ™—se of multiple QEst—tes in efter Q s™ope simil—rlyF „he illustr—tion
in pigure PFS suggests th—t the (rst o™™urren™e of the QEst—te serves —s the left delimiterF
sndeedD the ™onstru™tions

◻ (Q → . . .),
◻ (¬Q) ∨

(Q ∧ . . .),

for e˜sen™eD …nivers—lityD ‚esponse —nd gh—in ‚esponse
for ixisten™e —nd €re™eden™e

Q → (¬Q)U(Q ∧ . . .)

for founded ixisten™e

◻ (¬Q) ∨ (¬Q)U(Q ∧ . . .)

for €re™eden™e gh—in

in the v„v formul—s —re ™onsistent with the interpret—tion th—t the restri™tions on the system
exe™ution st—rt to —pply from the (rst o™™urren™e of — QEst—te @in™lusiveAF „hereforeD we re(ne
the inform—l de(nition of the efter Q s™ope to
V

Q

P

Q

Q

R

P

(a)

Q

R

(b)

pigure PFUX €ossi˜le interpret—tions of fetween Q —nd R s™opesF

After:

from the (rst o™™urren™e of — given st—te until the end of the exe™utionF

2.3.2

Multiple delimiters in Between and After-Until scopes

„he efterE…ntil s™ope is —n un—m˜iguously extended version of fetween s™ope —ndD thereE
foreD everything th—t we ™l—rify for the fefore s™ope —lso —pplies to the efterE…ntil s™opeF
gonsider the fetween Q —nd R s™opeF „he illustr—tion in pigure PFS suggests th—t this
s™ope ™onsists of m—xim—l interv—lsD where e—™h interv—l ends with —n REst—te —nd st—rts
with — QEst—te th—t is the f—rthermost from this REst—teD while not in™luding other REst—tesF
sn the ™—se of sever—l REst—tes —fter — QEst—teD the ™onstru™tions

◻(Q ∧ . . . → . . . UR) or ◻ (Q → (¬R)W(. . . ∧ ¬R)
of v„v formul—s —re ™onsistent with s—ying th—t the restri™tions —pply only until the ™losest

RF
„he ™—se of sever—l QEst—tes is slightly di'erentF por —ll p—tterns ex™ept ixisten™eD the
™onstru™tions of v„v formul—s

◻(Q ∧ . . . → . . .)
—gree with the illustr—tionF
ixisten™e of P D fetween Q —nd RX

◻ (Q ∧ ¬R → (¬R)W(P ∧ ¬R))

@PFIA

gonsider the ex—mpleD shown in pigure PFU—F „he inform—l de(nition of the ixisten™e
p—ttern holds on this m—xim—l interv—lD howeverD the ™orresponding v„v formul— @PFIA f—ilsF
W

„he ™onstru™tion

◻(Q ∧ . . . → . . .)
implies th—t e—™h QEst—te st—rts the interv—lD —s it is shown in pigure PFU˜D —nd for the
ixisten™e p—ttern it is not — m—xim—lD ˜ut — minim—l interv—lF sn this ™—se the inform—l
de(nition is —m˜iguousD —nd the provided illustr—tion f—ils to ™l—rify itF snste—d we propose
the following de(nitions
Between

Q

and

R s™ope ™onsists of —ll interv—ls th—t st—rt with — QEst—te —nd extends to

the next REst—teF
After

Q

Until

R extends fetween s™ope with —ll su0xes th—t ˜egin with — QEst—te —nd

h—ve no su˜sequent REst—tesF

2.3.3

Empty intervals

e™™ording to the de(nitions of s™opesD the left delimiter is in™luded in —nd the right delimiter
is ex™luded from the s™opeF sn the ™—se the delimiters —re not presentD the spe™i(™—tion is
v—™uously TrueF „he n—tur—l question here is how we tre—t empty interv—ls in the s™opesF
„he qlo˜—l s™ope is never emptyF „he efter Q s™ope is not empty if there is — QEst—te
in the exe™utionF
gonsider the s™ope fefore RD when the initi—l st—te in the exe™ution is —n REst—teF
„he initi—l st—te is not in™luded in the s™ope —ndD thereforeD the s™ope ™onsists of —n empty
interv—lF „he spe™i(™—tion is not v—™uously trueD —s the delimiter R is —™tu—lly presentF ‡ith
the fefore R s™opeD the v„v formul—s for —ll p—tterns ex™ept the ixisten™e h—s the form

. . . UR
whi™h is TrueF roweverD the v„v for the ixisten™e p—ttern

(¬R)W(P ∧ ¬R)
is FalseF
IH

por the fetween Q —nd R —nd efter Q until R s™opesD it is possi˜le to h—ve —n empty
interv—l when — st—te is ˜oth — QEst—te —nd —n REst—teF „he v„v formul—s for these s™opes
h—ve the forms

◻ (Q → . . . UR)

for the founded ixisten™e —nd gh—in p—tterns

◻ (Q ∧ ¬R → . . .)

for the rest of the p—tterns

st is e—sy to see th—t —ll of them —re True on the (Q ∧ R) empty interv—lF
„he l—st two ex—mples show some —m˜iguity in the interpret—tion of —n empty interv—l
for the ixisten™e p—ttern with the fefore —nd the fetween s™opesF
sf we tre—t the empty interv—l —s — p—rt of — s™opeD we expe™t the ixisten™e p—ttern
to f—ilF „his interpret—tion is ™onsistent with —ll s™opes ex™ept fetween —nd efterE…ntil
s™opes for the ixisten™e p—tternF sf we —ssume th—t —n empty interv—l is not — p—rt of
— s™opeD then h—ving no other st—tes in the s™ope results the ixisten™e p—ttern ˜eing
v—™uously trueD ˜y the inform—l de(nition of s™opesF „his interpret—tion is ™onsistent with
—ll s™opesD ex™ept the fefore s™ope for the ixisten™e p—tternF
es there is no re—son—˜le —rgument —g—inst —ny of these interpret—tions of s™opesD we
propose — form—liz—tion for e—™h of themF

II

Chapter 3
PROPOSED FORMALIZATION

3.1 Formal Denitions of Strong Scopes
‡e use ™omm—s ˜etween predi™—tes in the me—ning of ™onjun™tionsD to in™re—se the re—d—˜ility
of formul—sF ‡e —ssume pl—™eholders P, Q, R —nd S —re st—te formul—sF
e scope S is rel—tive to — given model of exe™ution σ s0 , s1 , s2 , . . .F ‡e represent — s™ope
—s — set of intervalsD where —n interv—l is — nonempty sequen™e of ™onse™utive num˜ersD
™orresponding to indi™es of the st—tes in the model σ F
Globally:

„he s™ope ™onsists of one interv—l listing —ll the indexes of the st—tes in the model

SG = {[0, ∞)}
Before

@QFIA

R:

„he s™ope ™ont—ins one interv—l —t mostF „his interv—l in™ludes the indi™es of —ll st—tes
˜efore @˜ut not in™ludingA the (rst REst—teF sf —n REst—te is —˜sent or in position HD
the s™ope is empty

SB = {[0, i) s0 ⊫ ¬R, i = min({k > 0 sk ⊫ R})}
R
After

@QFPA

Q:

„he s™ope ™ont—ins one interv—l —t mostF „his interv—l ™orresponds to —ll st—tes o™™urE
ring —fter @—nd in™ludingA the (rst QEst—teF sf no QEst—te existsD the s™ope is empty

SA = {[i, ∞) i = min({k ≥ 0 sk ⊫ Q})}
Q
Between

Q

and

@QFQA

R:

„his s™ope m—y ™onsist of multiple interv—lsF i—™h interv—l st—rts with —n index of —
IP

QEst—te th—t is not —n REst—teD @in™lusiveA —nd extends to the index of the next REst—te
@not in™lusiveAF e QEst—te th—t is —lso —n REst—te is not —n interv—lF

SBW
After

Q

until

QR

= {[i, j) i ≥ 0, si ⊫ (Q ∧ ¬R), j = min({k > i sk ⊫ R})}

@QFRA

R:

„his s™ope extends fetween Q —nd R with —ll su0xes th—t ˜egin with — QEst—te th—t
is not —n REst—te @in™lusiveA —nd h—ve no su˜sequent REst—tesF

SAU

QR

= SBW

QR

∪ {[i, ∞) i ≥ 0, si ⊫ Q, (∀j ≥ i

sj ⊫ ¬R)}

@QFSA

3.2 Formal Denitions of Weak Scopes
„he s™opes de(ned in ƒe™tion QFI ™ont—in no empty interv—ls ˜y ™onstru™tionD in this se™tion
we we—ken this restri™tionF hepending on — model the we—k s™ope SW is either — s™ope S
from ƒe™tion QFID or the s™ope S extended with the empty interv—lF
„here —re only two ™—ses when — s™ope SW m—y ™ont—in —n empty interv—lX
ˆ initi—l st—te is —n REst—te in fefore R s™opeD iFeF s0 ⊫ R
ˆ there is — (Q ∧ R)Est—te in fetween Q —nd R or efter Q until R s™opesD iFeF ∃n ≥

0 sn ⊫ Q ∧ R
rere we provide we—k de(nitions only for fefore RD fetween Q —nd R —nd efter Q until

R s™opesF „he rest of the s™opes ™—n9t possi˜ly ™ont—in —n empty interv—l —ndD thereforeD
their we—ken versions ™oin™ide with the versions de(ned in ƒe™tion QFIF
Weak Before

R:

„he s™ope ™ont—ins one interv—l —t mostF „his interv—l in™ludes the indi™es of —ll st—tes
˜efore @˜ut not in™ludingA the (rst REst—teF sf —n REst—te is —˜sentD the s™ope is emptyF
sf REst—te is in position HD the s™ope ™onsists of —n empty interv—lF

IQ

SW = {[0, i) i = min({k ≥ 0 sk ⊫ R})}
BR
Weak Between

Q

and

@QFTA

R:

„his s™ope m—y ™onsist of multiple interv—lsF i—™h interv—l st—rts with —n index of —

QEst—te @in™lusiveA —nd extends to the index of the next REst—te @not in™lusiveAF e
QEst—te th—t is —lso —n REst—te is —n empty interv—lF
SW
BW
Weak After

Q

until

QR

= {[i, j) si ⊫ Q, j = min({k ≥ i sk ⊫ R})}

@QFUA

R:

„his s™ope extends ‡e—k fetween Q —nd R with —ll su0xes th—t ˜egin with — QEst—te
th—t is not —n REst—te @in™lusiveA —nd h—ve no su˜sequent REst—tesF

SW
AU

QR

= SAU

QR

∪ SW
BW

QR

@QFVA

‡hen we swit™h from S to the we—k version of s™ope SW D v„v formul—s for the ™onstr—ints
th—t use — univers—l qu—nti(™—tion over the elements of the interv—lsD does not ™h—ngeF rowE
everD the use of —n existenti—l qu—nti(er in ixisten™e —nd ƒtrong ixisten™e will f—il the
™onstr—int on —n empty interv—lF

3.3 Formal Denitions of Patterns
e™™ording to the inform—l de(nition of s™opesD when there is no s™opeD —ll p—tterns listed in
ƒe™tion PFI —re TrueF roweverD simil—rly to —n existen™e ˜eing False on —n empty setD one
m—y require the ixisten™e p—ttern to ˜e FalseD when the s™ope is —˜sent @iFeF emptyAF ‡e
introdu™e the ƒtrong ixisten™e p—ttern with ex—™tly th—t —ddition—l requirementF
Absence:

„here is no P Est—te in the s™opeF

∀I ∈ S, ∀n ∈ I sn ⊫ ¬P
IR

@QFWA

Existence:

i—™h interv—l ™ont—ins — P Est—teF

∀I ∈ S, ∃n ∈ I sn ⊫ P

@QFIHA

Strong Existence:

„he s™ope is nonempty —nd e—™h of it9s interv—ls ™ont—ins — P Est—teF

S ≠ ∅, ∀I ∈ S, ∃n ∈ I sn ⊫ P

@QFIIA

Universality:

ivery st—te in the s™ope is — P Est—teF

∀I ∈ S, ∀n ∈ I sn ⊫ P
k

@QFIPA

- Bounded Existence:

qiven —n interv—l I in the s™ope SD we de(ne Max (I, P ) —s — set of m—xim—l P Est—te
su˜interv—ls of I F

Max (I, P ) = {[i, j) [i, j) ⊆ I, ∀m ∈ [i, j) sm ⊫ P,
(i − 1 ∉ I ∨ si−1 ⊫ ¬P ), (j ∉ I ∨ sj ⊫ ¬P )} @QFIQA
xo interv—l in the s™ope ™ont—ins more th—n k m—xim—l P Est—te su˜interv—lsF

∀I ∈ S

Max (I, P ) ≤ k

@QFIRA

Precedence:

sf there is — P Est—teD either it is —n S Est—te or there is —n S Est—te ˜efore it in the s—me
interv—lF

∀I ∈ S, ∀n ∈ I (sn ⊫ P

⇒ ∃m ∈ I (m ≤ n, sm ⊫ S))

IS

@QFISA

Response:

sf there is — P Est—teD either it is —n S Est—te or there is —n S Est—te —fter it in the s—me
interv—lF

∀I ∈ S, ∀n ∈ I (sn ⊫ P

@QFITA

⇒ ∃m ∈ I (m ≥ n, sm ⊫ S))

Precedence Chain:

e su˜sequen™e of st—tes s—tisfying S1 , . . . , Sk pre™edes e—™h su˜sequen™e of st—tes s—tE
isfying P1 , . . . , Pl D if the l—ter existsF st is possi˜le for the Sk Est—te to ™oin™ide with
the P1 Est—teF roweverD —n Si Est—te stri™tly pre™edes Sj Est—te for i < j Y with the simil—r
requirement for the P sequen™eF

∀I ∈ S, ∀n1 ∈ I, . . . , ∀nl ∈ I n1 < . . . < nl (sn1 ⊫ P1 , . . . , snl ⊫ Pl

⇒

@QFIUA

∃m1 ∈ I, . . . , ∃mk ∈ I m1 < . . . < mk ≤ n1 (sm1 ⊫ S1 , . . . , smk ⊫ Sk ))
Response Chain:

e su˜sequen™e of st—tes s—tisfying S1 , . . . , Sk follows e—™h su˜sequen™e of st—tes s—tisE
fying P1 , . . . , Pl D if the l—ter existsF st is possi˜le for the Pl Est—te to ™oin™ide with the

S1 Est—teF roweverD —n Si Est—te stri™tly pre™edes the Sj Est—te for i < j D with the simil—r
requirement for the P sequen™eF

∀I ∈ S, ∀n1 ∈ I, . . . , ∀nl ∈ I n1 < . . . < nl (sn1 ⊫ P1 , . . . , snl ⊫ Pl

⇒

@QFIVA

∃m1 ∈ I, . . . , ∃mk ∈ I nl ≤ m1 < . . . < mk (sm1 ⊫ S1 , . . . , smk ⊫ Sk ))

3.4 Pattern Mappings for LTL
€—renthesizes in the formul—s ˜elow —re set —™™ording to the not—tion introdu™ed in ‘IR“X
tempor—l oper—tors h—ve higher ˜inding power th—t the ˜oole—n onesF 9→9 in v„v formul—s
is equiv—lent to 9

⇒ 9 used everywhere else in this p—per —nd st—nds for the impli™—tionF

„o m—p the inform—l de(nitions of p—tterns —nd s™opes into — pre™ise formul— in ™ommon
form—l spe™i(™—tion l—ngu—gesD one h—s to guess the formul— (rst —nd then verify th—t this
IT

formul— is ™onsistent with the de(nitionsF f—sed on the form—l de(nitions introdu™ed in
ƒe™tions QFID QFP —nd QFQD we were —˜le to form—lly derive ™orresponding v„v formul—sD
there˜y ensuring th—t the tr—nsl—tions —re ™onsistent with our de(nitionsF „his is — m—jor
improvement over the w—y the formul—s in ‘I“ were ™re—tedF „he formul—s th—t we derived —re
not ne™ess—rily identi™—l to the formul—s in ‘I“F sn ™—ses where the formul— th—t we derived
di'ers from the tr—nsl—tion in ‘I“D we provide — proof th—t the formul—s —re equiv—lent or —
™ounterex—mple th—t shows they —re not equiv—lentF
hue to the over—ll ™omplexity of m—nu—l deriv—tion of these formul—sD we de™ided to
limit the extent of this work to the e˜sen™eD ixisten™eD ƒtrong ixisten™e —nd …niE
vers—lity p—tterns with ˜oth ƒtrong —nd ‡e—k versions of —ll s™opesD —nd the €re™eden™e
—nd ‚esponse p—tterns with the qlo˜—lly s™opeF fy doing soD we ™over VW7 of the SSS
p—tternGs™ope ™om˜in—tions mentioned in the survey in ‘U“F
yur v„v formul—s in „—˜le QFI —re proven to ˜e equiv—lent to the ™orresponding origin—l
formul—s ˜y wFhwyer et —lF ‘I“F „he proofs —re listed in the eppendix fF
‡e simpli(ed the v„v formul—s for the e˜sen™e —nd …nivers—lity p—tterns with ˜oth
fetween —nd efterE…ntil s™opes ˜y removing the redund—nt ¬R term from the —nte™edent
of the impli™—tionF ‡e —lso (xed — typogr—phi™—l error in the ixisten™e p—ttern with efter
s™opeF
sn ƒe™tion PFQFQ we des™ri˜ed the in™onsistent tre—tment of empty interv—ls in the origin—l
work ˜y wFhwyer et —lF „o resolve this pro˜lem we proposed two possi˜le form—liz—tionsX
strong s™opes —nd we—k s™opes @ƒe™tions QFI —nd QFP respe™tivelyAF ‡e show the ™orrespondE
ing v„v formul—s for these versions of s™opes in „—˜le QFPF st is enough to list only the
formul—s rel—ted to existenti—l p—tternsD —s there is no essenti—l di'eren™e ˜etween strong
—nd we—k s™opes for the other p—tterns —nd these formul—s —re listed in „—˜le QFIF
por ˜oth ™—sesD if we ignore empty interv—ls @strong s™opesA or t—ke them into —™™ount
@we—k s™opesAD we propose the v„v formul—sF ell formul—s in „—˜le QFP —re proven to ˜e
™onsistent with our de(nitions of strong —nd we—k s™opes in eppendix fF ‡e highlight in

IU

€roperty €—ttern

xew

yrigin—l @if di'erentA

Absence of P
qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R

◻(¬P )
R → (¬P )UR
◻(Q → ◻(¬P ))
◻(Q ∧ R → (¬P )UR)
◻(Q → (¬P )WR)

◻(Q ∧ ¬R ∧ R → (¬P )UR)
◻(Q ∧ ¬R → (¬P )WR)

P
see „—˜le
◻(¬Q) ∨
see „—˜le
see „—˜le

(¬R)W(P ∧ ¬R)
◻(¬Q) ∨ (Q ∧ P )) typo
◻(Q ∧ ¬R → (¬R)W(P ∧ ¬R))
◻(Q ∧ ¬R → (¬R)U(P ∧ ¬R))

Existence of

P

qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R
Universality of

QFP
(Q ∧
QFP
QFP

P)

P

qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R

◻P
R → P UR
◻(Q → ◻P )
◻(Q ∧ R → P UR)
◻(Q → P WR)

S precedes P
qlo˜—lly

(¬P )WS

S responds
qlo˜—lly

to

◻(Q ∧ ¬R ∧ R → P UR)
◻(Q ∧ ¬R → P WR)

P
◻(P →

S)

„—˜le QFIX €roposed v„v formul—s vsF origin—l formul—s ˜y wFhwyer et —lF
˜old the formul—s th—t —re equiv—lent to the the origin—l formul—s ˜y wFhwyer et —lF es it
w—s st—ted in ƒe™tion PFQFQD origin—l formul—s for the ixisten™e p—ttern with the fetween
—nd efterE…ntil s™opes ignore empty interv—lsD while the formul— for the fefore s™ope
does notF
‡hile the proposed p—ttern ƒtrong ixisten™e is not equiv—lent to the ixisten™e p—tE
tern ˜y wFhwyer et —lFD we think some users m—y (nd this —ltern—tive interpret—tion to ˜e
v—lu—˜leF

IV

€roperty €—ttern
Existence of

v„v formul— forX
ƒtrong s™opes

‡e—k s™opes

P
R ∨ ¬(¬P )UR
◻(¬Q) ∨ (Q ∧ P )
◻(Q ∧ ¬R → ¬(¬P )U R)
◻(Q ∧ ¬R → ¬(¬P )WR)

P
¬(¬P )U R
◻(¬Q) ∨ (Q ∧ P )
◻(Q → ¬(¬P )UR)
◻(Q → ¬(¬P )WR)

P

qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R

Strong Existence of

qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R

P
P
R ∧ ¬(¬P )UR
(Q ∧ P )
(Q ∧ ¬R ∧ R)∧
◻(Q ∧ ¬R → ¬(¬P )UR)
(Q ∧ ¬R)∧
◻(Q ∧ ¬R → ¬(¬P )WR)

P
R ∧ ¬(¬P )UR
(Q ∧ P )
(Q ∧ R)∧
◻(Q → ¬(¬P )UR)
(Q ∧ (¬R ∨ R))∧
◻(Q → ¬(¬P )WR)

„—˜le QFPX €roposed v„v formul—s for ‡e—k —nd ƒtrong s™opesF fold formul—s —re equiv—lent
to origin—l formul—s of wFhwyer et —lF

IW

Chapter 4
RELATED WORK

„his work is ˜—sed on the spe™i(™—tion p—ttern system @ƒ€ƒA des™ri˜ed in hwyer et —lF ‘TD U“
—nd the tr—nsl—tions of p—tterns to v„v in ‘I“F
ƒever—l —ppro—™hes were proposed to form—lize —nd extend ƒ€ƒD —nd to verify the tr—nsE
l—tions to di'erent form—lismsF €‚y€iv ‘PQ“ uses the dis™iplined n—tur—l l—ngu—ge @hxvA
—nd the (niteEst—te —utom—ton @pƒeA not—tions to form—lize most ™ommon p—tterns in ƒ€ƒF
„his —ppro—™h —ssumes only the eventE˜—sed form—lism —nd tr—nsl—tes p—tterns only ˜etween
hxv —nd pƒeF
€rospe™ ‘IU“ extends ƒ€ƒ with IP ™l—sses of ™omposite propositions @g€AD —llowing the
use of multiple propositions in — p—ttern or —s — delimiter of the s™opeF e tool inter—™tively
guide the user during the spe™i(™—tion pro™ess —nd tr—nsl—tes the spe™i(™—tion to future
interv—l logi™ or v„vF rowever ‘IU“ does not provide —ny det—ils —˜out the ™orre™tness of the
gener—ted v„v formul—sF
ƒ—l—m—h et —lF ‘PI“ extend ide—s of €rospe™tF „he p—per ™onsiders R p—tterns out of the
VD de(ned ˜y hwyer et —lF —nd g€s from €rospe™D tr—nsl—tes g€ ™l—sses to v„vD extends
v„v with —n —ddition—l ™onjun™tion oper—tor —nd tr—nsl—tes R p—tterns —nd S s™opes into
the extended v„vF sn ‘PP“D ƒ—l—m—h form—lly proves ™orre™tness of the formul—s within the
qlo˜—l s™ope —nd tests the formul—s within the fefore R s™opeF re el—˜or—tes on the g€
extensionD uses nonEst—nd—rd extension of v„v for the tr—nsl—tion —nd does not verify most
of the formul—sF
q—r™i— —nd ‚o—™h ‘IH“ developed the €roperty „esting „ool @€rotestAD whi™h —utom—tiE
™—lly gener—tes —nd tests v„v formul—s representing spe™i(™—tionsF „hey did some —ddition—l
testing of the formul—s in ‘PI“D ˜ut their tests ™overed only — sm—ll su˜set of properties —nd
g€ ™l—ssesF

PH

Chapter 5
CONCLUSIONS

„he use of p—tterns is — w—y for experts to sh—re their knowledgeF vike design p—tternsD
spe™i(™—tion p—tterns prep—red ˜y —n expert speed up the pro™ess of writing spe™i(™—tions —nd
widen the use of form—l methods in softw—re developmentF „he ƒ€ƒ developed ˜y hwyer et —lF
is well known —nd e—sily —™™essi˜le through — we˜ site ‘I“F ‡hile ˜eing prep—red —nd reviewed
˜y expertsD this ™olle™tion is not gu—r—nteed to ˜e ™orre™tF „he de(nitions of p—tterns —nd
s™opes h—ve to ˜e pre™ise —nd their tr—nsl—tion to other form—lisms h—ve to ˜e veri(edF es
we showed in ƒe™tion PFQ the origin—l de(nitions ™ont—in some —m˜iguity —nd their m—nner
of interpret—tion does not —ppe—r to —lw—ys ˜e ™onsistentF st m—kes little sense to verify the
form—l v„v formul—s o˜t—ined from the inform—l de(nitionsF ‡e proposed — form—liz—tion
of p—tterns —nd s™opes th—t is e—sy to re—dD ™losely resem˜les the origin—l de(nitionsD —nd
is pre™iseF „hese form—l de(nitions were used to form—lly derive the ™orresponding v„v
formul—sF ‡e veri(ed the formul—s provided in ‘I“ ˜y showing their equiv—len™e to the
formul—s we derivedF fe™—use of the ™omplexity of the m—nu—l proofsD we ™onsidered only the
most popul—r ™om˜in—tions of p—tterns —nd s™opesF e˜sen™eD ixisten™e —nd …nivers—lity
p—tterns —re veri(ed with —ll (ve s™opesY €re™eden™e —nd ‚esponse —re veri(ed with
qlo˜—l s™ope onlyF prom SSS p—tternsGs™opes listed in the survey ‘U“ we ™overed VW7 of
themF ‡e provide the —ddition—l p—tternD ƒtrong ixisten™eD whi™h is False on the empty
s™opeF „he ™orresponding v„v formul—s for this p—ttern with —ll (ve s™opes were derived
—nd —lso veri(edF

PI

APPENDICES

PP

Appendix A
ORIGINAL LTL FORMULAS

€—renthesizes in the formul—s ˜elow —re set —™™ording to the not—tion introdu™ed in ‘IR“X
tempor—l oper—tors h—ve higher ˜inding power th—t the ˜oole—n onesF

PQ

€roperty €—ttern
Absence of

v„v formul—s ˜y wFhwyer et —lF

P

qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R
Existence of

◻(¬P )
R → (¬P )UR
◻(Q → ◻(¬P ))
◻(Q ∧ ¬R ∧ R → (¬P )UR)
◻(Q ∧ ¬R → (¬P )WR)

P

qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R
Universality of

P
(¬R)W(P ∧ ¬R)
◻(¬Q) ∨ (Q ∧ P )) typo
◻(Q ∧ ¬R → (¬R)W(P ∧ ¬R))
◻(Q ∧ ¬R → (¬R)U(P ∧ ¬R))

P

qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R

◻P
R → P UR
◻(Q → ◻P )
◻(Q ∧ ¬R ∧ R → P UR)
◻(Q ∧ ¬R → P WR)

S precedes P
qlo˜—lly
fefore R
efter Q
fetween Q —nd R
efter Q until R

(¬P )WS
R → (¬P )W(S ∨ R)
(¬Q)W(Q ∧ (¬P )WS)
◻((Q ∧ ¬R ∧ R) → (¬P )W(S ∨ R))
◻(Q ∧ ¬R → (¬P )W(S ∨ R))

S responds to P
qlo˜—lly
◻(P → S)
fefore R
R → (P → (¬R)U(S ∧ ¬R))UR
efter Q
(¬Q)W(Q ∧ ◻(P → S))
fetween Q —nd R ◻((Q ∧ ¬R ∧ R) →
(P → (¬R)U(S ∧ ¬R))UR)
efter Q until R
◻(Q ∧ ¬R →
((P → (¬R)U(S ∧ ¬R)))WR)
„—˜le eFIX v„v formul—s presented in ‘I“
PR

Appendix B
PROOFS OF EQUIVALENCE

fefore st—rting the proofs of equiv—len™esD we de(ne —nd prove two —uxili—ry ™l—imsF
Claim 1.

¬(¬P )UR ⇐⇒ (¬R)W(P ∧ ¬R)

@fFIA

Proof of the Claim 1. ‡e w—nt to show
¬(¬P )UR ⇐⇒ ◻(¬R) ∨ (¬R)U(P ∧ ¬R)
ƒuppose there is no REst—te in our modelF st is e—sy to see th—t ˜oth v„vs —re TrueF
por the rest of the proof we —ssume —n REst—te exists —nd show

¬(¬P )UR ⇐⇒ (¬R)U(P ∧ ¬R)
sf ¬(¬P )UR is TrueD (¬P )UR is FalseF es —n REst—te exists ˜y our —ssumptionD there is
— P Est—te ˜efore the (rst REst—teF „herefore (¬R)U(P ∧ ¬R) is TrueF
sf (¬R)U(P ∧ ¬R) is TrueD there exists — P Est—te ˜efore —ny REst—teF „hen (¬P )UR is

False —nd ¬(¬P )UR is TrueF ‡e proved the i' rel—tion in @fFIAF

∎

Claim 2.

¬(¬P )WR ⇐⇒ (¬R)U(P ∧ ¬R)

@fFPA

Proof of the Claim 2.
¬(¬P )WR = ¬(◻(¬P ) ∨ (¬P )UR) =

P ∧ ¬(¬P )UR

ƒuppose there is no REst—te in our modelF foth ¬(¬P )WR —nd (¬R)U(P ∧ ¬R) redu™e to

PF
por the rest of the proof we —ssume there is —n REst—teF sn the proof of gl—im I we9ve
shown (¬R)U(P ∧ ¬R) ⇐⇒ ¬(¬P )URF
PS

sf (¬R)U(P ∧ ¬R) is FalseD
sf

P ∧ ¬(¬P )UR is —lso FalseF

P ∧ ¬(¬P )UR is FalseD either

P D ¬(¬P )UR or ˜oth —re FalseF st is e—sy to see th—t

(¬R)U(P ∧ ¬R) is False in —ll these ™—sesF „his proves @fFPAF

B.0.1

∎

Absence

B.0.1.1

Globally

◻(¬P ) ≈ e˜sen™e of P, qlo˜—lly

Proof.
e˜sen™e of P, qlo˜—lly ≡ ∀I ∈ SG , ∀n ∈ I sn ⊫ ¬P, where SG = {[0, ∞)}

SG h—s only one interv—lD [0, ∞)D so the ‚rƒ of the equ—tion —˜ove is
∀n > 0 sn ⊫ ¬P
F „his is ex—™tly the me—ning of ◻(¬P ) in (rstEorder predi™—te logi™F

B.0.1.2

Before

∎

R

Claim 3.

∀i ≥ 0 (s0 ⊫ ¬R, i = min({k > 0 sk ⊫ R})

⇒ φ(i)) ≡

∃j ≥ 0 sj ⊫ R

PT

⇒ ∃i ≥ 0 (si ⊫ R, φ(i)) @fFQA

Proof.
∀i ≥ 0 (s0 ⊫ ¬R, i = min({k > 0 sk ⊫ R})
s0 ⊫ R ∨ ∀i ≥ 0 (i = min({k > 0 sk ⊫ R})

⇒ φ(i))

⇐⇒

⇒ φ(i))

⇐⇒

s0 ⊫ R ∨ ∀j ≥ 0 sj ⊫ ¬R ∨ ∃i > 0 (i = min({k > 0 sk ⊫ R}), φ(i))

⇐⇒

∀j ≥ 0 sj ⊫ ¬R ∨ ∃i ≥ 0 (i = min({k ≥ 0 sk ⊫ R}), φ(i))

⇐⇒

∃j ≥ 0 sj ⊫ R

⇒ ∃i ≥ 0 (i = min({k ≥ 0 sk ⊫ R}), φ(i))

⇐⇒

∃j ≥ 0 sj ⊫ R

⇒ ∃i ≥ 0 (si ⊫ R, φ(i))
∎

R → (¬P )UR ≈ e˜sen™e of P, fefore R

@fFRA

Proof. e™™ording to @QFWA
e˜sen™e of P, fefore R ≡ ∀I ∈ SB , ∀n ∈ I sn ⊫ ¬P
R
it follows from @QFPA th—t

∀I ∈ SB , ∀n ∈ I sn ⊫ ¬P ≡
R
∀i ≥ 0 (s0 ⊫ ¬R, i = min({k > 0 sk ⊫ R})

⇒ ∀n ∈ [0, i) sn ⊫ ¬P )

˜y gl—im QD the ‚rƒ of the equiv—len™e holds i' the following holds

∃j ≥ 0 sj ⊫ R
this is the de(nition of

B.0.1.3

After

⇒ ∃i ≥ 0 (si ⊫ R, ∀n ∈ [0, i) sn ⊫ ¬P )

R → (¬P )URF

∎

Q
◻(Q → ◻(¬P )) ≈ e˜sen™e of P, efter Q

PU

@fFSA

Proof. e™™ording to @QFWA
e˜sen™e of P, efter Q ≡ ∀I ∈ SA , ∀n ∈ I sn ⊫ ¬P
Q
it follows from @QFQA th—t

∀I ∈ SA , ∀n ∈ I sn ⊫ ¬P ≡
Q
∀i ≥ 0 (i = min({k ≥ 0 sk ⊫ Q})

⇒ ∀n ∈ [i, ∞) sn ⊫ ¬P )

the ‚rƒ of the equiv—len™e holds i' the following holds

∀i ≥ 0 (si ⊫ Q

⇒ ∀n ∈ [i, ∞) sn ⊫ ¬P )

this is the de(nition of ◻(Q → ◻(¬P ))F

B.0.1.4

Between

Q

◻(Q ∧

and

∎

R

R → (¬P )UR) ≈ e˜sen™e of P, fetween Q —nd R

@fFTA

Proof. e™™ording to @QFWA
e˜sen™e of P, fetween Q —nd R ≡ ∀I ∈ SBW

QR

, ∀n ∈ I sn ⊫ ¬P

it follows from @QFRA th—t

∀I ∈ SBW , ∀n ∈ I sn ⊫ ¬P ≡
QR
∀i ≥ 0, ∀j ≥ 0 (i ≥ 0, si ⊫ (Q ∧ ¬R), j = min({k > i sk ⊫ R})

⇒

∀n ∈ [i, j) sn ⊫ ¬P )

PV

the ‚rƒ of the equiv—len™e holds i' the following holds

∀i ≥ 0, ∀j ≥ 0 (si ⊫ (Q ∧ ¬R), j = min({k > i sk ⊫ R})

⇒

∀n ∈ [i, j) sn ⊫ ¬P )

⇐⇒

⇒ ∀n ∈ [i, j) sn ⊫ ¬P ))

⇐⇒

∀i ≥ 0 (si ⊫ ¬(Q ∧ ¬R) ∨
∀j ≥ 0 (j = min({k > i sk ⊫ R})

∀i ≥ 0 (si ⊫ ¬Q ∨ si ⊫ R ∨ ∀m > i sm ⊫ ¬R ∨
∃j ≥ 0 (j = min({k > i sk ⊫ R}), ∀n ∈ [i, j) sn ⊫ ¬P ))

⇐⇒

∀i ≥ 0 (si ⊫ ¬Q ∨ si ⊫ R ∨ ∀m ≥ i sm ⊫ ¬R ∨
∃j ≥ 0 (j = min({k > i sk ⊫ R}), ∀n ∈ [i, j) sn ⊫ ¬P ))

⇐⇒

∀i ≥ 0 (si ⊫ ¬Q ∨ ∀m ≥ i sm ⊫ ¬R ∨
∃j ≥ 0 (j = min({k ≥ i sk ⊫ R}), ∀n ∈ [i, j) sn ⊫ ¬P ))
∀i ≥ 0 (si ⊫ Q, ∃m ≥ i sm ⊫ R

⇒

∃j ≥ 0 (j = min({k ≥ i sk ⊫ R}), ∀n ∈ [i, j) sn ⊫ ¬P ))
∀i ≥ 0 (si ⊫ Q, ∃m ≥ i sm ⊫ R

⇐⇒

⇐⇒

⇒

∃j ≥ 0 (sj ⊫ R, ∀n ∈ [i, j) sn ⊫ ¬P ))
this is the de(nition of ◻(Q ∧

B.0.1.5

After

Q

until

R → (¬P )UR)F

∎

R

◻(Q → (¬P )WR) ≈ e˜sen™e of P, efter Q until R

Proof. e™™ording to @QFWA
e˜sen™e of P, efter Q until R ≡ ∀I ∈ SAU , ∀n ∈ I sn ⊫ ¬P
QR

PW

@fFUA

it follows from @QFSA th—t

∀I ∈ SAU , ∀n ∈ I sn ⊫ ¬P ⇐⇒
QR
(∀I ∈ SBW , ∀n ∈ I sn ⊫ ¬P ) ∧ (∀I ∈ (SAU
− SBW ), ∀n ∈ I sn ⊫ ¬P )
QR
QR
QR
por the left p—rt of the ™onjun™tion

∀I ∈ SBW , ∀n ∈ I sn ⊫ ¬P ≡
QR
∀i ≥ 0, ∀j ≥ 0 (i ≥ 0, si ⊫ (Q ∧ ¬R), j = min({k > i sk ⊫ R})

⇒

∀n ∈ [i, j) sn ⊫ ¬P )
in @fFTA we h—ve shownD it is ◻(Q ∧

R → (¬P )UR)F

sn the right p—rt of the ™onjun™tion

∀I ∈ (SAU

QR

− SBW

QR

), ∀n ∈ I sn ⊫ ¬P ≡
∀i ≥ 0 (i ≥ 0, si ⊫ Q, ∀j ≥ i sj ⊫ ¬R

⇒ ∀n ≥ i sn ⊫ ¬P )

the ‚rƒ of the equiv—len™e holds i' the following holds

∀i ≥ 0 (si ⊫ Q, ∀j ≥ i sj ⊫ ¬R

⇒ ∀n ≥ i sn ⊫ ¬P )

this is the de(nition of ◻(Q ∧ ◻(¬R) → ◻(¬P ))F
gonjun™tion of these v„v

◻ (Q ∧
◻ ((Q ∧

R → (¬P )UR) ∧ ◻(Q ∧ ◻(¬R) → ◻(¬P ))

=

R → (¬P )UR) ∧ (Q ∧ ◻(¬R) → ◻(¬P )))

=

◻ (¬Q ∨ ( R ∨ ◻(¬P )) ∧ (◻(¬R) ∨ (¬P )UR))
gonsider two ™—sesX

R =True or

R =False for the formul—

( R ∨ ◻(¬P )) ∧ (◻(¬R) ∨ (¬P )UR)
QH

@fFVA

sf

R =TrueD we h—ve

True ∧ (¬P )UR = (¬P )UR
sf

R =FalseD
◻(¬P ) ∧ True = ◻(¬P )

thereforeD

( R ∨ ◻(¬P )) ∧ (◻(¬R) ∨ (¬P )UR) = (¬P )UR ∨ ◻(¬P )

@fFWA

(n—llyD from @fFVA —nd @fFWA it follows

◻(¬Q ∨ (¬P )UR ∨ ◻(¬P )) = ◻(Q → (¬P )WR)
∎

B.0.2

B.0.2.1

Existence with Strong Scopes

Globally

P ≈ ixisten™e of P, qlo˜—lly

Proof.
∀I ∈ SG , ∃n ∈ I sn ⊫ P, where SG = {[0, ∞)}
„he s™ope qlo˜—llyD SG D ™ont—ins only one interv—l [0, ∞)F por this ™—se the de(nition of
ixisten™e tr—nsforms to

∃n ∈ [0, ∞) sn ⊫ P
„his is ex—™tly the me—ning of

B.0.2.2

Before

PF

∎

R
R ∨ ¬(¬P )UR ≈ ixisten™e of P, fefore R

QI

@fFIHA

Proof. e™™ording to @QFIHA
ixisten™e of P, fefore R ≡ ∀I ∈ SB , ∃n ∈ I sn ⊫ P
R
it follows from @QFPA th—t

∀I ∈ SB , ∃n ∈ I sn ⊫ P ≡
R
∀i ≥ 0 (s0 ⊫ ¬R, i = min({k > 0 sk ⊫ R})

⇒ ∃n ∈ [0, i) sn ⊫ P )

the ‚rƒ of the equiv—len™e holds i' the following holds

s0 ⊫ R ∨ ∀i ≥ 0 (i = min({k > 0 sk ⊫ R})

⇒ ∃n ∈ [0, i) sn ⊫ P )

⇐⇒

s0 ⊫ R ∨ ∀i ≥ 0, ∃n ∈ [0, i) (i = min({k > 0 sk ⊫ R})

⇒ sn ⊫ P )

⇐⇒

s0 ⊫ R ∨ ∀i ≥ 0, ∃n ∈ [0, i) (i = min({k ≥ 0 sk ⊫ R})

⇒ sn ⊫ P )

⇐⇒

s0 ⊫ R ∨ ∀i ≥ 0, ∃n ∈ [0, i) (si ⊫ R

⇒ sn ⊫ P )

s0 ⊫ R ∨ ∀i ≥ 0, ∃n ∈ [0, i) (si ⊫ ¬R ∨ sn ⊫ P )

⇐⇒
⇐⇒

s0 ⊫ R ∨ ¬(∃i ≥ 0, ∀n ∈ [0, i) (si ⊫ R, sn ⊫ ¬P ))
this is the de(nition of R ∨ ¬(¬P )URF

∎

epplying gl—im ID we show

R ∨ ¬(¬P )UR ⇐⇒ R ∨ (¬R)W(P ∧ ¬R)

B.0.2.3

After

Q
◻(¬Q) ∨

(Q ∧

P ) ≈ ixisten™e of P, efter Q

Proof. e™™ording to @QFIHA
ixisten™e of P, efter Q ≡ ∀I ∈ SA , ∃n ∈ I sn ⊫ P
Q

QP

@fFIIA

it follows from @QFQA th—t

∀I ∈ SA , ∃n ∈ I sn ⊫ P ≡
Q

∀i ≥ 0 (i = min({k ≥ 0 sk ⊫ Q})

⇒ ∃n ∈ [i, ∞) sn ⊫ P )

the ‚rƒ of the equiv—len™e holds i' the following holds

(∀j ≥ 0 sj ⊫ ¬Q) ∨ (∃i ≥ 0 (i = min({k ≥ 0 sk ⊫ Q}) ∧ ∃n ∈ [i, ∞) sn ⊫ P )
(∀j ≥ 0 sj ⊫ ¬Q) ∨ (∃i ≥ 0 (si ⊫ Q ∧ ∃n ∈ [i, ∞) sn ⊫ P )
this is the de(nition of ◻(¬Q) ∨

B.0.2.4

Between

Q

and

(Q ∧

P )F

∎

R

◻(Q ∧ ¬R → (¬R)W(P ∧ ¬R)) ≈ ixisten™e of P, fetween Q —nd R

@fFIPA

Proof. e™™ording to @QFIHA
ixisten™e of P, fetween Q —nd R ≡ ∀I ∈ SBW , ∃n ∈ I sn ⊫ P
QR
it follows from @QFRA th—t

∀I ∈ SBW , ∃n ∈ I sn ⊫ P ≡
QR
∀i ≥ 0, ∀j ≥ 0 ((si ⊫ (Q ∧ ¬R), j = min({k > i sk ⊫ R}))

⇒

∃n ∈ [i, j) sn ⊫ P )
the ‚rƒ of the equiv—len™e holds i' the following holds

∀i ≥ 0, ∀j > i, ∃n ∈ [i, j) ((si ⊫ (Q ∧ ¬R), sj ⊫ R)

⇒ sn ⊫ P )

⇐⇒

∀i ≥ 0, ∀j ≥ i, ∃n ∈ [i, j) ((si ⊫ (Q ∧ ¬R), sj ⊫ R)

⇒ sn ⊫ P )

⇐⇒

∀i ≥ 0, ∀j ≥ i, ∃n ∈ [i, j) (si ⊫ (Q ∧ ¬R)

⇒ (sj ⊫ ¬R ∨ sn ⊫ P ))

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇒ ∀j ≥ i, ∃n ∈ [i, j) (sj ⊫ ¬R ∨ sn ⊫ P ))

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇐⇒

⇒ ¬(∃j ≥ i, ∀n ∈ [i, j) (sj ⊫ R, sn ⊫ ¬P )))

this is the de(nition of ◻(Q ∧ ¬R → ¬(¬P )UR)F
QQ

⇐⇒

∎

epplying gl—im I we show equiv—len™e

◻(Q ∧ ¬R → ¬(¬P )UR) ⇐⇒ ◻(Q ∧ ¬R → (¬R)W(P ∧ ¬R))

B.0.2.5

After

Q

until

R

◻(Q ∧ ¬R → (¬R)U(P ∧ ¬R)) ≈ ixisten™e of P, efter Q until R

@fFIQA

Proof. e™™ording to @QFIHA
ixisten™e of P, efter Q until R ≡ ∀I ∈ SAU

QR

, ∃n ∈ I sn ⊫ P

it follows from @QFSA th—t

∀I ∈ SAU , ∃n ∈ I sn ⊫ P ⇐⇒
QR
(∀I ∈ SBW , ∃n ∈ I sn ⊫ P ) ∧ (∀I ∈ (SAU
− SBW ), ∃n ∈ I sn ⊫ P )
QR
QR
QR

(∀I ∈ SBW

QR

, ∃n ∈ I sn ⊫ P ) ∧ (∀I ∈ (SAU

QR

− SBW

QR

∀i ≥ 0, ∀j ((si ⊫ (Q ∧ ¬R), j = min({k > i sk ⊫ R}))

), ∃n ∈ I sn ⊫ P ) ≡
⇒ ∃n ∈ [i, j) sn ⊫ P ) ∧

∀i ≥ 0 ((si ⊫ Q, ∀j ≥ i sj ⊫ ¬R)

⇒ ∃n ≥ i sn ⊫ P )

the ‚rƒ of the equiv—len™e holds i' the following holds

∀i ≥ 0, ∀j > i ((si ⊫ (Q ∧ ¬R), sj ⊫ R)

⇒ ∃n ∈ [i, j) sn ⊫ P ) ∧

∀i ≥ 0 ((si ⊫ (Q ∧ ¬R), ∀j > i sj ⊫ ¬R)

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇒ ∀j > i (sj ⊫ ¬R ∨ ∃n ∈ [i, j) sn ⊫ P )) ∧

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇒ ∃n ≥ i sn ⊫ P )

⇒ (∃j > i sj ⊫ R ∨ ∃n ≥ i sn ⊫ P ))

⇒
∀j > i (sj ⊫ ¬R ∨ ∃n ∈ [i, j) sn ⊫ P ) ∧
(∃j > i sj ⊫ R ∨ ∃n ≥ i sn ⊫ P ))
QR

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇒

¬( ¬(∀j > i (sj ⊫ ¬R ∨ ∃n ∈ [i, j) sn ⊫ P )) ∨
¬(∃j > i sj ⊫ R ∨ ∃n ≥ i sn ⊫ P ) ))

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇒

¬( ∃j > i (sj ⊫ R ∧ ∀n ∈ [i, j) sn ⊫ ¬P ) ∨
(∀j > i sj ⊫ ¬R ∧ ∀n ≥ i sn ⊫ ¬P ) )) @fFIRA
—ssume si ⊫ (Q ∧ ¬R) holds in @fFIRAD then we ™—n swit™h to we—k inequ—lities

∃j > i (sj ⊫ R ∧ ∀n ∈ [i, j) sn ⊫ ¬P ) ⇐⇒ ∃j ≥ i (sj ⊫ R ∧ ∀n ∈ [i, j) sn ⊫ ¬P )
∀j > i sj ⊫ ¬R ⇐⇒ ∀j ≥ i sj ⊫ ¬R
therefore @fFIRA holds i'

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇒

¬( ∃j ≥ i (sj ⊫ R ∧ ∀n ∈ [i, j) sn ⊫ ¬P ) ∨
(∀j ≥ i sj ⊫ ¬R ∧ ∀n ≥ i sn ⊫ ¬P ) )) @fFISA
„o show ∀j ≥ i sj ⊫ ¬R is redund—ntD it is enough to ™onsider the ™—se

∃j ≥ i (sj ⊫ R ∧ ∀n ∈ [i, j) sn ⊫ ¬P ) = F alse
∀j ≥ i sj ⊫ ¬R = F alse
∀j ≥ i sj ⊫ ¬R is the neg—tion of ∃j ≥ i sj ⊫ RD therefore
∀n ∈ [i, j) sn ⊫ ¬P = F alse
it follows

∀n ≥ i sn ⊫ ¬P = F alse

QS

—nd ∀j ≥ i sj ⊫ ¬R is redund—ntF

∀i ≥ 0 (si ⊫ (Q ∧ ¬R)

⇒

¬( ∃j ≥ i (sj ⊫ R ∧ ∀n ∈ [i, j) sn ⊫ ¬P ) ∨ (∀n ≥ i sn ⊫ ¬P ) )) @fFITA
(n—llyD using the following

◻(¬P ) ∨ (¬P )UR = (¬P )WR
∃j ≥ i (sj ⊫ R ∧ ∀n ∈ [i, j) sn ⊫ ¬P ) ≡ (¬P )UR
∀n ≥ i sn ⊫ ¬P ≡ ◻(¬P )
we show th—t @fFITA is equiv—lent to

◻(Q ∧ ¬R → ¬(¬P )WR)

@fFIUA

∎
pin—llyD we —pply gl—im P to show

◻(Q ∧ ¬R → ¬(¬P )WR) ⇐⇒ ◻(Q ∧ ¬R → (¬R)U(P ∧ ¬R))

B.0.3

Strong Existence with Strong Scopes

gomp—ring to ixisten™eD ƒtrong ixisten™e —dds the requirement for — s™ope not to ˜e
emptyF sn the following proofsD we st—rt from deriving the v„v formul— for this requirementD
then ™onjoining this derived formul— with v„vs for ixisten™eD o˜t—ined in ƒe™tion fFHFPF

B.0.3.1

Globally

P ≈ ƒtrong ixisten™e of P, qlo˜—lly

Proof. „he s™ope SG = {[0, ∞)} is not emptyD thus ƒtrong ixisten™e is equiv—lent to ixE
isten™e on this s™opeF

∎
QT

B.0.3.2

Before

R

‡e prove the equiv—len™e using the proposed formul—

R ∧ ¬(¬P )UR ≈ ƒtrong ixisten™e of P, fefore R

@fFIVA

Proof. e™™ording to @QFPA
SB ≠ ∅ ≡ ∃i ≥ 0 (s0 ⊫ ¬R, i = min({k > 0 sk ⊫ R}))
R

∃i ≥ 0 (s0 ⊫ ¬R, i = min({k > 0 sk ⊫ R}))

⇐⇒

s0 ⊫ ¬R, ∃i ≥ 0 (i = min({k > 0 sk ⊫ R}))

⇐⇒

s0 ⊫ ¬R, ∃i ≥ 0 si ⊫ R
this is the de(nition of ¬R ∧

(¬R ∧

RF gonjoining with v„v from @fFIHAD we get

R) ∧ (R ∨ ¬(¬P )UR)

⇐⇒

R ∧ (¬R ∧ (R ∨ ¬(¬P )UR))

⇐⇒

R ∧ ((¬R ∧ R) ∨ (¬R ∧ ¬(¬P )UR)

⇐⇒
@fFIWA

R ∧ ¬R ∧ ¬(¬P )UR

„he ¬R term is redund—ntF „o prove itD it is enough to show th—t @fFIWA is FalseD if ¬R is

False X
R is True —nd (¬P )UR is —lso TrueD thusD ¬(¬P )UR is False —nd the formul— is FalseF
‡e h—ve shown the equiv—len™e with the following v„v formul—

R ∧ ¬(¬P )UR
„his (nishes the proof of equiv—len™eF

@fFPHA

∎

‡e —pply gl—im I to show it is equiv—lent to

R ∧ (¬R)W(P ∧ ¬R))
QU

B.0.3.3

After

Q

‡e prove the following equiv—len™e

P ) ≈ ƒtrong ixisten™e of P, efter Q

(Q ∧

@fFPIA

Proof. e™™ording to @QFQA
SA ≠ ∅ ≡ ∃i ≥ 0 (i = min({k ≥ 0 sk ⊫ Q}))
Q

∃i ≥ 0 (i = min({k ≥ 0 sk ⊫ Q}))

⇐⇒

∃i ≥ 0 si ⊫ Q
this is the de(nition of

QF gonjoining with v„v from @fFIIAD we get

Q ∧ (◻(¬Q) ∨

(Q ∧

( Q ∧ ◻(¬Q)) ∨ ( Q ∧
Q∧

(Q ∧

(Q ∧

P ))
(Q ∧

⇐⇒
P ))

P)

⇐⇒

P)

⇐⇒

„his (nishes the proof of equiv—len™eF

B.0.3.4

Between

Q

and

∎

R

‡e propose the following formul—

(Q ∧ ¬R ∧

R) ∧ ◻(Q ∧ ¬R → ¬(¬P )UR) ≈
ƒtrong ixisten™e of P, fetween Q —nd R @fFPPA

Proof. e™™ording to @QFRA
SBW

QR

≠ ∅ ≡ ∃m ≥ 0, ∃n (sm ⊫ (Q ∧ ¬R), n = min({k > m sk ⊫ R}))

QV

∃m ≥ 0, ∃n (sm ⊫ (Q ∧ ¬R), n = min({k > m sk ⊫ R})) ⇐⇒
∃m ≥ 0, ∃n > m (sm ⊫ (Q ∧ ¬R), sn ⊫ R)) ⇐⇒
∃m ≥ 0, ∃n ≥ m (sm ⊫ (Q ∧ ¬R), sn ⊫ R))
this is ex—™tly the de(nition of

R)F gonjoining with v„v from @fFIPAD we get

(Q ∧ ¬R ∧

R) ∧ ◻(Q ∧ ¬R → ¬(¬P )UR)

(Q ∧ ¬R ∧
„his (nishes the proof of equiv—len™eF

∎

‡e —pply gl—im I to show it is equiv—lent to

R) ∧ ◻(Q ∧ ¬R → (¬R)W(P ∧ ¬R))

(Q ∧ ¬R ∧

B.0.3.5

After

Q

until

R

‡e propose the following formul—

(Q ∧ ¬R) ∧ ◻(Q ∧ ¬R → ¬(¬P )WR) ≈
ƒtrong ixisten™e of P, efter Q until R

Proof. e™™ording to @QFSA
SAU

QR

SBW

QR

≠ ∅ ∨ (SAU

≠ ∅ ⇐⇒ SBW

QR

− SBW

QR

QR

≠ ∅ ∨ (SAU

QR

− SBW

QR

)≠∅

)≠∅ ≡

∃i ≥ 0, ∃j (si ⊫ (Q ∧ ¬R), j = min({k > i sk ⊫ R})) ∨
∃i ≥ 0, ∀j ≥ i (si ⊫ Q, sj ⊫ ¬R)
the ‚rƒ of the equiv—len™e holds i' the following holds

∃i ≥ 0, ∃j > i (si ⊫ (Q ∧ ¬R), sj ⊫ R) ∨ ∃i ≥ 0, ∀j ≥ i (si ⊫ Q, sj ⊫ ¬R)
∃i ≥ 0 (si ⊫ (Q ∧ ¬R), (∃j > i sj ⊫ R ∨ ∀j > i sj ⊫ ¬R))
∃i ≥ 0 si ⊫ (Q ∧ ¬R)
QW

this is the de(nition of
@fFPQA

(Q ∧ ¬R)
gonjoining with v„v from @fFIQAD we get

(Q ∧ ¬R) ∧ ◻(Q ∧ ¬R → ¬(¬P )WR)
„his (nishes the proof of equiv—len™eF

∎

‡e —pply gl—im P to show it is equiv—lent to

(Q ∧ ¬R) ∧ ◻(Q ∧ ¬R → (¬R)U(P ∧ ¬R))

B.0.4

Universality

…nivers—lly P  is the s—me —s e˜sen™e of ¬P F „herefore we reuse v„vs —nd proofs from
th—t se™tionF

B.0.5

B.0.5.1

Existence with Weak Scopes,

(Before

SW

R )W
¬(¬P )UR ≈ ixisten™e of P, @fefore R)W

@fFPRA

Proof. e™™ording to @QFIHA
ixisten™e of P, @fefore R)W ≡ ∀I ∈ SW , ∃n ∈ I sn ⊫ P
BR
it follows from @QFTA th—t

∀I ∈ SW , ∃n ∈ I sn ⊫ P ≡
BR
∀i ≥ 0 (i = min({k ≥ 0 sk ⊫ R})

RH

⇒ ∃n ∈ [0, i) sn ⊫ P )

the ‚rƒ of the equiv—len™e holds i' the following holds

∀i ≥ 0, ∃n ∈ [0, i) (si ⊫ R

⇒ sn ⊫ P )

⇐⇒

∀i ≥ 0, ∃n ∈ [0, i) (si ⊫ ¬R ∨ sn ⊫ P )

⇐⇒

¬(∃i ≥ 0, ∀n ∈ [0, i) (si ⊫ R ∧ sn ⊫ ¬P )
this is the de(nition of ¬(¬P )URF

∎

‡e —pply gl—im I to show it is equiv—lent to

(¬R)W(P ∧ ¬R)

B.0.5.2

(Between

Q

and

R )W

◻(Q → ¬(¬P )UR) ≈ ixisten™e of P, @fetween Q —nd R)W

@fFPSA

Proof. e™™ording to @QFIHA
ixisten™e of P, @fetween Q —nd R)W ≡ ∀I ∈ SW
BWQR , ∃n ∈ I sn ⊫ P
it follows from @QFUA th—t

∀I ∈ SW
BWQR , ∃n ∈ I sn ⊫ P ≡
∀i ≥ 0, ∀j ≥ 0 (si ⊫ Q, j = min({k ≥ i sk ⊫ R})

⇒
∃n ∈ [i, j) sn ⊫ P )

the ‚rƒ of the equiv—len™e holds i' the following holds

∀i ≥ 0, ∀j ≥ i, ∃n ∈ [i, j) (si ⊫ Q, sj ⊫ R
∀i ≥ 0, ∀j ≥ i, ∃n ∈ [i, j) (si ⊫ Q

⇒ sn ⊫ P )

⇒ (sj ⊫ ¬R ∨ sn ⊫ P ))

∀i ≥ 0 (si ⊫ Q

⇒ ∀j ≥ i, ∃n ∈ [i, j) (sj ⊫ ¬R ∨ sn ⊫ P ))

∀i ≥ 0 (si ⊫ Q

⇐⇒
⇐⇒

⇒ ¬(∃j ≥ i, ∀n ∈ [i, j) (sj ⊫ R, sn ⊫ ¬P )))

this is the de(nition of ◻(Q → ¬(¬P )UR)F

⇐⇒

∎
RI

‡e —pply gl—im I to show it is equiv—lent to

◻(Q → (¬R)W(P ∧ ¬R))

B.0.5.3

(After

Q

until

R )W

◻(Q → ¬(¬P )WR) ≈ ixisten™e of P, @efter Q until R)W

@fFPTA

Proof. e™™ording to @QFIHA
ixisten™e of P, @efter Q until R)W ≡ ∀I ∈ SW
AUQR , ∃n ∈ I sn ⊫ P
it follows from @QFVA th—t

∀I ∈ SW
AUQR , ∃n ∈ I sn ⊫ P ⇐⇒
(∀I ∈ SAU

QR

, ∃n ∈ I sn ⊫ P ) ∧ (∀I ∈ SW
BWQR , ∃n ∈ I sn ⊫ P )

in @fFIQA —nd @fFPVA we h—ve derived the ™orresponding v„vs

◻ (Q ∧ ¬R → ¬(¬P )WR) ∧ ◻(Q → ¬(¬P )UR)

⇐⇒

◻ ((Q ∧ ¬R → ¬(¬P )WR) ∧ (Q → ¬(¬P )UR))

⇐⇒

st is e—sy to see th—t ¬R term is redund—nt

◻ ((Q → ¬(¬P )WR) ∧ (Q → ¬(¬P )UR))

⇐⇒

◻ ((Q → (¬ ◻ (¬P ) ∧ ¬(¬P )UR)) ∧ (Q → ¬(¬P )UR))

⇐⇒

◻ (Q → (¬ ◻ (¬P ) ∧ ¬(¬P )UR))

⇐⇒

◻ (Q → ¬(¬P )WR)
„his proves the equiv—len™eF

∎

pin—llyD we —pply gl—im P to show

◻(Q → ¬(¬P )WR) ⇐⇒ ◻(Q → (¬R)U(P ∧ ¬R))

RP

B.0.6

Strong Existence with Weak Scopes,

SW

es in the ƒe™tion fFHFQD it is enough to derive the v„v for the ™—se of —n empty s™ope —nd
™onjoin this v„v with the one derived in ƒe™tion fFHFSF

B.0.6.1

(Before

R )W

R ∧ ¬(¬P )UR ≈ ƒtrong ixisten™e of P, @fefore R)W

@fFPUA

Proof. e™™ording to @QFTA
SW ≠ ∅ ≡ ∃i ≥ 0 (i = min({k ≥ 0 sk ⊫ R}))
B
R

—nd the ™orresponding v„v is

RF gonjoining with @fFPRA
R ∧ ¬(¬P )UR

this is our (n—l formul—F

∎

‡e —pply gl—im I to show it is equiv—lent to

R ∧ (¬R)W(P ∧ ¬R)

B.0.6.2

(Between

(Q ∧

Q

and

R )W

R) ∧ ◻(Q → ¬(¬P )UR) ≈ ixisten™e of P, @fetween Q —nd R)W

@fFPVA

Proof. e™™ording to @QFUA
SW
BW

QR

≠ ∅ ≡ ∃i ≥ 0, ∃j ≥ 0 (si ⊫ Q, j = min({k ≥ i sk ⊫ R}))

—nd the ™orresponding v„v is

(Q ∧

R)

@fFPWA

gonjoining with @fFPSA

(Q ∧

R) ∧ ◻(Q → ¬(¬P )UR)

this is our (n—l formul—F

∎
RQ

‡e —pply gl—im I to show it is equiv—lent to

(Q ∧

B.0.6.3

(After

(Q ∧ (¬R ∨

Q

until

R) ∧ ◻(Q → (¬R)W(P ∧ ¬R))

R )W

R)) ∧ ◻(Q → ¬(¬P )WR) ≈
ixisten™e of P, @efter Q until R)W

Proof. e™™ording to @QFVA
SW
AU

QR

≠ 0 ⇐⇒ SAU

QR

≠ 0 ∨ SW
BW

QR

≠0

it follows from @fFPQA —nd @fFPWA

(Q ∧ ¬R) ∨

(Q ∧

((Q ∧ ¬R) ∨ (Q ∧
(Q ∧ (¬R ∨

R)

⇐⇒

@fFQHA

R))

⇐⇒

@fFQIA
@fFQPA

R))

gonjoining with v„v from @fFPTAD we get

(Q ∧ (¬R ∨

R)) ∧ ◻(Q → ¬(¬P )WR)

„his (nishes the proof of equiv—len™eF

∎

pin—llyD we —pply gl—im P to show it is equiv—lent

(Q ∧ (¬R ∨

B.0.7

Precedence

B.0.8

R)) ∧ ◻(Q → (¬R)U(P ∧ ¬R))

Globally

(¬P )WS ≈ S €re™edes P D qlo˜—lly
RR

Proof. e™™ording to @QFIA —nd @QFISA
S €re™edes P D qlo˜—lly ≡ ∀n ∈ [0, ∞) (sn ⊫ P

⇒ ∃m ∈ [0, n] sm ⊫ S)

the vrƒ holds i'

∀n ≥ 0 (sn ⊫ ¬P ∨ ∃m ∈ [0, n] sm ⊫ S)

⇐⇒

∀n ≥ 0 (sn ⊫ (¬P ∨ S) ∨ ∃m ∈ [0, n) sm ⊫ S)

⇐⇒

¬(∃n ≥ 0 (sn ⊫ (P ∧ ¬S), ∀m ∈ [0, n) sm ⊫ ¬S))
this is the de(nition of ¬((¬S)U(P ∧ ¬S))F fy @fFPA in gl—im P

¬((¬S)U(P ∧ ¬S)) ⇐⇒ (¬P )WS
this (nishes the proof of equiv—len™eF

B.0.9

∎

Response

B.0.10

Globally

◻(P →

S) ≈ S ‚esponses to P D qlo˜—lly

Proof. e™™ording to @QFIA —nd @QFITA
S ‚esponses to P D qlo˜—lly ≡ ∀n ∈ [0, ∞) (sn ⊫ P
this is the de(nition of ◻(P →

S)F

⇒ ∃m ≥ n sm ⊫ S)
∎

RS

Appendix C
PROOFS OF NON EQUIVALENCE

C.1 Existence
R ∨ ¬(¬P )UR ≈ ixisten™e of P D fefore R
/

Proof. ƒuppose the initi—l st—te of our model is —n REst—te @s0 ⊫ RAF „he v„v formul— on
the vrƒ is TrueD howeverD the origin—l v„v formul— de(ned in ‘I“D (¬R)W(P ∧ ¬R)D is False
on this modelF

∎

◻(Q → ¬(¬P )UR) ≈ ixisten™e of P, fetween Q —nd R
/

Proof. ƒuppose the initi—l st—te of our model is — (Q ∧ R)Est—te —nd —ll other st—tes —re
(¬Q)Est—tesD iFeF (s0 ⊫ Q ∧ R) ∧ (∀i > 0 si ⊫ ¬Q)F „he v„v formul— on the vrƒ is FalseD
howeverD the origin—l formul— v„v de(ned in ‘I“D ◻(Q ∧ ¬R → ¬(¬P )UR)D is TrueF

∎

◻(Q → ¬(¬P )WR) ≈ ixisten™e of P, efter Q until R
/

Proof. ‡e reuse the ex—mple form the previous proofF

∎

C.2 Strong Existence
R ∧ ¬(¬P )UR ≈ ixisten™e of P D fefore R
/

Proof. ƒuppose our model is des™ri˜ed ˜y ∀i ≥ 0 si ⊫ (¬R ∧ ¬P )F „he v„v formul— on the
vrƒ is FalseD howeverD the origin—l v„v formul— de(ned in ‘I“D (¬R)W(P ∧ ¬R)D is True on
this modelF

∎

RT

(Q ∧
(Q ∧ ¬R ∧
(Q ∧

P ) ≈ ixisten™e of P D efter Q
/

R) ∧ ◻(Q ∧ ¬R → ¬(¬P )UR) ≈ ixisten™e of P D fetween Q —nd R
/
R) ∧ ◻(Q → ¬(¬P )UR) ≈ ixisten™e of P D fetween Q —nd R
/

(Q ∧ ¬R) ∧ ◻(Q ∧ ¬R → ¬(¬P )WR) ≈ ixisten™e of P D efter Q until R
/
(Q ∧ (¬R ∨

R)) ∧ ◻(Q → ¬(¬P )WR) ≈ ixisten™e of P D efter Q until R
/

Proof. por —ll (ve formul—s we use the ex—mpleD no QEst—te in the modelD ∀i ≥ 0 si ⊫ ¬QF
„he v„v formul—s on the vrƒs —re FalseD howeverD the origin—l v„v formul—s de(ned in ‘I“
—re True on this modelF

∎

RU

BIBLIOGRAPHY

RV

BIBLIOGRAPHY

‘I“

r—mid el—viD
qeorge evruninD
t—mes gor˜ettD
v—ur— hillonD
w—tt
hwyerD
—nd gorin—
€—s—re—nuD
Property pattern mappings for ltlD
httpXGGp—tternsFproje™tsF™isFksuFeduGdo™ument—tionGp—tternsGltlFshtmlF

‘P“

eF gim—ttiD iF gl—rkeD pF qiun™higli—D —nd wF ‚overiD Nusmv: a new symbolic model
checkerD sntern—tion—l tourn—l on ƒoftw—re „ools for „e™hnology „r—nsfer 2 @PHHHAD PHHHF

‘Q“

iF wF gl—rkeD iF eF imersonD —nd eF €F ƒistl—D Automatic verication of nite-state
concurrent systems using temporal logic specicationsD egw „r—nsF €rogr—mF v—ngF
ƒystF 8 @IWVTAD PRR!PTQF

‘R“

‚—™hel vF go˜leighD qeorge ƒF evruninD —nd vori eF gl—rkeD User guidance for creating
precise and accessible property specicationsD €ro™eedings of the IRth egw ƒsqƒyp„
intern—tion—l symposium on pound—tions of softw—re engineering @xew ‰orkD x‰D …ƒeAD
ƒsqƒyp„ 9HTGpƒiEIRD egwD PHHTD ppF PHV!PIVF

‘S“

t—mes gF gor˜ett —nd qeorge ƒF evruninD Using integer programming to verify general
safety and liveness propertiesD pormF wethods ƒystF hesF 6 @IWWSAD WU!IPQF

‘T“

w—tthew fF hwyerD qeorge ƒF evruninD —nd t—mes gF gor˜ettD Property specication
patterns for nite-state vericationD €ro™eedings of the se™ond workshop on porm—l
methods in softw—re pr—™ti™e @xew ‰orkD x‰D …ƒeAD pwƒ€ 9WVD egwD IWWVD ppF U!ISF

‘U“

w—tthew fF hwyerD qeorge ƒF evruninD —nd t—mes gF gor˜ettD Patterns in property
specications for nite-state vericationD €ro™eedings of the PIst sntern—tion—l gonferE
en™e on ƒoftw—re ingineering sgƒi9WWD IWWWF

‘V“

w—tthew fF hwyerD vori eF gl—rkeD t—mieson wF go˜leighD —nd qle˜ x—umovi™hD Flow
analysis for verifying properties of concurrent software systemsD egw „r—nsF ƒoftwF
ingF wethodolF 13 @PHHRAD QSW!RQHF

‘W“

iri™h q—mm—D ‚i™h—rd relmD ‚—lph tohnsonD —nd tohn †lissidesD Design patterns:
elements of reusable object-oriented softwareD eddisonE‡esley vongm—n €u˜lishing goFD
sn™FD fostonD weD …ƒeD IWWSF

‘IH“ vF q—r™i— —nd ƒF ‚o—™hD Model-checker-based testing of ltl specicationsD righ essur—n™e
ƒystems ingineering ƒymposiumD PHHUF reƒi 9HUF IHth siiiD PHHUD ppF RIU !RIVF
‘II“ qFtF rolzm—nnD The model checker spinD ƒoftw—re ingineeringD siii „r—ns—™tions on
23 @IWWUAD noF SD PUW !PWSF
‘IP“ exel v—n v—msweerdeD Formal specication: a roadmapD €ro™eedings of the gonferen™e
on „he puture of ƒoftw—re ingineering @xew ‰orkD x‰D …ƒeAD sgƒi 9HHD egwD PHHHD
ppF IRU!ISWF

RW

‘IQ“ wi™h vuis—D pr—n™h w—ri—ngel—D —nd snver—rdi €ierluigiD Market research for requirements analysis using linguistic toolsD ‚equirF ingF 9 @PHHRAD RH!STF
‘IR“ F w—nn— —nd eF €nueliD Temporal verication of reactive systems: safetyD „empor—l
veri(™—tion of re—™tive systems G oh—r w—nn—Y emir €nueliD ƒpringerD IWWSF
‘IS“ ‚—du w—tees™u —nd wih—el— ƒighire—nuD Ecient on-the-y model-checking for regular
alternation-free mu-calculusD ƒ™iF gomputF €rogr—mF 46 @PHHQAD PSS!PVIF
‘IT“ uenneth vF w™will—nD Symbolic model checkingD uluwer e™—demi™ €u˜lishersD xorwellD
weD …ƒeD IWWQF
‘IU“ ys™—r wondr—gónD enn F q—tesD —nd ƒteven ‚o—™hD Prospec: Support for elicitation
and formal specication of software propertiesD ile™troni™ xotes in „heoreti™—l gomE
puter ƒ™ien™e 89 @PHHQAD noF PD TU ! VVD ‚† 9PHHQD ‚unEtime †eri(™—tion @ƒ—tellite
‡orkshop of ge† 9HQAF
‘IV“ ‚o™™o he xi™ol— —nd prits ‡F †——ndr—gerD Action versus state based logics for transition
systemsD €ro™eedings of the vs„€ ƒpring ƒ™hool on „heoreti™—l gomputer ƒ™ien™eX
ƒem—nti™s of ƒystems of gon™urrent €ro™esses @vondonD …uAD ƒpringerE†erl—gD IWWHD
ppF RHU!RIWF
‘IW“ uurt wF ylender —nd veon tF ysterweilD Cecil: A sequencing constraint language for
automatic static analysis generationD siii „r—nsF ƒoftwF ingF 16 @IWWHAD PTV!PVHF
‘PH“ ‰F ƒF ‚—m—krishn—D €F wF welli—rEƒmithD vF iF woserD vF uF hillonD —nd qF uuttyD
Interval logics and their decision procedures: part i: an interval logicD „heorF gomputF
ĪiF 166 @IWWTAD I!RUF
‘PI“ ƒ—l—m—h ƒ—l—m—hD enn F q—tesD †l—dik ureinovi™hD —nd ƒteve ‚o—™hD Verication of
automatically generated pattern-based ltl specicationsD righEessur—n™e ƒystems ingiE
neeringD siii sntern—tion—l ƒymposium on 0 @PHHUAD QRI!QRVF
‘PP“ ƒ—l—m—h s˜r—him ƒ—l—m—hD Generating linear temporal logic formulas for complex
pattern-based specicationsD €hFhF thesisD …niversity of „ex—sD il €—soD „ex—sD PHHUF
‘PQ“ ‚—™hel vF ƒmithD qeorge ƒF evruninD vori eF gl—rkeD —nd veon tF ysterweilD Propel: an
approach supporting property elucidationD €ro™eedings of the PRth sntern—tion—l gonferE
en™e on ƒoftw—re ingineering @xew ‰orkD x‰D …ƒeAD sgƒi 9HPD egwD PHHPD ppF II!PIF
‘PR“ ‡illem †isserD gorin— ƒF €§s§re—nuD —nd ƒ—rfr—z uhurshidD Test input generation with
——
java pathnderD ƒsqƒyp„ ƒoftwF ingF xotes 29 @PHHRAD WU!IHUF

SH