Welcome to pyModelChecking’s documentation!

pyModelChecking is a simple Python model checking package. Currently, it is able to represent Kripke structures, Propositional Logics, CTL, LTL, and CTL* formulas and it provides model checking methods for LTL, CTL, and CTL*. In future, it will hopefully support symbolic model checking.

Basic Notions

• Reactive Systems
  • Directed Graphs
    • Directed Acyclic Graphs and Trees
  • Kripke Structures
• Logics
  • Propositional Logics
    • Syntax
    • Semantics
  • Computational Tree Logic*
    • Syntax
    • Semantics
    • Restricted Syntax
  • Computational Tree Logic
    • Syntax
    • Semantics
    • Restricted Syntax
  • Linear Time Logic
    • Syntax
    • Semantics
    • Restricted Syntax
• Model Checking
  • Fair Model Checking
• Symbolic Representation
  • Binary Decision Diagrams
  • Ordered Binary Decision Diagrams

Using pyModelChecking

• Modelling Reactive Systems
  • Directed Graphs
  • Kripke Structures
• Encoding Formulas and Model Checking
  • Propositional Logics
    • Parsing Formulas
  • Temporal Logics Implementation
  • Model Checking Formulas

API

• Models API
  • Graph API
  • Kripke API
• Logics and Model Checking API
  • Propositional Logics sub-module API
    • Language
  • CTLS sub-module API
    • Language
    • Model Checking
  • CTL sub-module API
    • Language
    • Model Checking
  • LTL sub-module API
    • Language
    • Model Checking

Indices and tables

• Index
• Module Index
• Search Page