Skip to content Skip to navigation

OpenStax-CNX

You are here: Home » Content » Using Temporal Logic to Specify Properties: Homework Exercises

Navigation

Lenses

What is a lens?

Definition of a lens

Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

Who can create a lens?

Any individual member, a community, or a respected organization.

What are tags? tag icon

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

This content is ...

Affiliated with (What does "Affiliated with" mean?)

This content is either by members of the organizations listed or about topics related to the organizations listed. Click each link to see a list of all content affiliated with the organization.
  • Rice Digital Scholarship

    This module is included in aLens by: Digital Scholarship at Rice UniversityAs a part of collection: "Model Checking Concurrent Programs"

    Click the "Rice Digital Scholarship" link to see all content affiliated with them.

Also in these lenses

  • eScience, eResearch and Computational Problem Solving

    This module is included inLens: eScience, eResearch and Computational Problem Solving
    By: Jan E. OdegardAs a part of collection: "Model Checking Concurrent Programs"

    Click the "eScience, eResearch and Computational Problem Solving" link to see all content selected in this lens.

Recently Viewed

This feature requires Javascript to be enabled.
 

Using Temporal Logic to Specify Properties: Homework Exercises

Module by: John Greiner, Ian Barland, Moshe Vardi. E-mail the authors

Exercise 1

Give an English translation of the following LTL formulae. Try to give a natural wording for each, not just a transliteration of the logical operators.

  1. ( r (pUr))( r (pUr))
  2. (q ¬p ) (q ¬p )

Solution

  1. ``pp is true before rr.''
  2. ``pp is false after qq.''

Exercise 2

In the following, give an LTL formula that formalizes the given English wording. If the English is subject to any ambiguity, as it frequently is, describe how you are disambiguating it, and why.

  1. ``pp is true.''
  2. ``pp becomes true before rr.''
    • ``pp will happen at most once.''
    • ``pp will happen at most twice.''
  3. ``The light always blinks.'' Use the following proposition: pp = the light is on.
  4. ``The lights of a traffic signal always light in the following sequence: green, yellow, red, and back to green, etc., with exactly one light on at any time.'' ¶ Use the following propositions: gg = the green light is on, yy = the yellow light is on, and rr = the red light is on.

Solution

  1. This looks so simple and obvious, right? Unfortunately, it is ambiguous. The simple answer, pp, says it's true right now. But, the likelier intended meaning is that it's always true, pp.
  2. This can be reworded as ``pp becomes true while rr is still false.'' (¬rW(p¬r))(¬rW(p¬r))
  3. The version of LTL we use cannot capture the notion of something being true for exactly one state. Instead, we must instead think in terms of something being true for ``a while''. Using that idea, we'll reword the original English into more explicit, long-winded forms. ¶ ``pp will happen at most once'' becomes ``pp is false for a while, then it may become true for a while, then it may become false forever.'' It LTL, that can be written as (¬pW(pW ¬p ))(¬pW(pW ¬p )). ¶ Repeating that pattern, ``pp will happen at most twice'' becomes (¬pW(pW(¬pW(pW ¬p ))))(¬pW(pW(¬pW(pW ¬p )))).
  4. Here are three progressively simpler solutions which are equivalent.
    • ((p¬p)(¬pp)) ((p¬p)(¬pp))
    • ( (pU¬p) (¬pUp) )( (pU¬p) (¬pUp) )
    • ( p ¬p )( p ¬p )
  5. There are many ways to write this, but here's one. It states that whenever the green light is on, no other light is on, and it will stay on until the yellow one is on. Note that this implies the red light won't come on before the yellow one. What happens when the other lights are on is entirely parallel. Finally, at least one light is on. ¶ ((g((¬y¬r)(gUy)))(y((¬r¬g)(yUr)))(r((¬g¬y)(rUy)))(gyr)) ((g((¬y¬r)(gUy)))(y((¬r¬g)(yUr)))(r((¬g¬y)(rUy)))(gyr))

Exercise 3

