Compositional probabilistic model checking with string diagrams of MDPs

DOI10.1007/978-3-031-37709-9_3zbMATH Open1547.68458MaRDI QIDQ6535679FDOQ6535679

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

Publication date 1 February 2024

zbMATH Keywords

Markov decision processmodel checkingcategory theorycompositionalitymonoidal categorystring diagram

Mathematics Subject Classification ID

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

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

• 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 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A Representation Theorem for Unique Decomposition Categories
• A compositional approach to parity games
• A functor-valued invariant of tangles
• Abstraction-Refinement for Hierarchical Probabilistic Models
• Categories for Quantum Theory
• Compositional higher-order model checking via \(\omega\)-regular games over Böhm trees
• Compositional probabilistic model checking with string diagrams of MDPs
• Compositional probabilistic verification through multi-objective model checking
• 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

(2)

• Compositional probabilistic model checking with string diagrams of MDPs
• A compositional framework for Petri nets

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)