Model-checking-properties.md

-The model checking functions of _libhpng_ require an input of an SMC property definition by the user. The structure and rules for this input are as follows:
+The model checking functions of _libhpng_ require an input of a property definition by the user. The structure and rules for this input are according to the _Stochastic Time Logic_ and defined as follows:
 
 <ul style="list-style-type:disc">
 <li>The input has to begin with a point in time for which the property should be checked. This time specification has to be of the form "**x.x:**" (for example "3.0:" ). The decimal point has to be included and a colon has to follow.</li>
@@ -6,7 +6,7 @@ The model checking functions of _libhpng_ require an input of an SMC property de
 <li>After the time specification there has to be one of the following expressions:<p>
 <ol type="1">
 <li>"**P=?**" for the calculation of the mean value of all simulations and the corresponding confidence interval. The interval can have a specified width determining the number of runs or the number of runs can be set instead. Furthermore the confidence level has to be specified.</li>
-<li>"**P~x.x**" where "~" has to be replaced by "<" or ">=" (for example "P&gt;=0.5" or "P&lt;=0.1"). This expression is used for the sequiential probabilty ratio test.</li></li><p>
+<li>"**P~x.x**" where "~" has to be replaced by "<" or ">=" (for example "P&gt;=0.5" or "P&lt;=0.1"). This expression is used for the _Sequential Probability Ratio Test_.</li></li><p>
 <li>The expression is followed by a property surrounded by brackets "(" and ")". Brackets can be nested arbitrarily. Allowed types of formulas are as follows, where Φ1 and Φ2 are properties again.
 <ol type="1"><p>
 <li>True "**tt**"</li>
@@ -14,7 +14,7 @@ The model checking functions of _libhpng_ require an input of an SMC property de
 <li>Negation "**!Φ1**"</li>
 <li>Conjunction "**AND(Φ1, Φ2)**"</li>
 <li>Disjunction "**OR(Φ1, Φ2)**"</li>
-<li>_Until_ formula "**U\[t1, t2\](Φ1, Φ2)**" where t1 and t2 are the time bounds that have to be of the form "x.x".</li></li><p>
+<li>_Until_ formula "**U\[t1, t2\](Φ1, Φ2)**" where t1 and t2 are the relative time bounds that have to be of the form "x.x".</li></li><p>
 <p>
 <li>The supported atomic properties are as follows where "id" be the place ID, transition ID or guard arc ID depending on the kind of property and "~" has to be replaced by "<", "<=", "=", ">" or ">=".<ol type="i"><p>
 <li>The fluid level of a continuous place compared to a decimal value: "**fluidlevel('id')~x.x**"</li>