Logics and Model Checking API

The implementations of specific languages and their model checking routines are contained in pyModelChecking sub-modules. CTL*, CTL, and LTL are handled by CTLS sub-module, CTL sub-module and LTL sub-module, respectively.

Propositional Logics sub-module API

It represents Proposition Logics formulas.

Language

class pyModelChecking.PL.language.And(*phi)

Bases: pyModelChecking.PL.language.LogicOperator, pyModelChecking.language.And

Represents logic conjunction.

class pyModelChecking.PL.language.AtomicProposition(name)

Bases: pyModelChecking.PL.language.Formula, pyModelChecking.language.AlphabeticSymbol

The class representing atomic propositionic propositions.

clone()

Clones an atomic proposition

Returns:a clone of the current atomic proposition Return type:PL.AtomicProposition

subformula(i)

Returns the \(i\)-th subformula.

Parameters:i (Integer) – the index of the subformula to be returned Raises:TypeError – atomic propositions have not subformulas

subformulas()

Returns the list of all the subformulas.

Returns:returns the empty list of the subformulas of the current formula Return type:list

class pyModelChecking.PL.language.Bool(value)

Bases: pyModelChecking.language.Bool, pyModelChecking.PL.language.AtomicProposition

The class of Boolean atomic propositions.

class pyModelChecking.PL.language.Formula(*phi)

Bases: pyModelChecking.language.Formula

A class to represent propositional formulas.

Formulas are represented as nodes in labelled trees: leaves are terminal symbols (e.g., atomic propositions and Boolean values), while internal nodes correspond to operators and quantifiers. The ariety of internal nodes depends on the kind of operator or quantifier must be represented. For instance, the arity of a node representing the formula \(not (p \lor True)\) is one because the formula has exclusively one sub-formula, i.e., \(p \lor True\). On the contrary, this last formula has two sub-formulas, i.e., \(p\) and \(True\), thus, the node representing it has two sons.

cast_to(Lang)

Casts the current object in a formula of a different class.

Parameters:

• self (class) – this formula
• Lang – a class representing a language

Returns:

a syntactically equivalent formula in language represented by Lang

Return type:

Lang

wrap_subformulas(subformulas, FormulaClass)

Replaces subformulas of the current object

This method replaces the subformulas of the current object by using the FormulaClass objects representing the elements of :param subformulas:.

Parameters:

• self (PL.Formula) – this object
• subformulas (Container) – the set of objects to be used as model for the replacement
• FormulaClass (class) – the final class of the new subformulas

class pyModelChecking.PL.language.Imply(*phi)

Bases: pyModelChecking.PL.language.LogicOperator, pyModelChecking.language.Imply

Represents logic implication.

class pyModelChecking.PL.language.LogicOperator(*phi)

Bases: pyModelChecking.PL.language.Formula, pyModelChecking.language.LogicOperator

A class to represent logic operator such as \(\land\) or \(\lor\).

class pyModelChecking.PL.language.Not(*phi)

Bases: pyModelChecking.PL.language.LogicOperator, pyModelChecking.language.Not

Represents logic negation.

class pyModelChecking.PL.language.Or(*phi)

Bases: pyModelChecking.PL.language.LogicOperator, pyModelChecking.language.Or

Represents logic non-exclusive disjunction.

pyModelChecking.PL.language.get_symbols(alphabet)

CTLS sub-module API

It represents CTL* formulas and provides model checking methods for them.

Language

class pyModelChecking.CTLS.language.A(phi)

Bases: pyModelChecking.CTLS.language.PathQuantifier, pyModelChecking.language.AlphabeticSymbol

A class representing CTL* A-formulas.

get_equivalent_non_fair_formula(fairAP)

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.Not

symbols = ['A']

class pyModelChecking.CTLS.language.And(*phi)

Bases: pyModelChecking.CTLS.language.LogicOperator, pyModelChecking.PL.language.And

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.Not

class pyModelChecking.CTLS.language.AtomicProposition(name)

Bases: pyModelChecking.PL.language.AtomicProposition, pyModelChecking.CTLS.language.StateFormula

The class representing atomic propositionic propositions.

get_equivalent_non_fair_formula(fairAP)

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula. Since this is a method of the class CTLS.AtomicProposition, a clone of the current object is always returned.

Returns:a clone of the current atomic proposition. Return type:CTLS.AtomicProposition

