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.