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 : 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 : Sample Questions in Graphical Solution

Solved problems in Graphical Solution Procedure, sample assignments and homework Questions: Minimize Z = 10x1 + 4x2 Subject to

Q : FIN512 Entrepreneurial Finance Chapter

Chapter 6: Discussion Question: #4 p. 223 It is usually easier to forecast sales for a seasoned firm contrast to an early-stage venture because an early-stage venture has limited access to bank credit lines, sho

Q : Correlation analysis and the regression

1). When you take out a mortgage, there are many different kinds of costs. Usually the two largest are the interest rate (annual percentage that determines the size of your monthly payment) and the loan fee (a one-time percentage charged to you at the time

Q : Cumulative Frequency and Relative

Explain differences between Cumulative Frequency and Relative Frequency?

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

Discover Q & A

Leading Solution Library

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

No hassle, Instant Access

Start Discovering

18,76,764

1934512
Asked

3,689

Active Tutors

1438285

Questions
Answered

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

Submit Assignment