TEMPORAL LOGIC - A TOOL FOR SVSTEM MODELING 
INFORMATICA 4/1988 
UDK 519.711.3 
Bogdan Dugonik 
Technical Faculty Maribor 
Abstract 
This paper presents a model for processes, that communicate by 
message-passing, and the use o-f temporal logic -for their 
description. The epeci-fication o-f process determines behaviour 
on its external ports, whence its internal behaviour is not 
signiflcant. Speci-Tications based on the model are compositional, 
that is, He get external behaviour o-f a system -from 
specifications o-f its components. In the introduction a process 
recorded Mith traces is presented. A model is shoMn that 
represents a process speci-f Ication by use o-f temporal logic. 
Temporal logic operators, examples o-f temporal assertions and 
some speci-f ications -for primitive and composed processes are 
given. 
Povzetek 
V Članku Je prikazan model za procese in mreže procesov, ki 
komunicirajo izklJuCno s prehajanjem sporoCil, ' in uporaba 
Časovne logike za njihov opis. Specifikacija procesa doloCa 
obnašanje na njegovih zunanjih priklJuCkih, dogajanje v njegovi 
notranjosti pa nas ne zanima. Opisi procesov so komponibilni, kar 
pomeni, da zunanje obnaSanJe mreže dobimo iz specifikacij njenih 
komponent. Pri tem prikrijemo njeno notranjo strukturo. V uvodu 
predstavimo zapis procesa s sledmi. Prikažemo tudi specifikacijo 
procesa in mreže procesov z uporabo Časovne logike. Opisani so 
operatorji Časovne logike, podanih Je nekaj primerov Časovnih 
izjav ter specifikacij enostavnih in sestavljenih procesov. 
Introduction 
This paper treats processes that c 
exclusivGly through message passlng. 
ara transmitted over input and outp 
Let us observe a process on its exter 
for a tirne, up to some moment. 
sequence of events. The sequence gi 
trace. The trace Is an Informat 
behaviour of the process up to that 
Traces are appropriate to descr 
termlnating processes. The model of a 
modular, it Is composed of some 
processes. In a system output 
processes are linked to Inputs o 
processes. Some input and output por 
linked. Nonlinked ports are external 
linked ports are Internal ports. 
nal 
We 
ves 
Ion 
omnunlcate 
Messages 
ut ports. 
ports 
get a 
us a 
.about 
moment. 
ibe only 
system is 
primitive 
ports of 
f another 
ts are not 
ports and 
A process is determlned by a ' set of posslble 
Input-output behavlours . The behaviour on a 
set of input and output ports is an inflnite 
seguence of observations ; 
6 = (t«i,Inai,Out«,,Rdai) , (ti ,Ini ,Outi ,Rdi ) , . . . 
t is a trace of events on input ports (input 
events) and events on output ports (output 
events). 
Events represent coromunication betveen 
processes. Communlcation can be synchronous or 
asynchronous. If communicatlon Is synchronous, 
a process cannot send a message until the 
recelving process is ready to read the message 
on his input ports. If communlcation is 
asynchronous, a process can send message on his 
output ports as soon as it is ready without 
havlng to wait for the recelving process. In 
čase of synchronous communlcation, input 
events present the data read by a process, and 
In čase of asynchronous communicatton, they 
present the data that have appeared on input 
ports. Output events in both ways of 
communlcation present messages sent by a 
process at its output ports. An event is 
recorded in the trace as a pair (x,k), vhere x 
Is a datum and k is the port name where the 
event has appeared. In and Out are boolean 
f.unctions. If they are true for Input - output 
ports, then we say the process is ready to 

