EVENT

Event News

MTSS Center Colloquium by Kevin Zhou, Kittiphon Phalakarn, and Yun Chen Tsai

On Tuesday 15 July, Kevin Zhou, Kittiphon Phalakarn, and Yun Chen Tsai (National Institute of Informatics) will give talks for our colloquium at 16:30. Further details can be found below.

Talk 1:

Hereditary properties and weighted first-order model counting

Abstract:

The weighted first-order model counting problem asks: given a method of assigning weights to structures, compute the weighted sum of all models of a given first-order sentence. This problem is closely linked to statistical relational learning and probabilistic inference, where the weights can be used to model uncertainty about relational knowledge. The general weighted first-order model counting (WFOMC) problem is known to be computationally hard; however, prior work has shown that restricting to certain fragments of first-order logic allows for efficient computability.
Independently of the work on weighted model counting, the unweighted version of the model counting problem has been studied extensively in the combinatorics literature. This work has focused on understanding the asymptotic growth rates of hereditary properties of various combinatorial objects, which are classes defined by universally quantified first-order sentences. The most general such work is due to Laskowski and Terry, who classify the possible asymptotic growth rates of hereditary properties of arbitrary first-order structures in a finite relational signature into four discrete ranges.
These two streams of work have rather different aims and techniques; work on weighted model counting generally focuses on efficient algorithms, while work on hereditary properties generally focuses on proving structural results which lead to classification theorems. An obvious question then becomes, what can results from each area tell us about the other? We will discuss some preliminary work towards answering this question.

Speaker:

Kevin Zhou (National Institute of Informatics)

Talk 2:

Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games

Abstract:

For model checking stochastic games (SGs), bounded value iteration (BVI) algorithms have gained attention as efficient approximate methods with rigorous precision guarantees. However, BVI may not terminate or converge when the target SG contains end components. Most existing approaches address this issue by explicitly detecting and processing end components--a process that is often computationally expensive. An exception is the widest path-based BVI approach previously studied by Phalakarn et al., which we refer to as 1WP-BVI. The method performs particularly well in the presence of numerous end components. Nonetheless, its theoretical foundations remain somewhat ad hoc. In this paper, we identify and formalize the core principles underlying the widest path-based BVI approach by (i) presenting 2WP-BVI, a clean BVI algorithm based on (2-player) widest path games, and (ii) proving its correctness using what we call the maximality inheritance principle--a proof principle previously employed in a well-known result in probabilistic model checking. Our experimental results demonstrate the practical relevance and potential of our proposed 2WP-BVI algorithm.

Speaker:

Kittiphon Phalakarn (National Institute of Informatics)

Talk 3:

Chance and Mass Interpretations of Probabilities in Markov Decision Processes

Abstract:

Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over cylinder sets of paths and policies or strategies making random choices. An alternative view, especially suited to dealing with dynamical systems and studied recently, is to define MDPs as distribution transformers with policies distributing probability masses.
In this paper, we examine both of these views and formulate a unified framework for MDP semantics which distinguishes two sources of randomness: in the scheduler and in transitions. The framework allows us to describe these different settings in a uniform manner by introducing the concept of pre-configuration and a function parameter called the CM classifier. Doing so, we obtain two new semantics: the (CS, MT) semantics where scheduler choices are probabilistic, while transitions are distributional; and the (MS, CT) semantics, where scheduler choices are distributional and transitions are probabilistic. We address the problem of reachability in both these settings. Surprisingly, reachability in the (CS, MT) semantics turns out to be undecidable, even when the target reachability sets are restricted to monotone (upward- or downward-closed) sets. We develop a sound, but necessarily incomplete, antichain-based algorithm for this semantics. For the (MS, CT) semantics, we show that reachability is #P-hard and generalize a template-based algorithm that synthesizes submartingales for reachability providing a sound and verifiable solution for solving reachability. We implement both algorithms and show their performance on a set of simple yet practical examples.