0.5 Using temporal logic to specify properties (Page 6/11)

Model checking concurrent Page 6 / 11

As a more complicated variation, we generally want to match requests and their servicing. For example, what if there are tworequests, $r_{1}$ and $r_{2}$ , arriving in that order?In a particular context, do we expect that there are also exactly two servicings, $s_{1}$ and $s_{2}$ ? If so, do we also expect them in that order?

As a partial solution, how can we express ``whenever $r_{1}$ , $s_{1}$ will happen before $s_{2}$ ''?

If we are also requiring that $s_{2}$ indeed actually happen, then we can use the following: $□ ((r_{1} ◇ s_{2}) (s_{2} U s_{1}))$ .

Note that since LTL does not have quantifiers (like and) we cannot use variable indexing in our formulas.In other words, we can't talk about $r_{i}$ and $s_{j}$ , but instead, must always refer to specific variables like $r_{1}$ and $s_{2}$ .

From these examples and the ones following, we can see that English is typically too ambiguous. To get the appropriatelogic formula, we need to go back to the original problem and determine what was truly meant.Formalizing your specifications into temporal logic gives you the opportunity to closely examine what those specificationsreally should be.

Given a formula, try to understand it by translating it into English. Providing sample timelines that satisfy the formulais also quite helpful.

Describe the meaning of $□ ◇ p$ in words and a timeline.

Literally, we can simply say ``always, eventually $p$ ''. While that phrase is fairly common among logicians, it's not very natural ormeaningful to most people. A clearer, but more long-winded, equivalent is``at any point in time, $p$ will happen in the future''.

More concise, though, is `` $p$ happens infinitely often''. To understand that, consider a timeline. In words, at any time $t_{0}$ , $p$ will happen sometime in the future; call that time $t_{1}$ . And at moment $t_{1}$ +1, $p$ will happen sometime in the future; call that $t_{2}$ . Repeat forever.

The beginning of a trace where

p

happens infinitely often.

Describe the meaning of $□ (q □ p)$ in words and a timeline.

Again, a literal translation is ``always, if q then always not p''.Correct, but a bit more idiomatic-English would be ``whenever q, then forever not p'' or``Once q, p is forever false''.

The beginning of a trace satisfying the property.

A railroad wants to make a new controller for single-track railroad crossings.Naturally, they don't want any accidents with cars at the crossing, so they want to verify their controller.Their propositions $Prop$ include $train_is_approaching$ , $train_is_crossing$ , $light_is_flashing$ , and $gate_is_down$ .

Brainstorming: Using natural English, what are some propertieswe'd like to have true? Feel free to use words like ``always'', ``eventually'',``while'', and ``until''. You may add new propositions to $Prop$ , if you think it's appropriate.

For each, feel free to demonstrate that the one property is not sufficient:give a trace which satisfies the property but is either unacceptable or unrealistic.(For instance, ``the gate is always down'' is safe but unacceptable;``a train is always crossing'' is unrealistic since there aren't infinite trains.)

We can think of lots of examples, such as these.

Whenever a train passing, the gate is down.
If a train is approaching or passing, then the light is flashing.
If the gate is up and the light is not flashing, then no train is passing or approaching.
If a train is approaching, the gate will be down before the train passes.
If a train has finished passing, then later the gate will be up.
The gate will be up infinitely many times.
If a train is approaching, then it will be passing, and later itwill be done passing with no train approaching. (Thus, trains aren't infinitely long, and thereare gaps between the trains.)

<< Chapter < Page Page > Chapter >>

Read also:

Get Jobilize Job Search Mobile App in your pocket Now!

100% Free Mobile Applications
Receive real-time job alerts and never miss the right job again

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

	Anthropology Marriage Family Household By Richley Crapo Start Assignment
	2 Microeconomics 02 Choice in a World of Scarcity By OpenStax Start Flashcards
	PE Power Enigeering Safety By Gerr Zen Start Quiz
	Social Dances 1 By Marion Cabalfin Start Test
	College physics By OpenStax Read Online Course
	Cardiac Electrophysiology Basic 2 By Mistry Bhavesh Start Test
	Real Estate Finance By Mldelatte Start Quiz
	Business fundamentals By OpenStax Read Online Course
	Anthropology Economic System By Richley Crapo Start Assignment
	17 AP Key Terms 17 Endocrine System By OpenStax Start Key Terms