// Intrusion detection system taken from // Dynamic Policy-Based IDS Configuration // Quanyan Zhu and Tamer Basar // gxn 20/03/18 // simple example from the paper with 2 libraries and attacks // and system can only be healthy or compromised csg player policy policy endplayer player attacker attacker endplayer const int rounds; module rounds r : [0..rounds]; // current time-step [] r (r'=r+1); [] r=rounds -> true; endmodule module csystem s : [1..2]; // system state // 1 - healthy // 2 - compromised [defend1,attack1] true -> (s'=1); [defend1,attack2] true -> (s'=2); [defend2,attack1] true -> (s'=2); [defend2,attack2] true -> (s'=1); endmodule module policy [defend1] r true; [defend2] r true; endmodule module attacker [attack1] r true; [attack2] r true; endmodule rewards "damage" [defend1,attack1] s=1 : 0; [defend1,attack2] s=1 : 1; [defend2,attack1] s=1 : 0.5; [defend2,attack2] s=1 : 0; [defend1,attack1] s=2 : 1; [defend1,attack2] s=2 : 2; [defend2,attack1] s=2 : 1.5; [defend2,attack2] s=2 : 1; endrewards const K; rewards "i_damage" [defend1,attack1] r=K-1 & s=1 : 0; [defend1,attack2] r=K-1 & s=1 : 1; [defend2,attack1] r=K-1 & s=1 : 0.5; [defend2,attack2] r=K-1 & s=1 : 0; [defend1,attack1] r=K-1 & s=2 : 1; [defend1,attack2] r=K-1 & s=2 : 2; [defend2,attack1] r=K-1 & s=2 : 1.5; [defend2,attack2] r=K-1 & s=2 : 1; endrewards