Examples

Here are some examples of systems analyzed with TAKOS. Those examples are taken from INRIA Research Report 7349. Additional examples can be downloaded here; processing of all examples are exposed in the documentation.

Remark. In the tool, the size of an estimator (for states or trajectories) is the number of states recorded (at least 2). Thus a K-delay estimator is suitable to study (K-1)-step based notions of opacity.

System G1

Analysis of the system G1 depicted by the LTS below can be found here.

LTS G1 with secret states q2 and q5

System G2

Analysis of the system depicted by the LTS below can be found here.

LTS G2 with secret states q2

System G5

Analysis of the system G5 depicted by the LTS below can be found here.

LTS G5 with secret states q2