class pyModelChecking.CTLS.language.Bool(value)

Bases: pyModelChecking.PL.language.Bool, pyModelChecking.CTLS.language.AtomicProposition

The class of Boolean atomic propositions.

class pyModelChecking.CTLS.language.E(phi)

Bases: pyModelChecking.CTLS.language.PathQuantifier, pyModelChecking.language.AlphabeticSymbol

A class representing CTL* A-formulas.

get_equivalent_non_fair_formula(fairAP)

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.E

symbols = ['E']

class pyModelChecking.CTLS.language.F(*phi)

Bases: pyModelChecking.CTLS.language.TemporalOperator, pyModelChecking.language.AlphabeticSymbol

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.U

symbols = ['F']

class pyModelChecking.CTLS.language.Formula(*phi)

Bases: pyModelChecking.PL.language.Formula

A class to represent CTL* formulas.

Formulas are represented as nodes in labelled trees: leaves are terminal symbols (e.g., atomic propositions and Boolean values), while internal nodes correspond to operators and quantifiers. The ariety of internal nodes depends on the kind of operator or quantifier must be represented. For instance, the arity of a node representing the formula \(not (A(p U q) \lor True)\) is one because the formula has exclusively one sub-formula, i.e., \(A(p U q) \lor True\). On the contrary, this last formula has two sub-formulas, i.e., \(A(p U q)\) and \(True\), thus, the node representing it has two sons.

get_equivalent_non_fair_formula(fairAP)

is_a_state_formula()

Returns True if and only if the object represents a state formula.

This method should return True if and only if the current object represents a state formula. Since this is a general class meant to represent both state and path formulas, an implementation for this method cannot be provided. Thus, any call to it raise a RuntimeError.

Parameters:self (CTLS.Formula) – this formula Raises:RuntimeError – this method cannot be implemented by this general class

class pyModelChecking.CTLS.language.G(*phi)

Bases: pyModelChecking.CTLS.language.TemporalOperator, pyModelChecking.language.AlphabeticSymbol

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.Not

symbols = ['G']

class pyModelChecking.CTLS.language.Imply(*phi)

Bases: pyModelChecking.CTLS.language.LogicOperator, pyModelChecking.PL.language.Imply

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.Not

class pyModelChecking.CTLS.language.LogicOperator(*phi)

Bases: pyModelChecking.CTLS.language.Formula, pyModelChecking.PL.language.LogicOperator

A class to represent logic operator such as \(\land\) or \(\lor\).

is_a_state_formula()

Returns True if and only if the object represents a state formula.

This method returns True if and only if the current object represents a state formula.

Parameters:self (CTLS.LogicOperator) – this formula Returns:True if and only if the object represents a state formula. Return type:bool

class pyModelChecking.CTLS.language.Not(*phi)

Bases: pyModelChecking.CTLS.language.LogicOperator, pyModelChecking.PL.language.Not

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.Not

is_a_state_formula()

Returns True if and only if the object represents a state formula.

This method returns True if and only if the current object represents a state formula.

Parameters:self (CTLS.Not) – this formula Returns:True if and only if this formula is a state formula. Return type:bool

class pyModelChecking.CTLS.language.Or(*phi)

Bases: pyModelChecking.CTLS.language.LogicOperator, pyModelChecking.PL.language.Or

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.Or

class pyModelChecking.CTLS.language.PathFormula(*phi)

Bases: pyModelChecking.CTLS.language.Formula

A class representing CTL* path formulas.

is_a_state_formula()

Check whether the object has type StateFormula.

This method returns True if and only if the current object has type CTLS.StateFormula. Since this is a method of the class CTLS.PathFormula, it always returns False.

Parameters:self (CTLS.PathFormula) – this formula Returns:False Return type:bool

class pyModelChecking.CTLS.language.PathQuantifier(phi)

Bases: pyModelChecking.CTLS.language.StateFormula

A class to represent the path quantifiers \(A\) or \(E\).

class pyModelChecking.CTLS.language.R(*phi)

Bases: pyModelChecking.CTLS.language.TemporalOperator, pyModelChecking.language.AlphabeticSymbol

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.Not

symbols = ['R']

class pyModelChecking.CTLS.language.StateFormula(*phi)

Bases: pyModelChecking.CTLS.language.PathFormula

A class representing CTL* state formulas.

is_a_state_formula()

Check whether object has type StateFormula.

