Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
MASA-Safe-RL
Logo
MASA-Safe-RL

Get Started

  • Quick Start
  • Core Concepts
    • Labelling Function
    • Cost Function
  • Basic Usage

Common API

  • Constraints
    • Constrained Markov Decision Process (CMDP)
    • Linear Temporal Logic (LTL) Safety Constraint
    • Probabilistic Computation Tree Logic (PCTL) Constraint
    • Step-wise Probabilistic Constraint
    • Reach-avoid Constraint
    • Multi-Agent Constraints
      • Constrained Markov Game (CMG)
  • Wrappers
    • Core Wrappers
    • Misc Wrappers
    • Vectorized Envs
  • Metrics
    • Logging
  • Linear Temporal Logic (LTL)
    • Propositional Formula
    • DFA
    • Cost Function as a DFA
    • Shaped Cost Function
  • Probabilistic Computation Tree Logic (PCTL)

Environments

  • Multi Agent
    • Gridworlds
      • Markov Stag Hunt
    • Matrix Games
      • Bertrand
      • Chicken
      • Congestion
      • Dynamic Public Goods Game
      • Inspection
  • Single Agent
    • Cartpole
    • Safety Gridworlds
      • Island Navigation
      • Conveyor Belt
      • Sokoban
    • Pacman
    • Gridworlds
      • Bridge Crossing
      • Colour Grid World
      • Colour Bomb Grid World
    • Media Streaming

Algorithms

  • Algorithms Overview
  • Tabular Algorithms
    • Q Learning
    • Q Learning Lambda
    • LCRL
    • SEM
    • RECREG
  • On-Policy Algorithms
    • A2C
    • PPO
    • PPO Lagrangian
    • Constrained Policy Optimization
  • Shielded Algorithms
    • Parameterized PPO
    • Parameterized PPO V2

Tutorials

  • Basics
    • First MASA Experiment
    • Labels, Costs, and Infos
    • Wrapper Stack
  • Constraints
    • Constraints Tour
    • LTL-Safety
      • LTL Safety Colour Bomb
  • Wrappers
    • Vectorization and Normalization
  • Environments
    • Create a New Environment
  • Baselines
    • Tabular Safe RL Baselines
    • Continuous Safe RL Baselines
  • Shielding
    • Probabilistic Shielding MiniPacman
    • Safety Abstractions Pacman Coins
    • FrozenLake Shielding
  • Multi-Agent
    • Multi-Agent CMG

Misc

  • Probabilistic Shielding
Back to top
View this page
Edit this page

LTL-SafetyΒΆ

These tutorials show how to configure and inspect LTL-safety constraints in MASA.

  • Colour Bomb defines and loads DFA properties, runs labelled colour-bomb traces, and inspects automaton-state violations.

Runnable notebooks:

  • notebooks/tutorials/05_ltl_safety_colour_bomb.ipynb

Next
LTL Safety Colour Bomb
Previous
Constraints Tour
Copyright © 2025, Alexander Goodall, Omar Adalat, Edwin Hamel De Le Court, Francesco Belardinelli
Made with Sphinx and @pradyunsg's Furo