--%>
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 : 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 : Define Service Demand Law

    Service Demand Law:• Dk = SKVK, Average time spent by a typical request obtaining service from resource k• DK = (ρk/X

    		•
  • Q : Define Operational Analysis

    Operational Analysis: • Analysis method based on the measurement of the operational characteristics of the system.

    Q : Statistics basic question This week you

    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

    		•
  • Q : Computers playing games How Computers

    How Computers playing games can be categorized according to different dimensions?

    		•
  • Q : State the hypotheses At Western

    At Western University the historical mean of scholarship examination score for freshman applications is 900. Population standard deviation is assumed to be known as 180. Each year, the assistant dean uses a sample of applications to determine whether the mean ex

    		•
  • Q : What is Forced Flow Law Forced Flow Law

    Forced Flow Law: • The forced flow law captures the relationship between the various components in the system. It states that the throughputs or flows, in all parts of a system must be proportional t

    		•
  • Q : Explain Queuing theory Queuing theory :

    Queuing theory: • Queuing theory deals with the analysis of lines where customers wait to receive a service:

    Q : Regression Analysis 1. A planning

    1. A planning official in the Texas Department of Community Affairs, which works in the office next to you, has a problem. He has been handed a data set from his boss that includes the costs involved in developing local land use plans for communities wi

    		•
  • 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

    		•