pmodelchecker is an application that facilitates the use of formal model analysis using Model Checking of spatio-temporal properties of P system models developed within the Infobiotics workbench. pmodelchecker receives as input a model developed as specified in section and a list of temporal logic formulas formalising some spatio-temporal properties to be checked against the dynamics of the model.
pmodelchecker uses two different stochastic model checkers, PRISM and MC2. When using PRISM it generates a model in the reactive modules language needed in PRISM in order to check the input logic formulas. When using MC2 it generates the needed simulation samples by running mcss, the multicomparmental simulator introduced in the previous section.
For instructions on how to compile and install pmodelchecker, see the README file included with the pmodelchecker distribution.
In order to run pmodelchecker after its installation run the following command:
$ pmodelchecker PARAMETER_FILE
where PARAMETER_FILE is an xml file declaring the input parameters required to perform model checking using one of the two stochastic model checkers integrated in Infobiotics, PRISM or MC2. For example, in order to run the examples in the directory PRISMexamples/ browse to this directory provided in the directory examples/ of the pmodelchecker distribution and type one of the commands below depending on which example you want to run:
$ pmodelchecker NAR1.params $ pmodelchecker NAR2.params
In a similar manner to run the examples for MC2 browse to the directory MC2examples/ inside the directory examples/ provided in the pmodelchecker distribution and type the command below:
$ pmodelchecker NAR_MC2.params
The output, probabilities or expected values for temporal logic formulas, is produced into the result file specified as in the parameter file as explained below.
The pmodelchecker parameter file provides information to determine which specific model checker to use, PRISM or MC2, and some parameters to control the application of these model checkers like the use of verification versus approximation or the number of samples to consider in the case of a simulative or approximative approach.
The parameter file is in an XML format which has the general form:
<parameters> <parameterSet name="SimulationParameters"> <parameter name="PARAMETER NAME" value="PARAMETER VALUE"/> <parameter name="PARAMETER NAME" value="PARAMETER VALUE"/> ... </parameterSet> </parameters>
The specific parameters are given in the table below:
|model_specification||Name of the file containing the model specification as an LPP-system||String||None|
|temporal_formulas||Name of the file containing the temporal logic formulas formalising the properties to check||String||None|
|model-checker||Name of the model checker to use PRISM or MC2||String||None|
|PRISM_model||Name of the file where to output the translation of our model into the PRISM language||String||Only when using PRISM|
|task||Task to perform when using PRISM as model checker. Translate LPP-system into the PRISM languge, build the corresponding Markov chain, verify or approximate the input properties||Translate/ Build/ Verify/ Approximate||Only when using PRISM|
|model_parameters||A string stating the values of the parameters in the model as follows param=lb:ub:s,param=lb:ub:s, ... where lb is the lowe bound, up is the upper bound and s is the step||String||Only when using PRISM|
|formula_parameters||A string stating the values of the parameters in the formulas as follows param=lb:ub:s,param=lb:ub:s, ... where lb is the lowe bound, up is the upper bound and s is the step||String||Only when using PRISM|
|states_file||Name of the file where to output the states of the Markov chain generated from the LPP-system||String||Only when using PRISM with task Build or Verify|
|transitions_file||Name of the file where to output the transitions of the Markov chain generated from the LPP-system||String||Only when using PRISM with task Build or Verify|
|number_samples||Number of simulations to generate when taking an approximate or simulative approach to model checking||Integer||Only when using PRISM with task Approximate or whenever using MC2|
|precision||Precision to achieve whith respect to real value when generating an estimate using approximate or simulative model checking||Double||Only when using PRISM with task Approximate|
|confidence||Confidence to achieve whith respect to real value when generating an estimate using approximate or simulative model checking||Double||Only when using PRISM with task Approximate|
|pathMC2||Location of the executable file for MC2||String||Only when using MC2|
|simulations_generatedHDF5||Flag to determine if the simulations needed to run MC2 are available in HDF5 format||true/false||Only when using MC2|
|simulations_generatedMC2||Flag to determine if the simulations needed to run MC2 are available in MC2 format||true/false||Only when using MC2|
|simulations_file_hdf5||Name of the file containing the simulations in HDF5 format or where to write them when using mcss||String||Only when using MC2 and the flag simulations_generatedMC2 = false|
|simulations_file_MC2||Name of the file containing the simulations in MC2 format or where to write them||String||Only when using MC2|
|mcss_params_file||Name of the file containing the parameters to run mcss in order to generate the necessary simulations||String||Only when using MC2 and the flag simulations_generatedHDF5 = false and simulations_generatedMC=false|
|results_file||Name of the file where to write the answers to the temporal logic formulas generated by the model checker||String||None|
The pmodelchecker distribution, including all source code, model examples, and documentation, are the copyright of of the Infobiotics Team (Hongqing Cao, Claudio Lima, Natalio Krasnogor, Francisco Romero-Campero, Jamie Twycross, and Jonathan Blakes) and is released under the GNU GPL version 3 license.
pmodelchecker was written by Francisco J. Romero-Campero and is being used on Systems/Synthetic Biology research projects in the University of Nottingham, U.K.
For further information or any questions please contact fxc AT cs.nott.ac.uk.
copyright 2009 Infobiotics Team, released under GNU GPL version 3.