Modelling of multi-agent-system as Kripke structure and implementation of its knowledge-base with modal logic formulas.

[beta] An experimental model checker for LTL written in Rust

A Java library that allows you to check whether a given transition system (described as a Kripke structure) satisfies a given computation tree logic (CTL) formula.

A Kripke structure modelling framework

Interprets multi-agent knowledge-based programs to solve puzzles like the Muddy Children Problem

A generic bounded model checker.

A teaching aid for concepts and algorithms in logic

Formal Modeling project M2