Changes between Version 25 and Version 26 of WikiStart

Timestamp:

Jun 19, 2008, 9:32:32 AM (11 years ago)

Author:

Dr. Ivan S. Zapreev

Comment:

--

WikiStart

@@ -1 +1 @@
 [[TracNav]]
 
-= Welcome to the MRMC home page =
+= What is MRMC? =
 
-'''MRMC is a command-line model checker for:'''
+'''MRMC is a model checker for:'''
  * Discrete time Markov chains (DTMCs),
  * Continuous time Markov chains (CTMCs),
@@ -10 +10 @@
  * Continuous time Markov decision processes (CTMDPIs).
 
-'''The tool is written in C and supports verification of:'''
+'''The tool supports verification of:'''
  * Probabilistic Computation Tree Logic (PCTL),
  * Continuous Stochastic Logic (CSL),
@@ -16 +16 @@
  * Continuous Stochastic Reward Logic (CSRL).
 
-MRMC allows for numerical model checking on all types of
-input models. In addition, verification of CSL properties
-on CTMCs can be done using model checking by Discrete Event
-Simulation.
+'''MRMC allows for:''
+
+  * Numerical model checking on all types of input models,
+  * Model checking by Discrete Event Simulation on CTMCs,
+  * Formula-dependent and formula-independent bisimulation.
 
 [[Image(mrmc_cmd.jpg, border=1, align=right, 30%)]]
 
-'''MRMC is available for the following platforms:'''
-
+MRMC is a command-line tool, written in C. It is available for:
  * Windows,
  * Linux,
- * Mac OS X.
+ * and Mac OS X
+platforms. The tool is distributed under the [http://www.gnu.org/licenses/gpl.html GPL License].
 
-The tool is distributed under the [http://www.gnu.org/licenses/gpl.html GPL License]. An example of the tool usage can be found on the right. If you are looking
+An example of the tool usage can be found on the right. If you are looking
 for detailed information about MRMC, consider reading the [wiki:Specifications MRMC Manual].