Compositional probabilistic model checking with string diagrams of MDPs

DOI10.1007/978-3-031-37709-9_3MaRDI QIDQ6535679zbMATH OpenFDO

Authors Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37709-9_3

zbMATH Keywords

category theorycompositionalityMarkov decision processmodel checkingmonoidal categorystring diagram

Mathematics Subject Classification ID

String diagrams and graphical calculi (18M30) Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)

Recommendations

• Compositional reasoning for Markov decision processes (extended abstract)
• Model checking probabilistic systems
• Multi-Objective Model Checking of Markov Decision Processes
• Symbolic model checking for probabilistic processes
• Multi-objective Model Checking of Markov Decision Processes

Cites work

• A compositional approach to parity games
• A functor-valued invariant of tangles
• A Representation Theorem for Unique Decomposition Categories
• Abstraction-Refinement for Hierarchical Probabilistic Models
• Categories for Quantum Theory
• Categories for the working mathematician.
• Compositional higher-order model checking via -regular games over Böhm trees
• Compositional probabilistic model checking with string diagrams of MDPs
• Compositional probabilistic verification through multi-objective model checking
• scientific article; zbMATH DE number 4180789 (Why is no real title available?)
• scientific article; zbMATH DE number 4123722 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Maximizing the conditional expected reward for reaching the goal
• Notions of computation and monads
• Open system categorical quantum semantics in natural language processing
• Parameter synthesis for Markov models: faster than ever
• Traced monoidal categories

Cited in

(6)

• Compositional probabilistic model checking with string diagrams of MDPs
• A compositional framework for Petri nets
• Causally deterministic Markov decision processes
• Categorical semantics of compositional reinforcement learning
• Compositional verification of almost-sure Büchi objectives in MDPs
• Pareto fronts for compositionally solving string diagrams of parity games

This page was built for publication: Compositional probabilistic model checking with string diagrams of MDPs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535679)