This method returns True if and only if the current object has type CTLS.StateFormula. Since this is a method of the class CTLS.StateFormula, it always returns True.

Parameters:self (CTLS.StateFormula) – this formula Returns:True Return type:bool

class pyModelChecking.CTLS.language.TemporalOperator(*phi)

Bases: pyModelChecking.CTLS.language.PathFormula

A class to represent temporal operators such as \(R\) or \(X\).

class pyModelChecking.CTLS.language.U(*phi)

Bases: pyModelChecking.CTLS.language.TemporalOperator, pyModelChecking.language.AlphabeticSymbol

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula Return type:CTLS.U

symbols = ['U']

class pyModelChecking.CTLS.language.X(*phi)

Bases: pyModelChecking.CTLS.language.TemporalOperator, pyModelChecking.language.AlphabeticSymbol

get_equivalent_restricted_formula()

Return an equivalent formula in the restricted syntax.

This method returns a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent to this formula.

Returns:a formula that avoids \(A\), \(F\), \(R\), \(\land\) and \(\\rightarrow\) and is equivalent this formula Return type:CTLS.X

symbols = ['X']

Model Checking

pyModelChecking.CTLS.model_checking.modelcheck(kripke, formula, parser=None, F=None)

Model checks any CTL* formula on a Kripke structure.

This method performs CTL* model checking of a formula on a given Kripke structure.

Parameters:

• kripke (Kripke) – a Kripke structure.
• formula (a type castable in a CTLS.Formula or a string representing a CTLS formula) – the formula to model check.
• parser (CTLS.Parser) – a parser to parse a string into a CTLS.Formula.
• F (Container) – a list of fair states

Returns:

a list of the Kripke structure states that satisfy the formula.

CTL sub-module API

It represents CTL formulas and provides model checking methods for them.

Language

class pyModelChecking.CTL.language.A(phi)

Bases: pyModelChecking.CTLS.language.A, pyModelChecking.CTL.language.StateFormula

A class representing CTL A-formulas.

get_equivalent_non_fair_formula(fairAP)

get_equivalent_restricted_formula()

Return a equivalent formula in the restricted syntax.

This method returns a formula that avoids \(\land\), \(\\rightarrow\), \(A\), \(F\), and \(R\) and is equivalent to this formula.

Parameters:self (CTL.E) – this formula Returns:a formula that avoids \(\land\), \(\\rightarrow\), \(A\), \(F\), and \(R\) and is equivalent to this formula Return type:CTL.StateFormula

pyModelChecking.CTL.language.AF(psi)

A shortcut to build \(E(X(\psi))\).

This method returns the formula \(E(X(\psi))\) where \(\psi\) is the method parameter.

Parameters:psi (CTL.StateFormula) – a state formula Returns:the formula \(E(X(\psi))\) Return type:CTL.StateFormula

pyModelChecking.CTL.language.AG(psi)

A shortcut to build \(A(G(\psi))\).

This method returns the formula \(A(G(\psi))\) where \(\psi\) is the method parameter.

Parameters:psi (CTL.StateFormula) – a state formula Returns:the formula \(A(G(\psi))\) Return type:CTL.StateFormula

pyModelChecking.CTL.language.AR(psi, phi)

A shortcut to build \(A(R(\psi, \phi))\).

This method returns the formula \(A(R(\psi, \phi))\) where \(\psi\) and \(\phi\) are the method parameters.

Parameters:

• psi (CTL.StateFormula) – a state formula
• phi (CTL.StateFormula) – a state formula

Returns:

the formula \(A(R(\psi, \phi))\)

Return type:

CTL.StateFormula

pyModelChecking.CTL.language.AU(psi, phi)

A shortcut to build \(A(U(\psi, \phi))\).

This method returns the formula \(A(U(\psi, \phi))\) where \(\psi\) and \(\phi\) are the method parameters.

Parameters:

• psi (CTL.StateFormula) – a state formula
• phi (CTL.StateFormula) – a state formula

Returns:

the formula \(A(U(\psi, \phi))\)

Return type:

CTL.StateFormula

pyModelChecking.CTL.language.AX(psi)

A shortcut to build \(A(X(\psi))\).

This method returns the formula \(A(X(\psi))\) where \(\psi\) is the method parameter.

Parameters:psi (CTL.StateFormula) – a state formula Returns:the formula \(A(X(\psi))\) Return type:CTL.StateFormula

