🚀 go-pugleaf

In article <172o80INNk2k@iraul1.ira.uka.de> zundel@i10s7 (Armin Zundel) writes:
>Hello everyone! 
>
>after reading some papers about temporal logic I had some problems to
>decide when to use linear time logics and when to use branching time
>logics. I decided to read 
>
>"Sometimes" and "Not Never" revisited: On Branching versus Linear Time
>Temporal Logic 
>by E.a. Emerson and J.Y. Halpern.
>
>Now I'm even more confused. I just want so specify distributed systems.
>Can anyone tell me what real life properties can be specified with
>linear time logic and which can be specified in branching time logic. 


Unfortunately, the state of the art in formal specification is rather
primitive, and although there is no shortage sales pitches for various
specification methods, there is a marked shortage of worked non-trivial
examples to substantiate claims about which methods are better.

The branching/linear time temporal logic question is easy, however.
Branching time logics are technically more expressive than linear time
logics, but practically not very different. Essentially, linear time logics
consist of assertions about sequences of states, e.g. that every
state in the sequence satisfies a property or that some state in the
sequence satisfies the a property. One can consider each sequence to
record a particular execution trace of a program or device: with each
state being a snapshot of system properties at a discrete moment in time.
Branching time logics consist of assertions about trees of states. Each
tree can be considered to describe all possible execution paths of 
a program or device, with branches corresponding to moments where either
the program or its environment can change state in one of several different
ways which do not depend on the current state. For example, there
might be a branching point where a program receives input from the
environment --- of course, the contents of the input are not determined
by the state of the program. Each path in the tree is a sequence
which can be described using linear time logic, so it is possible to define
branching time logics simply by adding path quantifiers to a linear
time logic. For example, "Number_of_processes > 10 -> Eventually Fail"
is a linear time assertion, while:
  (Ex1)          There are states where Number_of_processes > 10
             AND Number_of_processes > 10 -> Eventually Fail
is a branching time assertion. Branching time is handy when we want to
describe what the environment can throw at us.
On the other hand, each sequence of states can be considered
to describe a path in a tree, and a language of sequences which is closed
under prefix is a description of a tree. So, while there is no linear
time logic assertion exactly equivalent to Ex1, one can write:

(Ex2)   Number_of_Processes =< 10 -> Enable("Start_new_process")
             AND Number_of_processes > 10 -> Eventually Fail

Esentially, you can encode the assertions about what branches can be taken
into a linear logic by introducing actions (as in TLA) or history variables
(as in hundreds of temporal logic variants).  Look at Pnueli's survey
article (see below) for examples of this second strategy.

If you really want to understand what's going on in temporal logics you
should read Kripke's paper on the semantics for modal logics and 
maybe Kroger's book on linear temporal logic. Much of what seems obscure
and mysterious in the temporal logics can be understood if you know
something about the original construction that Kripke did. His paper
is quite short and well worth the effort. On the other hand, if you
really want a useful method for specifying and verifying distributed
systems you should use modal functions not temporal logic (see, I told you
that there was no shortage of sales pitches in the field)

@article{Kripke  ,
author="Kripke, S. " ,
title=" Semantical Considerations on Modal Logic " , 
journal="Acta Philosophica Fennica" ,
volume=16 ,
pages={83-94} , year=1963 }

@book{Kroger  ,
author="Kroger, F. " , 
title="Temporal Logic of Programs" ,
series="EATCS Monographs on Theoretical
Computer Science" ,
publisher={Springer-Verlag} , year=1987 }


author={Victor Yodaiken},
title="Modal functions for concise representation of finite automata",
title="The Algebraic Feedback Product of Automata",
title="Verification of a Reliable Broadcast Algorithm",
[all available via anonymous ftp in pub/yodaiken on dime@cs.umass.edu]
[NOTE: I am offering a prize (not a very good one) to any authors who
 manage to specify and verify the Reliable Broadcast algorithm covered
 in the third paper by February 1 1993. Contestants from Oxford (in 
 timed CSP) are the only real contenders so far]


@incollection{Pnueli  ,
author="Pnueli, A. " ,
title="Applications of temporal logic to the specification and verification of
reactive systems: a survey of curent trends. " ,
booktitle="Current Trends in Concurrency" ,
editor="J.W. de Bakker" ,
series="Lecture Notes in Computer Science" ,
volume=224 ,
publisher="Springer-Verlag" ,
year=1985 
}

-- 


yodaiken@chelm.cs.umass.edu