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 : Regression Analysis 1. A planning

1. A planning official in the Texas Department of Community Affairs, which works in the office next to you, has a problem. He has been handed a data set from his boss that includes the costs involved in developing local land use plans for communities wi

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 : Principles of data analysis For the

For the data analysis project, you will address some questions that interest you with the statistical methodology we are learning in class. You choose the questions; you decide how to collect data; you do the analyses. The questions can address almost any topic,

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

Explain differences between Cumulative Frequency and Relative Frequency?

Q : Computers playing games How Computers

How Computers playing games can be categorized according to different dimensions?

Q : Average think time Software monitor

Software monitor data for an interactive system shows a CPU utilization of 75%, a 3 second CPU service demand, a response time of 15 seconds, and 10 active users. Determine the average think time of these users?

Q : Statics for each of the following

for each of the following studies a and b decide whether to reject the null hypothesis that groiups come from identical populations. Use the .01 level. (c) Figure the effects size for each study. (d) ADVANCED TOPIC: Carry out an analysis of variance for study (a) using the strucurtal method.

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

No hassle, Instant Access

Start Discovering

18,76,764

1937833
Asked

3,689

Active Tutors

1444410

Questions
Answered

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

Submit Assignment