Update README.md

-Coming soon
\ No newline at end of file
+# MAPTs
+
+MAPTs (Multi-Agent with timed periodic tasks) are a class of models dedicated to the representation of real-time systems of cooperative agents.
+Their state spaces can be dynamically explored to check CTL properties.
+
+## Zinc compiler
+
+MAPTS models can be translated into high level Petri nets for an implementation with the academic tool Zinc.
+Explorations algorithms have been implemented using the functions provided by this compiler.
+Zinc can be downloaded from https://github.com/fpom/zinc
+
+## Models
+
+The models provided in the repository "Models" represents three communicating autonomous vehicles an a highway portion.
+They use different decision making protocols and their state is define by a large number of variables.
+These models are use in the report  ... (link to do).
+
+## Checker
+
+The file "checker.py" features various explorations algorithms and boolean propostions along with their associated heuristic functions.
+To try these functions on the provided models, first install Zinc in a local repository.
+Then, copy in the same repository the contents of one of the chosen model ("libsverifcar.py" and "verifcar.py") and the file "checker.py".
+libsverifcar.py defines constants while verifcar.py implement the high level Petri net.
+First, the model should be compiled.
+Open a terminal and use:
+
+    python3 verifcar.py
+
+This will create a file name "netverifcar.py", which the functions in "checker.py" will be able to explore.
+Then enter the python3 environnement with the command:
+
+    python3
+    
+From the python3 environnement, you can now import "checker.py" and use the explorations algorithms.
+Here is an example where the query EF travel\_time\_A ≥ 15.9 is checked.
+
+    >>> import checker
+    >>> checker.exist_state(checker.travel_time_i_sup_n,checker.heuristic_hestimate_travel_time,(0,158))
+
+The function exist\_state is used with the boolean proposition travel\_time\_i\_sup\_n and its associated heuristic function heuristic\_hestimate\_travel\_time.
+0 is the identifier of the vehicle and 158 is the excluded lower bound for the proposition to be true.
+
+Here is another example where the query EF ttc\_A\_B ≤ 0 is checked.
+
+    >>> import checker
+    >>> checker.exist_state(checker.ttc_i_j_inf_n,checker.time_to_overtake_i_j_inv,(0,1,1))
+
+The function exist\_state is used with the boolean proposition ttc\_i\_j\_inf\_n(0,1,1) and its associated heuristic function time\_to\_overtake\_i\_j\_inv.
+0 and 1 are the identifiers of the vehicles and 1 is the excluded upper bound for the proposition to be true.
+
+    
\ No newline at end of file