Equilibrium Probabilistic LTL Synthesis¶

This repository contains experiments for learning policy profiles in multi-agent games where each agent has a probabilistic temporal-logic objective. The core question is:

Can independently learned agents satisfy their own temporal goals, and can we check in a model-free way whether the learned profile is close to equilibrium?

The project combines PettingZoo-style environments, LTLf reward monitors, reinforcement-learning baselines, and post-training verification. It is research code, but the main workflows are packaged as runnable Marimo notebooks and reusable Python experiment helpers.

What The Project Does¶

The experiment loop is:

1. Choose an environment and one temporal objective per agent.
2. Wrap the environment with a Boolean reward monitor for each objective.
3. Train a policy profile with one of the supported algorithms.
4. Evaluate objective satisfaction from rollouts.
5. Estimate whether any single agent can improve by deviating while the others stay fixed.
6. Save plots and reports for later comparison.

The temporal objective is not the same thing as equilibrium. Temporal formulas describe what each agent wants to make true over a finite trace. Equilibrium-style checks are computed after training from rollouts and learned best responses.

Reading Path¶

If you are new to the project, read these pages in order:

• Getting Started for setup, docs preview, and notebooks.
• Concepts for the vocabulary used throughout the repo.
• Workflow for the train, verify, compare cycle.
• Environments to choose a benchmark.
• Verification to interpret NashConv, AlphaRank, and satisfaction reports.

If you already know the project and need a specific reference:

• Algorithms explains the trainer families and CER variants.
• Notebooks maps the Marimo notebooks.
• Artifacts explains exports, reports, checkpoints, and resume behavior.
• API Reference documents curated Python entrypoints.
• Development explains where user docs and internal AI notes belong.

Repository Map¶

• src/environments/ contains matrix and gridworld environments.
• src/monitor/ contains LTLf monitors and reward wrappers.
• src/rl/ contains training implementations.
• src/verify/ contains model-free verification and satisfaction estimation.
• src/experiments/ contains reusable experiment orchestration.
• notebooks/ contains Marimo notebooks for running and inspecting experiments.
• docs/ contains these user-facing docs.
• docs/AI/ contains durable implementation notes for developers and agents.