diff --git a/examples/mdp/consensus/coin.cexprop b/examples/mdp/consensus/coin.cexprop
new file mode 100644
index 000000000..bb60f986d
--- /dev/null
+++ b/examples/mdp/consensus/coin.cexprop
@@ -0,0 +1 @@
+P<0.4 [ F finished & all_coins_equal_1 ]
diff --git a/examples/mdp/csma/csma.cexprop b/examples/mdp/csma/csma.cexprop
new file mode 100644
index 000000000..fd4346176
--- /dev/null
+++ b/examples/mdp/csma/csma.cexprop
@@ -0,0 +1 @@
+P<0.5 [ !collision_max_backoff U all_delivered ]
diff --git a/examples/mdp/firewire/impl/firewire.cexprop b/examples/mdp/firewire/impl/firewire.cexprop
new file mode 100644
index 000000000..02d43560f
--- /dev/null
+++ b/examples/mdp/firewire/impl/firewire.cexprop
@@ -0,0 +1 @@
+P<0.5 [F elected]
diff --git a/examples/mdp/wlan/wlanX_1.cexprop b/examples/mdp/wlan/wlanX_1.cexprop
new file mode 100644
index 000000000..4c3a40fd8
--- /dev/null
+++ b/examples/mdp/wlan/wlanX_1.cexprop
@@ -0,0 +1 @@
+P<0.5 [ F oneCollision ]
diff --git a/examples/mdp/wlan/wlanX_2.cexprop b/examples/mdp/wlan/wlanX_2.cexprop
new file mode 100644
index 000000000..1dad8767d
--- /dev/null
+++ b/examples/mdp/wlan/wlanX_2.cexprop
@@ -0,0 +1 @@
+P<0.1 [ F twoCollisions ]