<< Chapter < Page Chapter >> Page >
Strong Until
i ( U ) iff k i . ( k j . ( i j < k j ) ) .

Decide whether each is true or false for following trace : (This is the same trace seen earlier .)

A timing diagram for a trace , and propositions p and q .
  • 0 ( q U p )
  • 2 ( q U p )
  • 5 ( q U p )
  • 9 ( q U p )
  • True. q is true in 0 , and it doesn't take long before p becomes true in 1 .
  • False.Starting at 2 , we see that p doesn't become true until 5 , yet q doesn't stay true that long.
  • Very true, since p is already true in 5 . (In the definition, take k =5; then there are not any j to even need to worry about.)
  • False. Since p is from 9 onward, we can't even find a ( k 9 ) such that k p . However, it is true that 9 ( q W p ) .

Give the formal semantics of Weak Until (in the same way we have given semantics for , , and Strong Until).

i ( W ) iff ( j i . j ( k i . k i j < k . j ) )

Weak Until could be omitted from our core set of LTL connectives, since it can be defined in terms of the remaining connectives.Provide such a definition.That is, give an LTL formula equivalent to ( W ) .

Here are three equivalent definitions. The first follows directly from the above exercise .

  • ( W ) ( ( U ) )
  • ( W ) ( ( U ) )
  • ( W ) ( U ( ) )

Any logic that includes temporal connectives is a temporal logic . More specifically, this is Linear Temporal Logic ( LTL ). The ``linear'' part of this name means thatwe are looking only at individual traces, rather than making formulas that discussall possible traces of a program. After all, a single program can result in many possible traces.An LTL formula does not allow us to say, for example, that a property holds in all possible executions of the program.However, SPIN overcomes some limitations by essentially testing an LTL formula against all possible traces.Will will return to SPIN in the next section .

In summary, the syntax used in SPIN is given by the following grammar.

Spin's grammar for ltl formulas
ltl ::= atom
| (ltl binop ltl)
| unop ltl
| (ltl)
unop ::= [] ``Always''
| <> ``Eventually''
| ! ``Not''
binop ::= U ``Strong Until''
| W ``Weak Until''
| && ``And''
| || ``Or''
atom ::= true
| false
| name #define 'd identifiers
Some presentations of LTL use a box or ``G'' (Globally) for Always,and use a diamond or ``F'' for Eventually. Confusingly, some use ``U'' for Weak Until.Also, some include additional connectives like ``X'' (Next),which cannot be defined in terms of those given.

Do we really need a whole new logic?

We could use regular ol' first-order logic as our formal language for specifying temporal properties.We'd do this by adding an explicit time index to each proposition in Prop , turning it into a unary relation.For example, instead of considering Philosopher_B_has_fork in state 17, we'd instead write Philosopher_B_has_fork ( 17 ) , and so on.

This approach, though, quickly becomes cumbersome. Consider the everyday concept ``Someday, X will happen''.We have to go through some contortions to shoehorn this concept into first-order logic:``There exists a day d , such that d is today or later, and X will happen on d ''. Quite a mouthful forwhat is about the simplest temporal concept possible!

Get Jobilize Job Search Mobile App in your pocket Now!

Get it on Google Play Download on the App Store Now




Source:  OpenStax, Model checking concurrent programs. OpenStax CNX. Oct 27, 2005 Download for free at http://cnx.org/content/col10294/1.3
Google Play and the Google Play logo are trademarks of Google Inc.

Notification Switch

Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?

Ask