Compositional Probabilistic Model Checking with String Diagrams of MDPs (ATVA 2025 - NIER)

Mon 27 - Fri 31 October 2025 Bengaluru, India

Track

ATVA 2025 NIER

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi.

Use conference time zone: (GMT+05:30) Chennai, Kolkata, Mumbai, New DelhiSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Mon 27 Oct 2025 11:30 - 12:00 at R102 - NIER 2

Abstract

We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of string diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evaluation demonstrates its performance advantages.

The talk is based on [Watanabe+, CAV’23, TACAS’24 & CAV’24]