22 
communicate. If logical values o 
port functlons are true, then 
process is ready to read on thos 
logical values of some output po 
are true, then we say the process 
send on those output ports . Rd 
number of messages read up to 
moment for each Input port . It 1 
thls number cannot be greater than 
of messages which have appeared 
port. We could describe the proce 
down ali posslble seguences 6/ wh 
and for more compllcated cases 
Impossible. Because of that , 
language which enables us to 
posslble behaviours of a process 
Temporal logici 
f some Input 
we say the 
e ports. If 
rt functlons 
Is ready to 
glves us the 
the observed 
s clear that 
the number 
on an Input 
ss by vrrlting 
Ich Is vague 
practically 
we apply a 
expreBS ali 
Temporal aasertlonai 
Formulas given below are examples of some 
temporal assertions. They are compounded by 
using temporal operators roentioned above. We 
Kili vrite A for conjunction, -i for negation, 
and T> for impllcation. 
n(u =f> O v) 
O D w 
a O w 
whenever u is true, it wlll 
eventually be folloued by v. 
eventually w vili become true 
and it will remaln thrue fotevett 
every instant is followed by 
some later instant, when w Is 
true, so w is true lndefinitely 
often. 
Natural languages are very expressive, but not 
predse, whereas formal languages are very 
predse but not so expressive. Formal languages 
have strictly defined semantlcs and syntax. It 
is impossible to say everythlng in them. But 
what you can say is unambiguous. 
Temporal logic is a formal language. It allovs 
us to make a temporal description of a process 
and also formal dealing of it. He present a 
model of temporal logic with infinlte seguence 
of States 
O v =*•((-! v)M u) - if v ever happens, its flrst 
occurrence is preceded by, or 
coincides with u. 
Assert 
meanin 
operat 
symbol 
functi 
divide 
symbol 
Global 
state 
values 
boolea 
tempor 
and un 
in the 
ions in 
g becau 
ors. La 
s: indi 
on and 
d into 
s and a 
Bymbols 
to stat 
from 
n opera 
al oper 
iversal 
system 
tem 
se 
ngua 
vidu 
pr 
two 
set 
kee 
e 
one 
tors 
ator 
guan 
pora 
they 
ge 
al 
edic 
su 
of g 
P th 
Loca 
sta 
s . 
tif 1 
1 logi 
incl 
employ 
varlab 
ate s 
bsets 
lobal 
ir va 
1 symb 
te to 
classl 
Existe 
catlon 
c have 
ude som 
I set 
les and 
ymbolB. 
a set 
Byn)bols. 
lues unc 
ols can 
anothe 
cal ope 
nce qua 
are al 
1 temporal 
I temporal 
of basic 
constants, 
These are 
of local 
hanged from 
vary their 
r. We use 
rators and 
ntifIcation 
so included 
The operators o-f temporal logtct 
By w we denote a term or a formula that may 
contain some temporal operators. 
- temporal operator "always": 
• w means; w is true in this moment and will 
be true forever. 
- temporal operator "eventually": 
O w means! w wlll be true at least in one of 
folloving moments. 
- temporal operator "until"i 
Hi ti W2 means : Wi is contlnually true 
until Wa, becomes true, and wa does Indeed 
become true. 
We choose some fixed referenc 
reference moment when interpre 
assertion. It tells us, wha 
reference moment, i.e. nov, 
happen in the future of it. I 
about what happened before. In 
Si,Sz,.. let us urite 6 
vhere <Si is an observatlon in b 
observation can be treated 
Usually, a state of a process 
values of variables of the proč 
observation (Si is a state, wh 
hlstory of process up to a cu 
its trace ti. Specification 
signifies hov this process beh 
model we vrite process specifi 
form of temporal assertions. 
The specification of the system 
<P> R , vhere R is an asserti 
temporal logic. Specification 
each behaviour of system P sati 
R. <P> R is external specif 
speclfies behaviour on P's 
System specification is a 
component assertions. 
specification is obtained by 
syBtem. 
The proof system for speclfic 
rules for temporal logic, rule 
description of the domain of va 
designlng a system, a set of s 
vith their predse specificatio 
vhich define the behaviour 
Specification defines tvo ki 
properties: safety and livena 
safety specification asserts, 
may do, and llveness specifi 
vhat it must do.We vili give s 
speclfications. 
moment named 
ting a temporal 
t holds at the 
and vhat vili 
t says nothing 
stead of G ' ms, 
<S»,Si ,62, • . 
ehaviour (S . An 
as a state. 
reflects current 
ess. Hence, an 
ich involves the 
rrent moment In 
of a process 
aves. For thls 
catlons In the 
P has the form 
on, vrittan in 
<P> R Is reads 
sfies assertion 
ication, if R 
external ports. 
conjunction of 
The external 
using a proof 
ations includes 
s regarding the 
lues, rules for 
ystem components 
ns, and axioms 
of ths systen. 
nds of process 
ss. Infornally, 
vhat the process 
cation asserts, 
orne examples of 
First, ve shov hov certain ports of a process 
can be disabled, discarded from connunlcatlon 
by using negation operator -i vith In or Out 
function. 
In the specification belov 
output port bi are disabled. 
input port Bi 
Input al can 
and 
not 
read the data, and bi can not send the data. 
- temporal operator "unless": 
Hi M Ha means: vi is continually true or 
there is a moment, when va is true and up 
to the moment vi is continually true. 
- temporal operator "neKt": 
o meansi v vili be true in next moment. 
< C > D -1 In(ai ) A Out(bi) 
Nov, let us asBume that communlcation is 
asynchronouB. We vili vrite external 
specifications of processes. That is, we vili 
specify a process only by means of lengths of 
ports' traces, vithout using In, Out and Rd. 
By Ibl ve denote the length of trace on port b. 
bGc means, that seguence b Is a preflx of 

23 
Bequence c. First exaitiple belcu (flg.l.) glves 
a process wlth input port k and output port 1. 
The process reads six values on input k and 
writes them on output 1 leaving out tha first 
two values. 
flg.l. Process 
port 1. 
with input port k and output 
< A > D 1 E [ k(2),k(3),k(4),k(5) ] 
A ( lil = 0 Jf Ikl žs 3) 
A (O |k| = 3 ={> O lil = i) 
A (O |k| =4 ={> O lil = 2) 
A (O |k| = 5 * O lil = 3) 
A (O |k| ^6 =t> O lil = 4) 
The first line is safety specificatlon. It 
Indicates that at most four values may occur 
on the output port, which will be read on input 
port k. The second conjunct Indicates that the 
length of the output trace is zero, unless the 
length of input trace is three. The third 
conjunct and those foHowing reguire the 
length of the output trace to be increased by 
one as soon the length of the input trace is 
increased. 
Second exainple (fig. 2) is a process with two 
inputs and one output. It reads one value on j 
and one value on k. Then it writes first the 
value on the output 1 from input k, and later 
the value from input j. 
Fig.2. A process named B with two inputs 
one output 
and 
< B > a 1 E [ k(0),d(0) ] 
A ( O |k| = 1 =t> O lil = 1 ) 
A ( 0( Ijl = 1 A Ikl ^ 1) =r- D lil 2) 
Finally, we present 
of component process 
and B have one input 
C two input^s and one 
llnked as shown in 
one value on input 
output C. Process B r 
and wrltes it once on 
values on its input 
output e as foll6wsi 
d, then both values 
an asynchronous network P 
es A,B and C. Components A 
and one output, component 
output. Components are 
figure 3. Process A reads 
a and writes it twice on 
eads one value on input b 
output d. Process C reads 
, then writes them on 
first a value from input 
from input c. 
0; 
bi 
R 
B 
Q 
,. _b__ 
r; 
d r— 
•\ 
/ 
/ 
p 
C 
"1 
i 
!e 
1 
1 
i 
3 
Fig.3. Process P with visible and hldden 
internal structure. 
First, specifications for each components are 
given: 
< A > a C C [ a(0),a(0) ] 
A ( O |a| ^ 1 * O D |c| =2) 
<B> DdECbCB)] 
A. ( O Ibl = 1 * O Q Idi = 1) 
< C > D e E [ d(0),c(0) ,c(l) ] 
A ( O Id I i 1 =t O le I = 1) 
A ( O ( Icl = 1 A Idi ^ 1) • ( O lel = 2) 
A ( O ( Icl = 2 A Idi Si 1) * ( O |e| = 3) 
External specification of P is obtained from 
conjunction of component specifications by 
using proof rules. 
< P > De E [ b(0), a(0), a(0) ] 
A ( O |b| Ž! 1 * O lel = 1 ) 
A ( O ( |a| ži 1 A Ibl i 1) =t> O D |e| = 3 ) 
It tells us how the system behaves on its 
external ports. 
Conclugjon 
We presented a model for processes which ušes 
temporal logic as one of existing formal 
languages for specifying them. The benefit of 
temporal logic is its ability of describing 
temporal behaviour of processes. 
Specifications can be short and so expresslve, 
that they need no extra comments. Troubles 
arlse, If we uant to set the exact tirne, 
because in the model we can express ourselves 
only qualitatlvely about the tirne of 
events. 

24 
Re-fTencest 
[1] Dugonik B., Modeliranje procesov, 
diplomsko delo, Tehnifika fakulteta v 
Mariboru, 1987 
[2] Hoare C.A.R., Communicatlng Seguential 
Processes , Prentice - Hali International, 
Ltd., London 1985. 
[3] Kapus T., časovna logika in mreže 
procesov, diplomsko delo. Tehniška 
fakulteta v Mariboru, 1987 
[4] Lamport L., What Good is Temporal Logic ?, 
Information Processing (1983),pp. 667-668 
[5] Manna Z.,Pnueli A., Veriflcatlon of 
Concurrent Programs, Part Ii The temporal 
Framework; Tahnical Report STAN-SC-81-836, 
Standford Universitj', June 1981. 
[6] Nguyen V., Oemers A., Grles D., Owicki S., 
A model and temporal proof system for 
netvorks of processes, Distributed 
Computing (1986), 1, pp. 7-25.