Model Checking Toolkit for Python.
mctk
is a Python library for Explicit-State Model Checking (will also support Symbolic Model Checking and Bounded Model Checking in the future) on Kripke Structures (will also support other Transition Systems) supporting the CTL(Computation Tree Logic) operators: EX, EU, EG, EF, AX, AU, AG, AF, and the Propositional Logic operators: NOT, AND, OR, IMPLIES, IFF.
Users can use functions that implements CTL operators to formally verify if a Kripke Structure (can be created during runtime or input in a JSON file) satisfies certain CTL properties. All checking functions will return a set of states that satisfy the CTL property, which means that if any start state of the Kripke Structure is in the returned set, then the Kripke Structure satisfies the CTL property.
Get the latest version of mctk
from PyPI. Note that the registered name is mctk-py
on PyPI due to the strict typo-squatting prevention mechanism of the registry. However, when using the library, you should import it as mctk
.
pip3 install mctk-py
If you are having trouble with pip3
, you can also install from the source code, see Developing.
Clone this Repository to your Local Environment.
git clone https://github.com/marcusm117/mctk.git
Go into the Repository Directory.
cd mctk
Install the Library with all Dependencies.
make develop
We use a Makefile
as a command registry:
make format
: autoformat this library withblack
make lint
: perform static analysis of this library withblack
,flake8
andpylint
make annotate
: run type checking usingmypy
make test
: run automated tests withpytest
make coverage
: run automated tests withpytest
and collect coverage information
from mctk import *
# create a Kripke Structure from scratch
ks = KripkeStruct()
# set 2 Atomic Propositions in this Kripke Structure
ks.set_atoms(["p", "q"])
# add 2 states to the Kripke Structure
# a State Name is represented by a string, it must be unique
# a State Label is represented by a list of Atoms, it must be unique
ks.add_state("s0", ["p"])
ks.add_state("s1", ["q"])
# set the Start States of the Kripke Structure
# there can be multiple Start States
ks.set_starts(["s0"])
# add 2 Transitions to the Kripke Structure
# a Transition is represented by a key-value pair
# where key the Source State Name and value is a list of Destination State Names
ks.add_trans({"s0": ["s1"], "s1": ["s0"]})
# check if the Kripke Structure satisfies the CTL formula: EX p
# SAT_atom(ks, "p") returns a set of states that satisfy the Atomic Proposition p
# EX returns a set of states that satisfy the CTL formula EX p
sat_states = EX(ks, SAT_atom(ks, "p"))
# the result should be {"s1"}
# since the start state "s0" is not in sat_states, ks doesn't satisfy the CTL formula
assert sat_states == {"s1"}
# check if the Kripke Structure satisfies the CTL formula: E p U q
# SAT_atom(ks, "p") returns a set of states that satisfy the Atomic Proposition p
# SAT_atom(ks, "q") returns a set of states that satisfy the Atomic Proposition q
# EU returns a set of states that satisfy the CTL formula E p U q
sat_states = EU(ks, SAT_atom(ks, "p"), SAT_atom(ks, "q"))
# the result should be {"s0", "s1"}
# since the start state "s0" is in sat_states, ks satisfies the CTL formula
assert sat_states == {"s0", "s1"}
# check if the Kripke Structure satisfies the CTL formula: EX (p AND EX q)
sat_states = EX(ks, AND(SAT_atom(ks, "p"), EX(ks, SAT_atom(ks, "q"))))
# the result should be {"s1"}
# since the start state "s0" is not in sat_states, ks doesn't satisfy the CTL formula
assert sat_states == {"s1"}
# check if the Kripke Structure satisfies the CTL formula: EG (A p U (NOT q))
sat_states = EG(ks, AU(ks, SAT_atom(ks, "p"), NOT(ks, SAT_atom(ks, "q"))))
# the result should be set(), empty set
# since the start state "s0" is not in sat_states, ks doesn't satisfy the CTL formula
assert sat_states == set()
ks_json = {
"Atoms": ["a", "b", "c", "d"],
"States": {
"s1": ["a"],
"s2": ["a", "b"],
"s3": ["b", "c"],
"s4": ["b", "c", "d"],
"s5": ["b"],
"s6": ["c"],
"s7": ["d"],
},
"Starts": ["s1"],
"Trans": {
's1': ['s2'],
's2': ['s3', 's4'],
's3': ['s4'],
's4': ['s7'],
's5': ['s6'],
's6': ['s7', 's5'],
's7': ['s5'],
},
}
ks = KripkeStruct(ks_json)
# check if the Kripke Structure satisfies the CTL formula: EX a
sat_states = EX(ks, SAT_atom(ks, "a"))
# the result should be {"s1"}
# since the start state "s1" is in sat_states, ks satisfies the CTL formula
assert sat_states == {"s1"}
# check if the Kripke Structure satisfies the CTL formula: E a U b
sat_states = EU(ks, SAT_atom(ks, "a"), SAT_atom(ks, "b"))
# the result should be {'s1', 's2', 's3', 's4', 's5'}
# since the start state "s1" is in sat_states, ks satisfies the CTL formula
assert sat_states == {'s1', 's2', 's3', 's4', 's5'}
# check if the Kripke Structure satisfies the CTL formula: EG a
sat_states = EG(ks, SAT_atom(ks, "a"))
# the result should be set()
# since the start state "s1" is not in sat_states, ks doesn't satisfy the CTL formula
assert sat_states == set()
All contrbutions are welcome!
Please read CONTRIBUTING.md for details.