Encoding Formulas and Model Checking

pyModelChecking provides a user friendly support for building CTL*, CTL and LTL formulas. Each of these languages corresponds to a pyModelChecking’s sub-module which implements all the classes required to encode the corresponding formulas.

Propositional logic is also supported by pyModelChecking as a shared basis for all the possible temporal logics.

Propositional Logics

Propositional logics support is provided by including the pyModelChecking.language sub-module. This sub-module allows to represents atomic propositions and Boolean values through the pyModelChecking.formula.AtomicProposition and pyModelChecking.formula.Bool classes, respectively.

>>> from pyModelChecking.formula import *
>>> AtomicProposition('p')

p

>>> Bool(True)

True

Moreover, the pyModelChecking.language sub-module implements the logic operators \(\land\), \(\lor\), \(\rightarrow\) and \(\neg\) by mean of the classes pyModelChecking.formula.And, pyModelChecking.formula.Or, pyModelChecking.formula.Imply and pyModelChecking.formula.Not, respectively. These classes automatically wrap strings and Boolean values as objects of the classes pyModelChecking.formula.AtomicProposition and pyModelChecking.formula.Bool, respectively.

>>> And('p', True)

(p and True)

>>> And('p', True, 'p')

(p and True and p)

>>> f = Imply('q','p')
>>> And('p', f, Imply(Not(f), Or('q','s', f)))

(p and (q --> p) and (not (q --> p) --> (q or s or (q --> p))))

>> Imply('p', 'q', 'p')
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: __init__() takes exactly 3 arguments (4 given)

For user convenience, the function pyModelChecking.formula.LNot() is also provided. This function returns a formula equivalent to logic negation of the parameter and minimise the number of outermost \(\neg\).

>>> f = Not(Not(Not(And('p',Not('q')))))
>>> f

not not not (p and not q)

>>> LNot(f)

(p and not q)

>>> LNot(Not(f))

not (p and not q)

>>> LNot(LNot(f))

not (p and not q)

Temporal Logics Implementation

CTL* formulas can be defined by using the pyModelChecking.CTLS sub-module.

>>> from pyModelChecking.CTLS import *

Path quantifiers \(A\) and \(E\) as well as temporal operators \(X\), \(F\), \(G\), \(U\) and \(R\) are provided as classes (see ref:CTLS sub-module<ctls_api> for more details). As in the case of propositional logics, these classes wrap strings and Boolean values as objects of the classes pyModelChecking.CTLS.language.AtomicProposition and pyModelChecking.CTLS.language.Bool, respectively.

>>> phi = A(G(
...         Imply(And(Not('Close'),
...                   'Start'),
...               A(Or(G(Not('Heat')),
...                    F(Not('Error')))))
...         ))
>>> phi

A(G(((not Close and Start) --> A((G(not Heat) or F(not Error))))))

In order to simplify the use of the library, a parsing class pyModelChecking.CTLS.Parser: has been implemented. Its objects read a formula from a string and, when it is possible, translate it into a corresponding pyModelChecking.CTLS.Formula objects.

>>> parser = Parser()
>>> psi_str = 'A G ((not Close and Start) --> ' +
...           'A(G(not Heat) or F(not Error)))'
>>> psi = parser(psi_str)
>>> psi

A(G(((not Close and Start) --> A((G(not Heat) or F(not Error))))))

The sub-module also implements the CTL* model checking and fair model checking algorithms described in [CGP00].

>>> from pyModelChecking import Kripke
>>> K = Kripke(R=[(0, 1), (0, 2), (1, 4), (4, 1), (4, 2), (2, 0),
...               (3, 2), (3, 0), (3, 3), (6, 3), (2, 5), (5, 6)],
...            L={0: set(), 1: set(['Start', 'Error']), 2: set(['Close']),
...               3: set(['Close', 'Heat']),
...               4: set(['Start', 'Close', 'Error']),
...               5: set(['Start', 'Close']),
...               6: set(['Start', 'Close', 'Heat'])})
>>> modelcheck(K, psi)

set([0, 1, 2, 3, 4, 5, 6])

>>> modelcheck(K, psi, F=[6])

set([])

It is also possible to model check a string representation of a CTL* formula by either passing an object of the class pyModelChecking.CTLS.Parser or leaving the remit of creating such an object to the function pyModelChecking.CTLS.modelcheck().

>>> modelcheck(K, psi_str)

set([0, 1, 2, 3, 4, 5, 6])

>>> modelcheck(K, psi_str, parser=parser)

set([0, 1, 2, 3, 4, 5, 6])

Analogous functionality are provided for CTL and LTL by the sub-modules pyModelChecking.CTL and pyModelChecking.LTL, respectively.