--%>
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 : Spss in Business and Management Please

    Please tell me the cost of this current assignment. Note : I do not want the Solutions but please tell me the price as the assignment is .. Is the cost 3 euro? Do you sell those questions?

    		•
  • Q : State Littles Law Little’s Law : • L =

    Little’s Law: • L = λR = XR • Lq = λW = XW • Steady state system • Little’s Law holds as long as customers are not destroyed or&nbs

    		•
  • 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 : MANOVA and Reflection Activity

    Activity 10:   MANOVA and Reflection   4Comparison of Multiple Outcome Variables This activity introduces you to a very common technique - MANOVA. MANOVA is simply an extension of an ANOV

    		•
  • Q : Creating Grouped Frequency Distribution

    Creating Grouped Frequency Distribution: A) At first we have to determine the biggest and smallest values. B) Then we have to Calculate the Range = Maximum - Minimum C) Choose the number of classes wished for. This is generally between 5 to 20. D) Find out the class width by dividing the range b

    		•
  • 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 : Define Utilization Law Utilization Law

    Utilization Law: • ρk = XK . SK = X . DK • Utilization of a resource is the fraction

    		•
  • Q : Develop the most appropriate regression

    Predicting Courier Costs The law firm of Adams, Babcock, and Connors is located in the Dallas-Fort metroplex.  Randall Adams is the senior and founding partner of the firm.  John Babcock has been a partne

    		•
  • Q : Problem on Model Checking Part (a).

    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 sta

    		•
  • Q : STATISTICS Question This week you will

    This week you will analyze if women drink more sodas than men.  For the purposes of this Question, assume that in the past there has been no difference.  However, you have seen lots of women drinking sodas the past few months.  You will perform a hypothesis test to determine if women now drink more

    		•