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 : Designing a system What are the

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

Q : Model Checking Approach Model Checking

Model Checking Approach: • Specify program model and exhaustively evaluate that model against a speci?cation –Check that properties hold

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

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 : Cumulative Frequency and Relative

Explain differences between Cumulative Frequency and Relative Frequency?

Q : Hw An experiment is conducted in which

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 : STATISTICS Question This week you will

Q : Computing Average revenue using

Can anyone help me in the illustrated problem? The airport branch of a car rental company maintains a fleet of 50 SUVs. The inter-arrival time between the requests for an SUV is 2.4 hrs, on an average, with a standard deviation of 2.4 hrs. There is no indication of a

Q : State Littles Law Little’s Law : • L =

Little’s Law: • L = λR = XR • Lq = λW = XW • Steady state system • Little’s Law holds as long as customers are not destroyed or&nbs

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 1450164 Solved problems, classrooms assignments, textbook's solutions, for quick Downloads

No hassle, Instant Access

Start Discovering

18,76,764

1924547
Asked

3,689

Active Tutors

1450164

Questions
Answered

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

Submit Assignment