diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm
new file mode 100644
index 00000000..190a6452
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm
@@ -0,0 +1,16 @@
+// simple sanity test case for DTMC steady state computations (2 BSCCs)
+
+dtmc
+
+module m1
+  s: [0..2] init 0;
+
+  [] s=0 -> 1/4:(s'=0) + 1/2:(s'=1) + 1/4:(s'=2);
+  [] s>0 -> true;
+endmodule
+
+module m2
+  t: [0..2] init 0;
+
+  [] true -> 1/2:(t'=0) + 1/4:(t'=1) + 1/4:(t'=2);
+endmodule
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props
new file mode 100644
index 00000000..01252ac8
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props
@@ -0,0 +1,32 @@
+// RESULT: 0
+S=?[ s=0 ];
+
+// RESULT: 0
+S=?[ s=0 & t=0 ];
+
+// RESULT: 1/3
+S=?[ s=1 & t=0 ];
+
+// RESULT: 1/6
+S=?[ s=1 & t=1 ];
+
+// RESULT: 1/6
+S=?[ s=1 & t=2 ];
+
+// RESULT: 1/6
+S=?[ s=2 & t=0 ];
+
+// RESULT: 1/12
+S=?[ s=2 & t=1 ];
+
+// RESULT: 1/12
+S=?[ s=2 & t=2 ];
+
+// RESULT: 1/2
+S=?[ t=0 ];
+
+// RESULT: 1/4
+S=?[ t=1 ];
+
+// RESULT: 1/4
+S=?[ t=1 ];
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args
new file mode 100644
index 00000000..d21284d2
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args
@@ -0,0 +1,5 @@
+-explicit
+-hybrid
+-sparse
+-mtbdd
+-exact
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm
new file mode 100644
index 00000000..62af59ad
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm
@@ -0,0 +1,10 @@
+// simple test case for DTMC steady state computation (exhibits non-convergence using "naive" iteration)
+
+dtmc
+
+module m
+  s: [0..2] init 0;
+
+  [] s=0 -> 1/2:(s'=1) + 1/2:(s'=2);
+  [] s>0 -> (s'=0);
+endmodule
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props
new file mode 100644
index 00000000..ff54cb7a
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props
@@ -0,0 +1,12 @@
+// RESULT: 1
+S=?[ s=0 | s=1 | s=2 ];
+
+// RESULT: 1/2
+S=?[ s=0 ];
+
+// RESULT: 1/4
+S=?[ s=1 ];
+
+// RESULT: 1/4
+S=?[ s=2 ];
+
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props.args b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props.args
new file mode 100644
index 00000000..9a4cebfa
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props.args
@@ -0,0 +1,7 @@
+# sanity check for convergence for the different engines
+# mtbdd/sparse/hybrid currently require the switch to the power method for convergence
+-mtbdd -power
+-sparse -power
+-hybrid -power
+-explicit
+-exact