🚀 go-pugleaf

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