bounded-prescience 0.0.3
Shielding Atari Games with Bounded Prescience
Requires Python: >=3.5
Keywords: rl,safety,atari,agent

# bounded-prescience
This repo contains code for the paper Shielding Atari Games with Bounded Prescience (https://arxiv.org/abs/2101.08153) by Mirco Giacobbe, Hosein Hasanbeig, Hjalmar Wijk and Daniel Kroening. In addition to replicating the experiments in the paper and the bounded prescience shield, the repo allows the creation of property-labelled versions of the standard Atari gym environments which can expose safety information for other agents and policies.
## Installation
The prescience package needs to be installed through pip:
```
git clone https://github.com/HjalmarWijk/bounded-prescience.git
cd bounded-prescience
pip3 install .
```
or alternatively:
```
pip3 install git+https://github.com/HjalmarWijk/bounded-prescience.git
```
## Properties
| Game         | Property       | Description                                  | Classification |
|--------------|----------------|----------------------------------------------|----------------|
| Alien        | death          | Losing a life                                |                |
| Amidar       | death          | Losing a life                                |                |
| Assault      | death          | Losing a life                                |                |
| Assault      | overheat       | Losing a life from overheating               | Shallow        |
| Asterix      | death          | Losing a life                                |                |
| Asteroids    | death          | Losing a life                                |                |
| Atlantis     | death          | Losing a life                                |                |
| BankHeist    | death          | Losing a life                                |                |
| BankHeist    | death          | Losing a life                                |                |
| BattleZone   | death          | Losing a life                                |                |
| BeamRider    | death          | Losing a life                                |                |
| Berzerk      | death          | Losing a life                                |                |
| Berzerk      | death          | Losing a life                                |                |
| Bowling      | no-hit         | Missing all pins                             | Minimal        |
| Bowling      | no-strike      | Missing at least one pin                     |                |
| Boxing       | knock-out      | Getting knocked out                          | Minimal        |
| Boxing       | lose           | Losing the match                             | Minimal        |
| Boxing       | no-enemy-ko    | Match ends without knocking out enemy        |                |
| Breakout     | death          | Losing a life                                |                |
| Centipede    | death          | Losing a life                                |                |
| CrazyClimber | death          | Losing a life                                |                |
| DemonAttack  | death          | Losing a life                                |                |
| DemonAttack  | death          | Losing a life                                |                |
| DemonAttack  | death          | Losing a life                                |                |
| DoubleDunk   | out-of-bounds  | Moves out of bounds                          | Shallow        |
| DoubleDunk   | shoot-bf-clear | Losing ball due to shooting before clearing\* | Shallow        |
| Enduro       | crash-car      | Crashing into another car                    |                |
| FishingDerby | lose           | Not winning over the opponent                |                |
| Freeway      | hit            | Being hit by car                             |                |
| Frostbite    | death          | Losing a life                                |                |
| Frostbite    | freezing       | Losing a life from time running out          |                |
| Gopher       | lose-carrot    | Having a carrot eaten                        |                |
| Gravitar     | death          | Losing a life                                |                |
| Gravitar     | fuel           | Running out of fuel                          | Shallow        |
| Hero         | death          | Losing a life                                |                |
| IceHockey    | enemy-score    | Opponent scores                              |                |
| Jamesbond    | death          | Losing a life                                |                |

\* See [manual](https://atariage.com/manual_html_page.php?SoftwareLabelID=153) for details on this game rule.

To test properties use the test\_property.py script with flags --env [Game name] --prop [Property name]

This simulates a random agent and logs violations. To evaluate properties with human play, use --human flag (requires pygame). 

## Verification

To check properties for the 9 pre-trained agents evaluated in the paper under a variety of settings see the script check\_noops.py
To run the ChainerRL agents you first need to download them by running download\_models.py (the Atari Zoo agents download dynamically).
The scripts chainer\_no\_shield.sh and atari\_zoo\_no\_shield.sh run all the agents for all propertiesm and write results as a csv in the results folder. Note that Atari Zoo agents need Tensorflow 1 (and AtariZoo) installed, while ChainerRL agents needs Tensorflow 2 and ChainerRL. 

## Shielding

To check properties using prescience shielding use the --lookahead flag for check\_noops.py
The shield scripts run this check for all algorithms, properties and shield depths up to 5.

## Reference
Please use this bibtex entry if you want to cite this repository in your publication:

```
@misc{bounded_prescience_repo,
  author = {Mirco Giacobbe, Mohammadhosein Hasanbeig, Daniel Kroening, and Hjalmar Wijk},
  title = {Shielding Atari Games with Bounded Prescience Code Repository},
  year = {2020},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/HjalmarWijk/bounded-prescience}},
}
```

## License
This project is licensed under the terms of the [BSD-3-Clause](/LICENSE)