--%>
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 : 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 : 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 : Problems on ANOVA We are going to

    We are going to simulate an experiment where we are trying to see whether any of the four automated systems (labeled A, B, C, and D) that we use to produce our root beer result in a different specific gravity than any of the other systems. For this example, we would l

    		•
  • Q : Designing a system What are the

    What are the questions that comes into mind when designing a system?

    		•
  • Q : Help An experiment is conducted in

    An experiment is conducted in which 60 participants each fill out a personality test, but not according to the way they see themselves. Instead, 20 are randomly assigned to fill it out according to the way they think a parent sees them (i.e. how a parent would fill it out to describe the participant

    		•
  • Q : OIL I need to product when oil will

    I need to product when oil will finish time (by years) for 6 countries if the keep their production (per day) in the same level. So, the 6 countries have fixed reserves and production 1. statistics for Bahrain Crude oil reserves (million barrels) = 124.6 be careful in million Crude oil producti

    		•
  • Q : Write out the null hypothesis 1.

    1. (AAC/ACA c9q1).  For each of the following studies, decide whether you can reject the null hypothesis that the groups come from identical populations. Use the alpha = .05 level.1a.

  • Q : Time series what are the four

    what are the four components of time series?

    		•
  • 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 : Calculate the p- value Medical tests

    Medical tests were conducted to learn about drug-resistant tuberculosis. Of 284 cases tested in New Jersey, 18 were found to be drug- resistant. Of 536 cases tested in Texas, 10 were found to be drugresistant. Do these data indicate that New Jersey has a statisti

    		•
    Home | Company Overview | Services | Discover Q&A | Sitemap | Contact Us | T & C | Refund Policy | Copyright Policy | Blog | Q&A | Directory

    ©TutorsGlobe All rights reserved 2022-2023.