# 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)