Problem on Model Checking, Part (a). Draw a state diagram for a car with the following

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.

View Complete Question

Related Questions in Basic Statistics

Q : Safety and Liveness in Model Checking

Safety and Liveness in Model Checking Approach; •? Safety: Nothing bad happens •? Liveness: Something good happens •? Model checking is especially good at verifying safety and liveness properties –?Concurrency i

Q : How to solve statistics assignment in

How to solve staistics assignment, i need some help in solving stats assignment on AVOVA based problems. Could you help in solving this?

Q : State Kendalls notation

Kendall’s notation: A/B/C/K/m/Z A, Inter-arrival distribution M exponential D constant or determ

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 : 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 : 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 : Statistics for Management Assignment

Q : Probability how can i calculate

how can i calculate cumulative probabilities of survival

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

Q : Simplified demonstration of Littles Law

Simplified demonstration of Little’s Law:

Discover Q & A

Leading Solution Library

Avail More Than 1419464 Solved problems, classrooms assignments, textbook's solutions, for quick Downloads

No hassle, Instant Access

Start Discovering

18,76,764

1959061
Asked

3,689

Active Tutors

1419464

Questions
Answered

Start Excelling in your courses, Ask an Expert and get answers for your homework and assignments!!

Submit Assignment