Determinizing Monitors for HML with Recursion

TL;DR

This paper proves that any monitor for HML with recursion can be transformed into an equivalent deterministic monitor with at most doubly exponential size, and explores the size differences when using process or automaton representations.

Contribution

It establishes the optimal doubly exponential bound for determinizing monitors and compares size efficiencies between process and automaton descriptions.

Findings

Determinization results in at most doubly exponential size increase.

Doubly exponential bound is tight for CCS-like process descriptions.

Finite automaton representations can be exponentially more succinct.

Abstract

We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (as their LTS), then they can be exponentially more succinct than their CCS process form.