References

---

A dumping ground for interesting references. Don't expect a lot of organization! 😅

Footnotes per Page

---

All references from all pages.

/cli

• See docker-mcmas.git for the default container, see environment variables for control over default image.

/doxastic

• wiki://Dynamic_epistemic_logic#Knowledge_versus_Belief

• wiki://Doxastic/Types-of-Reasoners

• Principles of Knowledge and Belief

/epistemics-in-model-checkers

• via claude://ec0f46bc-3244-46a8-92b9-1f3f35aecb3a

• Official User Manual

• See all references from all pages

/ispl

• ISPL examples that ship with the engine source

• Reasoning About Knowledge, Fagin et al

/isplref

• claude://ba29d757-ba5e-45c7-992e-971da71b6d30

• Official User Manual, Section 3.2 (pdf)

• See all references from all pages

• For the ISPL grammar, see User Manual, Section 3.4 (pdf)

/lib

• MCMAS: an open-source model checker for the verification of multi-agent systems, Lomuscio et al 2015

/logic

• Here, "exotic" means especially epistemic-logics for describing knowledge/belief, but also strategy-logic, which has applications in game theory and protocol design. See also this mathoverflow Q/A

• MCMAS: an open-source model checker for the verification of multi-agent systems, Lomuscio et al 2015

/opref

• claude://ba29d757-ba5e-45c7-992e-971da71b6d30

• Official User Manual, Section 3.2 (pdf)

• See all references from all pages

• For the ISPL grammar, see User Manual, Section 3.4 (pdf)

/overview

• MCMAS: an open-source model checker for the verification of multi-agent systems, Lomuscio et al 2015 (pdf)

• wiki://Specification-language

• Official SAIL page

• Engine source mirror (github)

• Official user-manual (pdf)

• ISPL examples

• The container[^8] is managed by the python-docker SDK[^9], but you still need a docker daemon ready (or available at DOCKER_HOST).

• For a look at the container py-mcmas uses, see docker-mcmas.git.

• rtd://docker-py

• wiki://Witnesess

• wiki://Multi-Agent-System

• wiki://Agent-Based-Model

• joint embedding / JEPA

• The coming AI Revolution in Distributed Systems

• wiki://Formal-Specification

• ghio://Chain-of-Code

• AGI is an engineering problem

• gh://Camel-AI

• World Models

• MCP Overview

• wiki://Doxastic/Types-of-Reasoners

• yt://specs-are-the-new-code

• github://humanlayer/context-engineering

• wiki://Formal-Methods

• wiki://autocatalytic-set

• https://ai.pydantic.dev

• Reasoning about Knowledge, Fagin et al 1995

• wiki://Dynamic_epistemic_logic/Syntax

• There's a EBNF-style grammar for ISPL available in the documentation and the engine source uses flex/bison.

• pyModelChecking symbols ↔ ISPL Logic

• ISPL primitives are well-suited to this, but ideally such a system could directly target other kinds of solvers[^11] other formalisms like mean-field games[^12].

/philosophy

• MCMAS: an open-source model checker for the verification of multi-agent systems, Lomuscio et al 2015 (pdf)

/quickstart

• placeholder

• placeholder

Misc Links

---

---

Foundational Stuff:

• MCMAS: an open-source model checker for the verification of multi-agent systems, Lomuscio et al 2015
• Halpern, Joseph Y, Reasoning about uncertainty, The MIT Press, 2003.
• Reasoning About Knowledge, Fagin et al 1995

Languages, Engines, Tools, Resources for Model Checking

• wiki://model checking
• wiki://Binary_decision_diagram
• Tools:
  • github://johnyf/tool_lists: index of tools for verification and games
  • github://albertocasagrande/pymodelchecking
  • github://marcusm117/mctk: kripke structures / model checking logic from scratch in python
  • ELVis: Epistemic logic visualizer
  • A cheatsheet/overview of the popular stuff, including SPIN, PRISM, etc.
  • ghio://tyche, a library for aleatoric description logic Engines:
  • wiki://tla+
  • Prism model checker, uses PCTL
  • mCRL2
    • formal-spec toolset: https://www.mcrl2.org/web/index.html *mcrl2 algebra
  • gh://jrclogic/SMCDEL model checker with PAL support
  • gh://sysulic/MEPK A general multi-agent epistemic planner based on higher-order belief change
  • gh://msakai/haskell-decision-diagrams BDDs lib in haskell
• Papers/Lectures/Etc:
  • MCK
    • Gammie, Peter, and Ron Van Der Meyden, ‘MCK: Model checking the logic of knowledge’, in Computer Aided Verification, Springer, 2004,
    • MCK solver whitepaper (an alternative to MCMAS also supporting epistemic logic)
  • Montanari lecture slides, with an intro to model checkers
  • SMV language lectures, mentioned as inspiration for ISPL. (2011)
  • Scaling Multi-Agent Epistemic Planning through GNN-Derived Heuristics (2025)
  • A process algebraic framework for multi-agent dynamic epistemic systems (2024)
  • A Computationally Grounded, Weighted Doxastic Logic Chen et al 2015
  • Intro to PAL / Public Announcement Logic
  • Kh logics, i.e. Know-how vs Know-that. Wang, Li, 2021
  • Resources for MCAPL (model checking agent programming language) ~2023

Related Topics in Formal Models, Games, & Simulation * wiki://mean-field-game-theory * rtd://mfglib

Agentic AI, LLMs, MCP: * Papers: * dynasaur: LLAgents beyond predefined actions * Camel agents * camel agents * code * Generative Agents: Interactive Simulacra of Human Behavior Park et al 2023
* Genetic programming with LLMs as evolutionary operators * Evolving Code with A Large Language Model * code * Small LLMs focused on tool-calling: * https://github.com/ollama/ollama/blob/main/docs/linux.md * https://medium.com/data-science-in-your-pocket/smollm3-the-best-small-llm-for-everything-3fa53713ebb7 * https://ollama.com/driaforall/tiny-agent-a * https://ollama.com/library/granite3-dense * Standards etc * pydantic-ai-mcp * github://bstuddard/simple-mcp-example gh://projectmesa/mesa Agent-based modeling in Python