The home of the MC4CSL^TA model checker.

A new model checker for the CSL^TA logic

MC4CSL^TA is a probabilistic model checker for the CSL^TA stochastic logic that performs formal modeling and quantitative probabilistic analysis of systems, specified as continuous time Markov chain (CTMCs). The tool analyses systems designed with the GreatSPN tool with the Petri net graphical formalism. Performance queries are written in the CSL^TA stochastic logic, specifing complex path properties as Deterministic Timed Automata (DTA). Other formats are supported, like MRMC and Prism CTMCs in input, and Cosmos models as output.

Moreover, MC4CSL^TA is a general framework for the analysis of Markov chains and Markov regenerative processes (MRP) with deterministic events. The tool implements both forward and backward analysis, with explicit, implicit and component-based numerical solution. Linear solutions uses implicit matrix-free numerical methods, with optional preconditioning.

The source code is written in C++11 and is available for free. A fully-featured graphical user interface is under active development and is available for download from this page.

Installation

The latest version of the MC4CSL^TA tool is version 2.0, and can be download from this link. Extract the distribution in a directory, and type make to build the source. The tool requires clang-3.2 and flex 2.5.35 to compile. The flex tool is found under the label Lex. If your system does not have asymbolic link to flex named Lex, please create one or modify the Makefile.
The compiled binaries are put in the build/ subdirectory of the tree.

Older versions of the tool are still available:

• Version 2.0
• Version 1.0

How to use MC4CSL^TA

MC4CSL^TA is a command line tool that loads models drawn with GreatSPN, or in the format of MRMC and Prism. The main tool is called DSPN-Tool, and is found in the bin/ subdirectory in both release and debug builds. The complete list of commands is shown by issuing the command:

The tool executes the commands in the same order they are given on the command line, so the order is significant. Model checking a CSL^TA query on a GreatSPN model is done with the command:

loads a Petri net model in the GreatSPN format, computes the tangible reachability graph, and then evaluates the CSL^TA query expr for all the CTMC states. A similar command, -cslta0 expr evaluates the CSL^TA query expr starting from the CTMC state with index state. The first case uses a numerical backward analysis, while the second case uses a forward analysis. Forward model checking can start from an arbitrary initial state using the command: -csltaN state expr. A report of the numerical analysis is written on the standard output. The solution satisfiability set can be written to the disk appending the command: -wrsat filename. Instead of loading a Petri net and build its TRG, it is possible to load directly a CTMC in MRMC format (model.lab and model.tra files) with the command:

Similarly, a Prism model exported in the states, labels and transitions files can be imported with the command: -load-prism model. The expected file extensions are .states, .labels and .trns.

An expression in the CSL^TA language is defined by the grammar:

where ap is a boolean condition on the state variables, ∼ is a comparison operator, λ is a real value in [0,1], dta is the name of a dta file in the dta search path, and parameters... are the dta parameters. The CSL^TA operators S_∼λ() and P_∼λ() are called STEADY() and PROB_TA(). The language of atomic propositions includes marking-dependent expressions over the CTMC state variables.

DTAs are read from a file. The specified dta argument name is looked in the dta search path (modified with -dta-path new-path) and in the colon-separated directories specified in the DIR_PATH environment variables. Usually, the DIR_PATH is set to the DTA/ subdirectory in the source tree of MC4CSL^TA, to have access to common DTAs (like the Until). DTAs are parametric in the atomic propositions, clock values and action names. Therefore, common DTAs like the Until or the Next, can be reused between different models by specifying the proper binding of the parameters.

A sample DTA is written in the following syntax:

The clock parameter alpha, the abstract action names a and b, and the abstract atomic proposition PHI and PSI are bound to the target model in the parameters... part of the PROB_TA operator. For instance, the CSL^TA expression:

evaluates the probability that a CTMC path satisfies the SampleDTA automaton when the abstract DTA parameters are substituted with the specified clock value (10), transition names (T1, T2) and state proposition expressions (#P1=0 and #P2!=#P3). State proposition expressions can be CSL^TA expressions (nested expressions).

Since DTAs are reusable, MC4CSL^TA comes equipped with a small number of commonly used DTAs, in the DTA/ directory of the source tree. These DTAs include the CSL Until and Next operators. For example, the CSL operator: Φ Until[α, β] Ψ can be obtained using the common DTA until_AB with the CSL^TA expression:

by replacing α, β, Φ, Ψ with the proper clock values and atomic propositions.

The numerical solution of a CSL^TA P_∼λ() expression builds the cross product of the CTMC state space with the DTA location space. By default, the entire cross state space is generated.

• Full cross product, explicit numerical solution. Option: -e
  The cross product state space is entirely generated and a solution MRP is constructed. The embedded Markov chain (EMC) of this MRP is then constructed and solved with a linear solution method.
• Full cross product, implicit (matrix-free) numerical solution. Option: -i
  The cross product state space is entirely generated, but the EMC is not constructed. Instead, a matrix-free solution method is used to compute the MRP solution.
• Full cross product, component-based solution. Option: -scc
  The cross product state space is entirely generated, and the solution is computed by analysing the state space one component at a time. Usually, components are CTMCs and not MRPs.
• [in progress] On the fly state space generation. Option: -on-the-fly
  The state space is generated one component at a time, and solved in isolation. This method does not require to keep in memory the entire state space of the cross product.

By default, MC4CSL^TA uses the first method (the slowest). The numerical solution can be chosen from many algorithms, including Gauss-Seidel (the default), Jacobi (-jor), Symmetric SOR (-ssor) and Krylov-subspace methods like GMRES (-gmres and -M base) conjugate gradient squared (-cgs) and bi-conjugate gradient stabilized (-bicgstab). Matrix-free solutions always use a Krylov-subspace method, and may use a preconditioner. The accuracy of the solution is set using -epsilon value.

Publications

The MC4CSL^TA has been the subject of the following publications.

• Amparore, E.G., Donatelli, S.: MC4CSL^TA: an efficient model checking tool for CSL^TA. In: International Conference on Quantitative Evaluation of Systems, Los Alamitos, CA, USA, IEEE Computer Society (2010) 153-154.
• Amparore, E.G., Donatelli, S.: Revisiting the Iterative Solution of Markov Regenerative Processes. Numerical Linear Algebra with Applications, Special Issue on Numerical Solutions of Markov Chains 18 (2011) 1067-1083.
• Amparore, E.G., Donatelli, S.: A component-based solution for reducible markov regenerative processes. Performance Evaluation 70 (2013) 400-422.
• Improving and assessing the efficiency of the MC4CSL^TA model checker. EPEW 2013, Venice, Italy.

If you want to cite the MC4CSL^TA tool in your publications, use the first citation of the above list.

Developers

The current developer and mantainer of MC4CSL^TA is Elvio G. Amparore, who have worked on it under the supervision of Susanna Donatelli. If you want more informations on the tool, please write an e-mail to amparore (at) di.unito.it or to susi (at) di.unito.it.

© 2013  Universitá degli Studi di Torino, Dipartimento di Informatica.