Projetos

Versão de 2/5/2007

Model checking

descaradamente copiado de http://www.cs.bham.ac.uk/~mzk/courses/AutoVeri-p1/index.html

A new controller system is being installed to manage entry into a tunnel, which has to periodically close. The tunnel controller sends out signals to the approaching cars. Cars are equipped with sensors able to read the signals. Formulate transition system models for two sub-systems, Tunnel and Car, based on the descriptions below.

• A. The tunnel controller emits a warning signal (closing) to approaching cars when it is about to close. A short while after the tunnel closes. When the tunnel is reopened, another signal (opening) is sent out.
• B. When a car is approaching the tunnel, it listens for the warning signal from the tunnel controller system. If such a signal is received, the car must begin to brake until fully stationary; else it proceeds at normal speed. When the tunnel is reopened, the car waits for the opening signal and starts driving.

Consider the models A and B that you have formulated.

• A. Construct the product of models A and B synchronised on closing and opening.
• B. The tunnel controller system must satisfy the basic safety requirement, i.e., the car must be stopped when the tunnel is closed. Express this requirement in CTL.
• C. Does your model satisfy this requirement? If not, how can the problem be fixed?

Planejamento usando POMDP

resolva o problema 1 deste arquivo descaradamente e ilegalmente copiados de http://www.cs.mcgill.ca/~jpineau/comp765/

não precisa me mandar nada via email. é so implementar os outros itens. Planejamento classico

Este projeto não é exatamete de planejamento, mas sim de PDDL, que é a linguagem de especificação de ações para a grande maioria dos planejadores disponiveis. Um problema de planejamento completo involveria, além da codificação em PDDL, pedido neste projeto, que os estados inicial e final fossem definidos, e que voces baixassem um dos planejadores disponiveis na internet.

Codifique um dos dois problema abaixo em PDDL.

• We have a parcel delivery robot that can move parcels between the Sandford Fleming, Pratt, and Bahen buildings. Assume the robot can carry an unlimited number of parcels and the only relevant locations are the Sandford Fleming, Pratt, and Bahen buildings. When travelling between Bahen and the other two buildings, the robot must go outside. In contrast, it can travel indoors between Sandford Fleming and Pratt by using the bridge, provided it can open the door to the bridge. The robot must use one of its parcels to keep the door propped open as it passes through. Once through, it can safely pick up the parcel used. Assume all other doors have a wheel chair access button which allows the robot to go through without using any parcel to prop them open. If the robot goes outside when it's raining, it will get wet unless it has an umbrella. It can get an umbrella in Sandford Fleming. Our goals can specify things about the location of various parcels, the robot's location and the robot staying dry.
• NASA needs to plan the mission of a group of robotic probes that will be sent to Mars, as a prelude to human exploration of the planet. Two types of probes are being send, comsats and rovers. Comsats (communication satellites) remain in orbit and establish a communication network, relaying data produced by the rovers on Mars to mission control on Earth. A comsat is fixed in one of two orientations, facing Earth or facing Mars. When facing Earth, a comsat may send test results back to mission control; when facing Mars it may receive test results sent by a rover. A comsat can always relay a message to another comsat. Rovers explore the planet, perform tests, and send test results back to the comsats. Rovers may move between test sites on the planet's locations that have been identified as being of scientific importance. At a test site, a rover may perform one of two tests, a soil composition test or a mineral analysis test. Each rover is equipped with some instruments that allows it to perform only some of the tests. Due to memory limitations in the rovers, if a rover has performed a test, it cannot perform another test until it has sent the results to a comsat. Typically, mission control will request that the results of certain tests performed at certain sites be sent back to earth. After a test is performed the rover must send the results back to a comsat, that in turn must relay the message (possibly through other comsats) back to mission control.

copiado de http://www.cs.toronto.edu/~ppoupart/teaching/lectures/lectures.html

Diagnostico

Este site lista os simtomas de 5 doenças infantis comuns. implemente um sistema de diagnótico para essas 5 doenças.