/ACOW

Applied Formal Methods.

Primary LanguagePythonMIT LicenseMIT

ACOW

Metric Temporal Logic Model Checking Tool written in Python 3.X

(This is the project for AERE/COMS 407X/507X Applied Formal Methods. You need Conda and Graphviz installed first.)

What this tool can do:

1) Verication of safety/liveness property

  • Safety: certain (bad) states reachable?
  • Liveness: certain (good) states bound to be reached?

2) Bounded and unbounded model checking

  • Bounded methods: Only consider traces of up to a maximum length.
  • Unbounded methods: Consider an unlimited number of steps.

Steps:

  1. Create python Environment:
conda env create -f environment.yml
  1. Activate the Environment:
source activate ACOW
  1. Modefiy the state space model and MTL formula in MTL_main.py. Then run:
python MTL_main.py