class pyModelChecking.CTL.language.And(*phi)

Bases: pyModelChecking.CTLS.language.And, pyModelChecking.CTL.language.StateFormula

A class representing CTL conjunctions.

class pyModelChecking.CTL.language.AtomicProposition(name)

Bases: pyModelChecking.CTLS.language.AtomicProposition, pyModelChecking.CTL.language.StateFormula

A class representing CTL atomic propositions.

class pyModelChecking.CTL.language.Bool(value)

Bases: pyModelChecking.CTLS.language.Bool, pyModelChecking.CTL.language.StateFormula

A class representing CTL Boolean atomic propositions.

class pyModelChecking.CTL.language.E(phi)

Bases: pyModelChecking.CTLS.language.E, pyModelChecking.CTL.language.StateFormula

A class representing CTL E-formulas.

get_equivalent_non_fair_formula(fairAP)

get_equivalent_restricted_formula()

Return a equivalent formula in the restricted syntax.

This method returns a formula that avoids \(\land\), \(\\rightarrow\), \(A\), \(F\), and \(R\) and is equivalent to this formula.

Parameters:self (CTL.E) – this formula Returns:a formula that avoids \(\land\), \(\\rightarrow\), \(A\), \(F\), and \(R\) and is equivalent to this formula Return type:CTL.StateFormula

pyModelChecking.CTL.language.EF(psi)

A shortcut to build \(E(F(\psi))\).

This method returns the formula \(E(F(\psi))\) where \(\psi\) is the method parameter.

Parameters:psi (CTL.StateFormula) – a state formula Returns:the formula \(E(F(\psi))\) Return type:CTL.StateFormula

pyModelChecking.CTL.language.EG(psi)

A shortcut to build \(E(G(\psi))\).

This method returns the formula \(E(G(\psi))\) where \(\psi\) is the method parameter.

Parameters:psi (CTL.StateFormula) – a state formula Returns:the formula \(E(G(\psi))\) Return type:CTL.StateFormula

pyModelChecking.CTL.language.ER(psi, phi)

A shortcut to build \(E(R(\psi, \phi))\).

This method returns the formula \(E(R(\psi, \phi))\) where \(\psi\) and \(\phi\) are the method parameters.

Parameters:

• psi (CTL.StateFormula) – a state formula
• phi (CTL.StateFormula) – a state formula

Returns:

the formula \(E(R(\psi, \phi))\)

Return type:

CTL.StateFormula

pyModelChecking.CTL.language.EU(psi, phi)

A shortcut to build \(E(U(\psi, \phi))\).

This method returns the formula \(E(U(\psi, \phi))\) where \(\psi\) and \(\phi\) are the method parameters.

Parameters:

• psi (CTL.StateFormula) – a state formula
• phi (CTL.StateFormula) – a state formula

Returns:

the formula \(E(U(\psi, \phi))\)

Return type:

CTL.StateFormula

pyModelChecking.CTL.language.EX(psi)

A shortcut to build \(E(X(\psi))\).

This method returns the formula \(E(X(\psi))\) where \(\psi\) is the method parameter.

Parameters:psi (CTL.StateFormula) – a state formula Returns:the formula \(E(X(\psi))\) Return type:CTL.StateFormula

class pyModelChecking.CTL.language.F(*phi)

Bases: pyModelChecking.CTLS.language.F, pyModelChecking.CTL.language.PathFormula

A class representing CTL F-formulas.

class pyModelChecking.CTL.language.Formula(*phi)

Bases: pyModelChecking.CTLS.language.Formula

A class representing CTL formulas.

class pyModelChecking.CTL.language.G(*phi)

Bases: pyModelChecking.CTLS.language.G, pyModelChecking.CTL.language.PathFormula

A class representing CTL G-formulas.

class pyModelChecking.CTL.language.Imply(*phi)

Bases: pyModelChecking.CTLS.language.Imply, pyModelChecking.CTL.language.StateFormula

A class representing CTL implications.

class pyModelChecking.CTL.language.Not(*phi)

Bases: pyModelChecking.CTLS.language.Not, pyModelChecking.CTL.language.StateFormula

A class representing CTL negations.

class pyModelChecking.CTL.language.Or(*phi)

Bases: pyModelChecking.CTLS.language.Or, pyModelChecking.CTL.language.StateFormula