Recall the Dining Philosophers Problem from the previous homework. Using temporal logic, formally specify the following desired properties of solutions to the D.P. Problem. Use the following logic variables, where 0 i < N 0 i < N :

  • l i l i : Philosopher ii has his/her left fork.
  • r i r i : Philosopher ii has his/her left fork.

For each question, your answer should cover exactly the given condition -- nothing more or less. You may assume N=3 N 3 .

  1. No fork is ever claimed to be held by two philosophers simultaneously.
  2. Philosopher ii gets to eat (at least once).
  3. Each philosopher gets to eat infinitely often.
  4. The philosophers don't deadlock. (The main difficulty is to conceptualize and restate ``deadlock'' within this specific model in terms of the available logic variables.) ¶ You may assume philosophers pick up two forks in some order, eat, and drop both forks.
  5. The philosophers don't deadlock. (The main difficulty is to conceptualize and restate ``deadlock'' within this specific model in terms of the available logic variables.) ¶ You may not assume philosophers pick up two forks in some order, eat, and drop both forks. For example, one might pick up a single fork and then drop it. Or, the philosophers might be lazy and never pick up a fork.
  6. Describe a D.P. Problem run in which philosophers don't deadlock, but it is not the case that each philosopher gets to eat infinitely often.

Solution

  1. (¬ ( l 0 r 2 ) ¬ ( l 1 r 0 ) ¬ ( l 2 r 1 ) ) (¬ ( l 0 r 2 ) ¬ ( l 1 r 0 ) ¬ ( l 2 r 1 ) )
  2. ( l i r i ) ( l i r i )
  3. ( ( l 0 r 0 ) ( l 1 r 1 ) ( l 2 r 2 ) )( ( l 0 r 0 ) ( l 1 r 1 ) ( l 2 r 2 ) )
  4. Here are two solutions.
    • (¬ ( l 0 l 1 l 2 ) ¬ ( r 0 r 1 r 2 ) ) (¬ ( l 0 l 1 l 2 ) ¬ ( r 0 r 1 r 2 ) )
    • (( l 0 r 0 )( l 1 r 1 )( l 2 r 2 )) (( l 0 r 0 )( l 1 r 1 )( l 2 r 2 ))
  5. This simply says that it never gets stuck in one particular fork configuration. There would be many if statements, one per configuration, and this is abbreviated. ¶ ((( l 0 l 1 l 2 ) ¬ ( l 0 l 1 l 2 ) )((¬ l 0 l 1 l 2 ¬ r 2 ) ¬ (¬ l 0 l 1 l 2 ¬ r 2 ) )) ((( l 0 l 1 l 2 ) ¬ ( l 0 l 1 l 2 ) )((¬ l 0 l 1 l 2 ¬ r 2 ) ¬ (¬ l 0 l 1 l 2 ¬ r 2 ) ))
  6. There are many possibilities. One is where philosopher 0 repeatedly eats, grabbing the forks so quickly that neither other philosopher has a chance to grab one that is shared with him.

Exercise 4

