🚀 go-pugleaf

In article <172o80INNk2k@iraul1.ira.uka.de>, 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

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

A brief summary from what I have gleaned of temporal/tense logics.

Linear:

	+ describe behaviours of individual histories (functions of time)
	+ corresponds to use of a function
		TIME --> STATE/EVENT
	  in classical predicate calculus
	+ good for describing a class of behaviours which are acceptable
	- difficult to specify required alternative behaviours
		e.g. both the bzzt and spht events must be available

Branching:

	+ describes collections of histories (relations of time)
	+ in classical predicat calculus corresponds to use of a 
	  uniquely identified set of time stamped observations
		(ID --> TIME cross STATE/EVENT)
	  with a casality thread (or accessibility or time-branching relation)
		(ID <--> ID)
	  which determines the allowed futures for each time stamped
	  observation.
	  The usual special case is
		TIMETREE ::= STATE/EVENT \cross listof TIMETREE 
	+ good for describing a range of reuired alternative behaviours

Branching time is linear time + possibility. That is linear time
discusses the properties of a single observation of a system, whilst
branching time discusses the properties of all the possible observations
of a system.

A simple branching time logic which brings this out has the following
modalities:

	predicate - true of this time and this observation
	F - will occur sometime in the future
	G - will always be the case in the future
	<> - will occur in some observation of the system
	[] - will occur in every observation of the system

This makes all the concerns orthogonal in the language.

E.g.
	both the bzzt and spht events must be available now
		<> bzzt \land <> spht

	always both the bzzt and spht events must be available
		G(<> bzzt \land <> spht)

	eventually both the bzzt and spht events must be available
		F(<> bzzt \land <> spht)

	(necessarily) both the bzzt and spht events must eventually be available
		[]F bzzt \land []F spht

The usual branching time sometime is then <>F, the usual always []G.
--
When soldiers form lines or hollow squares, you call it reason.
When wild geese in flight take the form of a letter V, you say instinct.
When the homogeneous atoms of a mineral arrange themselves into shapes
mathematically perfect you have nothing to say. You have not even invented a name to conceal your heroic unreason."

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