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

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 : Probability how can i calculate

how can i calculate cumulative probabilities of survival

Q : Variance and standard error A hospital

A hospital treated 412 skin cancer patients over a year. Of these, 197 were female. Give the point estimate of the proportion of females seeking treatment for skin cancer. Give estimates of the

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 : 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?

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 : 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 : Creating Grouped Frequency Distribution

Q : Define Operational Analysis

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

Discover Q & A

Leading Solution Library

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

No hassle, Instant Access

Start Discovering

18,76,764

1940077
Asked

3,689

Active Tutors

1451384

Questions
Answered

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

Submit Assignment