--%>
Assignment Help - homework help

Problem on Model Checking

Part (a). Draw a state diagram for a car with the following state variables: D indicating whether the car is in drive; B indicating the brake pedal is depressed; G indicating the gas pedal is depressed; and M indicating whether the car is moving. (For example, the state DB¬G¬M says that the car is in drive, the brake pedal is down, the gas pedal is not down, and the car is not moving). Your state diagram should obey the following properties:

The start state is ¬D¬B¬G¬M.

  • To put the car in drive, the brake pedal must be down.
  • To push the gas pedal, the car must be in drive.
  • It is not possible to push both the gas and the brake at the same time.
  • Once the gas is down, the car will eventually move.
  • Once the car is moving, it is possible to stop the car by depressing the brake.

Part (b). For each of properties 1-4 listed in Part (a), write an LTL formula specifying the property, and make an informal argument why the property holds for your diagram.

Part (c). Is it possible to specify property 5 using an LTL formula? Justify your answer.

   Related Questions in Basic Statistics

  • Q : Assumptions in Queuing system

    Assumptions in Queuing system: • Flow balance implies that the number of arrivals in an observation period is equal to the

    		•
  • Q : Use the NW corner rule to find an

      (a) Use the NW corner rule to find an initial BFS, then solve using the transportation simplex method. Indicate your optimal objective function value. (b) Suppose we increase s1 from 15 to 16, and d3 from 10 to 11. S

    		•
  • Q : Define SPIN simulation modes SPIN: •

    SPIN: • SPIN generates C program that is the model checker – The pan verifier • Process Analyzer – Run the pan executable to do the model check

    		•
  • Q : Homework help on Human memory & SPSS

    Effect of Scopolamine on Human Memory: A Completely Randomized Three Treamtent Design (N = 28) Scopolamine is a sedative used to induce sle

    		•
  • Q : What is Interactive Response Time Law

    Interactive Response Time Law: • R = (L/X) - Z• Applies to closed systems.• Z is the think time. The time elapsed since&nb

    		•
  • Q : Explain Service times Service times: A)

    Service times:A) In most cases, servicing a request takes a “short” time, but in a few occasions requests take much longer.B) The probability of completing a service request by time t, is independent of how much tim

    		•
  • Q : Point of estimate standing data se to

    standing data se to develop a point of estimate

    		•
  • Q : Principles of data analysis For the

    For the data analysis project, you will address some questions that interest you with the statistical methodology we are learning in class. You choose the questions; you decide how to collect data; you do the analyses. The questions can address almost any topic,

    		•
  • Q : Problem on queuing diagram Draw a 

    Draw a queuing diagram for the systems below and describe them using Kendall’s notation: A) Single CPU system <

    		•
  • Q : Report on Simple Random Sampling with

    One of my friend has a problem on simple random sampling. Can someone provide a complete Report on Simple Random Sampling with or without replacement?

    		•