They following algorithm is an attempt to implement mutual exclusion for two processes. Here, each process is willing to defer to the other. (It also introduces Promela's goto, which lets you branch to a label; this is an alternate way of implementing loops and other control flow.)

Verify whether the algorithm is correct or not.

  • Verify using SPIN's built-in checks, without using temporal logic.
  • Verify using temporal logic.
  • If it is incorrect, find a shortest possible trace when it fails.


 1  int x, y, z;
 2
 3  active[2] proctype user()
 4  {
 5    int me = _pid+1;                            /* me is 1 or 2. */
 6
 7   L1:
 8    x = me;
 9    if
10    :: (y != 0 && y != me) -> goto L1   /* Try again. */
11    :: (y == 0 || y == me)                      /* Continue...  */
12    fi;
13
14    z = me;
15    if
16    :: (x != me) -> goto L1                     /* Try again. */
17    :: (x == me)                                /* Continue... */
18    fi;
19
20    y = me;
21    if
22    :: (z != me) -> goto L1                     /* Try again. */
23    :: (z == me)                                /* Continue... */
24    fi;
25
26    /* Entering critical section. */
27    /* ... */
28
29    /* Leaving critical section. */
30  }
	

Solution

As usual, we must check that no more than one process is in the critical section at a time. We can our usual code


  in_crit++;
  assert(in_crit == 1);
  in_crit--;
          
and declaring in_crit global. This code passes verification, but warns us that this code isn't necessarily even executed!

For a critical section protocol to be valid, it must also guarantee that each process eventually enters the critical section. Since the gotos create a control flow loop, we can check this by looking for non-progress cycles, labeling the critical section as progress.

Figure 1: The shortest counter-example trace. For brevity, the local values of me are not shown, since they cannot vary.
Figure 1 (mutex_failed_trace.png)

Using temporal logic, we can create a formula that describe our desired behavior: ``Eventually, each process gets to the critical section, but not both at the same time.'' One such formula is ( p q ¬ (pq) )( p q ¬ (pq) ) where we define


#define p (user[0]@crit)
#define q (user[1]@crit)
          
and define the label crit in the critical section.

This is a Promela version of an algorithm once recommended by a major computer manufacturer. As you can see, like many other mutual exclusion algorithms that have been proposed, it is flawed.

Exercise 5

The following is pseudocode for an attempt to implement critical sections for n processes. It is based on the idea that processes take numbers, and the one with the lowest number proceeds next. This algorithm has one small flaw. Your task is to find and fix the flaw. In particular, show the following steps of this process.

  1. Implement this algorithm in Promela, and show the resulting code. Include any code added for verification purposes, although that is counts towards the next problem's score.
  2. Show the use(s) of SPIN to verify that there is a flaw and to determine what the flaw is. Briefly describe the flaw.
  3. Fix the flaw in the code, and show either the fix or the resulting code. Again, include any code added for the next problem's verification.
  4. Show the use(s) of SPIN to verify your final implementation.

Hints: First, do not radically change the algorithm. There is a straightforward solution that only changes/adds a line or two. Second, do not overly serialize the code. Since the entry protocol's for loop is already serialized, this really means that each each process should be able to calculate max concurrently.

  • Shared variable declarations.
    
    /* Is Pi choosing a number? */
    boolean       choosing[n];
    
    /* Pi's number, or 0 if Pi has none. */
    unsigned int  number[n];
               
  • Global initialization. Occurs once, before any process attempts to enter its critical section.
    
    /* No process has a number. */
    for all j ∈ {0,…,n-1}
       number[j] = 0;
               
  • Critical section entry protocol, for process i. I.e., each process has the following code immediately before its critical section. ¶
    
    /* Choose Pi's number. */
    choosing[i] = true;
    number[i]   = max(number[0],number[1],…,number[n-1]) + 1;
    choosing[i] = false;
    
    /* For all other processes, … */
    for all j ∈ {0,…,i-1, i+1,…,n-1} in some serial order
        /* Wait if the other process is currently choosing. */
        while (choosing[j]) /* nothing */ ;
    
        /* Wait if the other process has a number and comes ahead of us. */
        if ((number[j] > 0) &&
            (number[j] < number[i]))
           while (number[j] > 0) /* nothing */ ;
               
    Note that, because of the if's test, it is equivalent to allow j to get the value i in this loop, as well. Although less intuitive, that simplifies the loop.
  • Critical section exit protocol, for process i. I.e., each process has the following code immediately after its critical section.
    
    /* Clear Pi's number. */
    number[i] = 0;
               

Solution

The problem with the given code is that the concurrent max computations does not necessarily result in each element of number[] being unique. Uniqueness is assumed by the following conditional to prioritize the processes:


    if ((number[j] > 0) &&
        (number[j] < number[i]))
       

One of the hints precludes changing the max calculation to produce uniqueness. So, we need a way to prioritize processes when they receive the same number. This is most easily accomplished by using their process IDs:


    if ((number[j] > 0) &&
        ((number[j] < number[i]) ||
         ((number[j] == number[i]) && j<i)))
       

Of course, …j>i… is also fine.

Content actions

Download module as:

Add module to:

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

Definition of a lens

Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

Who can create a lens?

Any individual member, a community, or a respected organization.

What are tags? tag icon

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

| External bookmarks