A class representing CTL disjunctions.

class pyModelChecking.CTL.language.PathFormula(*phi)

Bases: pyModelChecking.CTL.language.Formula, pyModelChecking.CTLS.language.PathFormula

A class representing CTL* path formulas.

class pyModelChecking.CTL.language.R(*phi)

Bases: pyModelChecking.CTLS.language.R, pyModelChecking.CTL.language.PathFormula

A class representing CTL R-formulas.

class pyModelChecking.CTL.language.StateFormula(*phi)

Bases: pyModelChecking.CTL.language.Formula, pyModelChecking.CTLS.language.StateFormula

A class representing CTL* state formulas.

class pyModelChecking.CTL.language.U(*phi)

Bases: pyModelChecking.CTLS.language.U, pyModelChecking.CTL.language.PathFormula

A class representing CTL U-formulas.

class pyModelChecking.CTL.language.X(*phi)

Bases: pyModelChecking.CTLS.language.X, pyModelChecking.CTL.language.PathFormula

A class representing CTL X-formulas.

Model Checking

pyModelChecking.CTL.model_checking.modelcheck(kripke, formula, parser=None, F=None)

Model checks any CTL formula on a Kripke structure.

This method performs CTL model checking of a formula on a given Kripke structure.

Parameters:

• kripke (Kripke) – a Kripke structure.
• formula (a type castable in a CTL.Formula or a string representing a CTL formula) – the formula to model check.
• parser (CTL.Parser) – a parser to parse a string into a CTL.Formula.
• F (Container) – a list of fair states

Returns:

a list of the Kripke structure states that satisfy the formula.

LTL sub-module API

It represents LTL formulas and provides model checking methods for them.

Language

class pyModelChecking.LTL.language.A(*phi)

Bases: pyModelChecking.LTL.language.StateFormula, pyModelChecking.CTLS.language.A

A class representing LTL A-formulas.

class pyModelChecking.LTL.language.And(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.And

A class representing LTL conjunctions.

class pyModelChecking.LTL.language.AtomicProposition(name)

Bases: pyModelChecking.CTLS.language.AtomicProposition, pyModelChecking.LTL.language.PathFormula

A class representing LTL atomic propositions.

class pyModelChecking.LTL.language.Bool(value)

Bases: pyModelChecking.CTLS.language.Bool, pyModelChecking.LTL.language.PathFormula

A class representing LTL Boolean atomic propositions.

class pyModelChecking.LTL.language.F(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.F

A class representing LTL F-formulas.

class pyModelChecking.LTL.language.Formula(*phi)

Bases: pyModelChecking.CTLS.language.Formula

A class representing LTL formulas.

class pyModelChecking.LTL.language.G(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.G

A class representing LTL G-formulas.

class pyModelChecking.LTL.language.Imply(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.Imply

A class representing LTL implications.

class pyModelChecking.LTL.language.Not(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.Not

A class representing LTL negations.

class pyModelChecking.LTL.language.Or(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.Or

A class representing LTL disjunctions.

class pyModelChecking.LTL.language.PathFormula(*phi)

Bases: pyModelChecking.LTL.language.Formula, pyModelChecking.CTLS.language.PathFormula

A class representing LTL path formulas.

class pyModelChecking.LTL.language.R(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.R

A class representing LTL R-formulas.

class pyModelChecking.LTL.language.StateFormula(*phi)

Bases: pyModelChecking.LTL.language.Formula, pyModelChecking.CTLS.language.StateFormula

A class representing LTL state formulas.

class pyModelChecking.LTL.language.U(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.U

A class representing LTL U-formulas.

class pyModelChecking.LTL.language.X(*phi)

Bases: pyModelChecking.LTL.language.PathFormula, pyModelChecking.CTLS.language.X

A class representing LTL X-formulas.

Model Checking

pyModelChecking.LTL.model_checking.modelcheck(kripke, formula, parser=None, F=None)

Model checks any LTL formula on a Kripke structure.

This method performs LTL model checking of a formula on a given Kripke structure.

Parameters:

• kripke (Kripke) – a Kripke structure.
• formula (a type castable in a LTL.Formula or a string representing a LTL formula) – the formula to model check.
• parser (LTL.Parser) – a parser to parse a string into a LTL.Formula.
• F (Container) – a list of fair states

Returns:

a list of the Kripke structure states that satisfy the formula.