The home of the MC4CSLTA model checker.

The MC4CSLTA tool v3.0 can be downloaded here:

MacOSX version

Windows version

Linux version

The new Graphical User interface of MC4CSLTA is available here.

University of Torino logo.

GreatSPN modeling framework

A new model checker for the CSLTA logic

MC4CSLTA is a probabilistic model checker for the CSLTA 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 CSLTA 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, MC4CSLTA 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.


The latest version of the MC4CSLTA 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:

How to use MC4CSLTA

MC4CSLTA 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:

./DSPN-Tool -h

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

./DSPN-Tool -load model -cslta expr

loads a Petri net model in the GreatSPN format, computes the tangible reachability graph, and then evaluates the CSLTA query expr for all the CTMC states. A similar command, -cslta0 expr evaluates the CSLTA 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:

./DSPN-Tool -load-mrmc model -cslta expr

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 CSLTA language is defined by the grammar:

expr ::= True | False | ap | (expr) |
         expr && expr | expr || expr |
         STEADY (expr) |
         PROB_TA λ dta (parameters...)

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 CSLTA 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 MC4CSLTA, 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:

DTA SampleDTA = {
  CLOCKVALUESET = { alpha }
  ACTIONSET = { a, b }
    INITIAL l_0 : PHI;
            l_1 : PHI && !PSI;
            l_2 : PHI && PSI;
      FINAL l_3 : PSI;
  EDGES = {
    l_0 -> l_0 (x < alpha, {a}, RESET);
    l_0 -> l_2 (x = 0, #);
    l_1 -> l_0 (x = alpha, #, RESET);
    l_2 -> l_1 (x < alpha, Act);
    l_2 -> l_2 (x > alpha, Act);
    l_2 -> l_3 (x > 0, {b});

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 CSLTA expression:

PROB_TA > 0.5 SampleDTA (10 | T1, T2 | #P1=0, #P2!=#P3)

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 CSLTA expressions (nested expressions).

Since DTAs are reusable, MC4CSLTA 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 CSLTA expression:

PROB_TA > 0.5 until_AB (α, β | | Φ, Ψ)

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

The numerical solution of a CSLTA 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.

By default, MC4CSLTA 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.


The MC4CSLTA has been the subject of the following publications.

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


The current developer and mantainer of MC4CSLTA 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) or to susi (at)