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