NetNews Usenet Archive 1992 #18/NN_1992_18.iso/spool/comp/specific/382

Text File | 1992-08-21 | 3.4 KB | 78 lines

Newsgroups: comp.specification
Path: sparky!uunet!decwrl!deccrl!news.crl.dec.com!pa.dec.com!src.dec.com!src.dec.com!horning
From: [e-mail]
Subject: Re: Linear and Branching Time Temporal Logic
Message-ID: <[e-mail]>
Followup-To: [e-mail]
Keywords: TLA, Temporal Logic of Actions
Sender: [e-mail] (News)
Organization: DEC Systems Research Center
References:  <[e-mail]>
Date: Fri, 21 Aug 92 23:05:56 GMT
Lines: 64

In article <[e-mail]>, zundel@i10s7 (Armin Zundel) writes:

|> 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.


Dear Mr. Zundel,

Your message will probably stimulate lots of philosophical debate among
theoreticians.  Here's my view, based on my experience actually
verifying and specifying concurrent systems.

The simplest linear-time logic, with just state predicates and the Box
operator, can express the intuitive concepts "always" and "eventually".
The analogous branching-time logic, with just state predicates and the
Box operator, can express the intuitive concepts "always" and
"possibly".  Since "eventually" is a pretty important concept, I don't
think anyone advocates the use of such a simple branching-time logic.
I believe that the branching-time logics that people propose allow one
to express both "eventually" and "possibly".  I have never wanted to
write a specification such as

  "If the user enters an input, then it is possible for the system to
   produce the correct answer."

so the ability to express possibility is of no interest to me.
Therefore, I've found linear-time temporal logic adequately expressive,
and have no need for complicated branching-time logics.

Unfortunately, a simple linear-time logic with just Box and state
predicates isn't expressive enough.  You need something more.  The
traditional approach has been to add more powerful temporal operators,
and to write a specification as a list of temporal-logic formulas.
However, my experience is that, for systems of any complexity, such
specifications become incomprehensible and are usually wrong.  The only
practical specification methods are ones that write a specification as
an abstract program.  (Petri nets and CCS formulas are examples of
abstract programs.) However, programs aren't as mathematically simple
or as amenable to manipulation and reasoning as logical formulas are.

My approach is to use just the Box operator, but to generalize from
simple state predicates to predicates on pairs of states.  With this
logic, which I call TLA (the Temporal Logic of Actions), it is easy to
write abstract programs as logical formulas.  For example, one could
express the program that starts with x equal to 0 and repeatedly
increments x by one as

   (x = 0)  /\  [](x' = x+1)

(where /\ denotes conjunction and [] denotes Box).  TLA is described in
a research report that I am sending you in a separate message.

Leslie Lamport