FiMDP

FiMDP implements controller synthesis for Consumption Markov Decision Processes (CMDPs) with Linear Temporal Logic (LTL) objectives expressed by deterministic Büchi automata.

Key Features:

• Polynomial-time controller synthesis: Implements and builds on a polynomial-time algorithm for controller synthesis in CMDPs with resource constraints.
• LTL objectives: Supports Linear Temporal Logic objectives expressible by deterministic Büchi automata.
• Heuristics for reachability: Incorporates heuristics aimed at improving expected reachability times of accepting states.
• Multi-agent task allocation: Provides support for multi-agent task allocation within resource-constrained environments.
• Simulation framework (FiMDPEnv): Includes FiMDPEnv for strategy simulation in realistic environments.
• Storm integration: Integrates with the Storm model checker for evaluation and validation of CMDP controllers.
• Python implementation: Provided as a Python-based package for computational use and integration.

Scientific Applications:

• Resource-constrained system modeling: Modeling and analysis of systems with resource consumption constraints using CMDPs.
• Probabilistic decision-making analysis: Studying probabilistic decision-making under temporal objectives specified in LTL.
• Controller evaluation and validation: Evaluating and validating synthesized controllers via simulation (FiMDPEnv) and the Storm model checker.

Methodology:

Builds upon a polynomial-time controller synthesis algorithm for CMDPs, uses deterministic Büchi automata to encode LTL objectives, incorporates heuristics to improve expected reachability times, supports multi-agent task allocation, and employs FiMDPEnv and Storm for simulation and evaluation.