diff --git a/README.md b/README.md
index ae3e8a1..ca075d4 100644
--- a/README.md
+++ b/README.md
@@ -10,12 +10,16 @@ The toolkit consists of two separate modules implementing:
 
 The `examples` directory contains sample input files.
 
+### Multi-agent reaction systems (rsCTLK verification)
+
 To quickly test the BDD module you can perform verification of the TGC controller consiting of three trains:
 
 ```
 $ ./reactics bdd -c f1 examples/bdd/tgc.rs
 ```
 
+### Reachability
+
 The above command tests the formula labelled `f1` in the input file.
 
 To test the SMT module you can perform reachability verification of the scalable chain system:
@@ -24,6 +28,14 @@ To test the SMT module you can perform reachability verification of the scalable
 $ ./reactics smt examples/smt/chain_reaction.py 2 3 1
 ```
 
+### rsLTL verification
+
+To test the SMT module for rsLTL verification with the scalable chain system you need, the following command may be used:
+
+```
+./reactics smt examples/smt/scalable_chain.py 2 5 1
+```
+
 ### Reaction synthesis
 
 To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command: