This is a simple C++ based implementation of the CTL and LTL model checking algorithms. It parses the formulae and descriptions of transition systems, and...
- for CTL, calculates the SAT sets of the subformulae and decides whether the system satisfies the formula.
- for LTL, calculates the closure, valid atoms and generates a tableau.
Both the formulae and the transision systems are parsed using the Boost.Spirit Parser library. It is written in Standard C++ and runs on both Windows and Linux.
The syntax for transistion system descriptions is a simple subset of the language used by the Graphviz dot graph plotting application, which allows to easily plot the system. An example transition system is:
digraph G {
S0 -> S1
S1 -> S2
S2 -> S0
S0 [label = "S0: r", shape="box"]
S1 [label = "r,y"]
S2 [label = "S2: g"]
}
The lines 2-4 define some states and transitions. The lines 6-8 define additional attributes for the states. The label is used by graphviz for displaying, and used by MCheck to define the atomic propositions. The part up to and including the colon is optional and ignored by MCheck. The remainder should be a comma-seperated list of propositions, each being a C-like identifier. Nodes whose shape is defined as "box" are assumed as initial states. Transistion systems descriptions are saved in ordinary text files and passed to MCheck.
Formulae are input via simple text files, one formula per line. Unicode UTF-8 characters are used for the operators. ASCII symbols are available as alternatives. Empty lines are ignored, as are comments starting with #. If the unicode operators are used, the files must be encoded as UTF-8, without a byte order mark. Therefore, Windows notepad can not be used. Whitespace is generally ignored except within atomic propositions. In the following sections, r, g and y are atomic propositions that correspond to the ones defined in the transition system, and Φ,Ψ are placeholders for sub-formulae.
CTL Formulae look like this:
∀ ⬜ (y → (∀ X g))
∃ ⬜ ∃(r U (∀X y))
The following syntax elements are defined for CTL formulae:
| Form | ASCII Alternative | Description |
|---|---|---|
| ⊤ / ⊥ | true/false | Boolean literals |
| ¬Φ | ! | Negation |
| Φ∧Ψ | & | Logical And |
| Φ∨Ψ | | | Logical Or |
| Φ→Ψ | -> | Logical implication |
| ∃XΦ | E X | Exists next |
| ∃(Φ U Ψ) | E(Φ U Ψ) | Exists until |
| ∃⬜Φ | E W | Exists always |
| ∀XΦ | A X Φ | For all next |
| ∀(Φ U Ψ) | A(Φ U Ψ) | For all until |
| ∀⬜Φ | A W Φ | For all always |
LTL Formulae look like this:
⊤ U (y ∧ (X g))
!(⊤ U (r ∧ ¬(X g)))
The following syntax elements are defined for LTL formulae:
| Form | ASCII Alternative | Description |
|---|---|---|
| ⊤ / ⊥ | true/false | Boolean literals |
| ¬Φ | ! | Negation |
| Φ∧Ψ | & | Logical And |
| Φ∨Ψ | | | Logical Or |
| Φ→Ψ | -> | Logical implication |
| XΦ | X | Next |
| Φ U Ψ | Until |
This table sums up the operator precedences. The first row has the highest precedence. The CTL/LTL formula grammars each include only a subset of these operators:
| Precedence | Operators |
|---|---|
| 4 | XΦ, ¬Φ, ∃XΦ, ∃(Φ U Ψ), ∃⬜Φ, ∀XΦ, ∀(Φ U Ψ), ∀⬜Φ |
| 3 | Φ U Ψ |
| 2 | Φ∧Ψ |
| 1 | Φ∨Ψ |
| 0 | Φ→Ψ |
As with many other languages, precedence can be enforced by parentheses.
MCheck is a console application, run it as:
MCheck CTL TransitionSystem.txt Formulae.txtor
MCheck LTL TransitionSystem.txt Formulae.txt Output.pdfWhere TransitionSystem.txt contains a description of a transition system and Formulae.txt one or more CTL/LTL formulae. The output of the LTL algorithm is written to Output.pdf, and the output of the CTL algorithm is printed to the standard output. Since the Windows Console does not support all of the Unicode operators, output can be redirected to a file which can then be displayed by a text editor to view the unicode characters:
MCheck CTL TransitionSystem.txt Formulae.txt > Result.txtAn example output for CTL is
∀ ⬜ (y → (∀ X g))
Is satisfied
Sat (∀ ⬜ (y → (∀ X g))) = {S0, S1, S2}
Sat (y → (∀ X g)) = {S0, S1, S2}
Sat (y) = {S1}
Sat (∀ X g) = {S1}
Sat (g) = {S2}
All computed formulae are printed, followed by the computation result, and its syntax tree. Each sub-formula is annotated with the set of states satisfying it.
The LTL algorithm prints the closure, and consistent atoms, and the resulting tableau into the PDF file.
The Releases page provides binaries for Windows and Linux. If you want to compile MCheck yourself, you can download the source code from GitHub.
For the CTL algorithm, no steps other than obtaining the binary are neccessary. For LTL, Graphviz (specifically, its "dot" application) and pdflatex (for example via the TeX Live distribution) have to be installed and reachable via the "Path" environment variable.
This project uses CMake and is known to work at least with MSVC and GCC on Linux. To compile it on Linux, run:
cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release .
make -j 4To compile on Windows, run
cmake -G "Visual Studio 14 2015 Win64" .and open the generated project in MSVC and compile it.
This is an open source project licensed under the terms of the BSD license. See the LICENSE file for details.