History-Constrained Systems

TL;DR

This paper investigates verification problems for history-constrained systems, modeling guarded nested computations, and analyzes their expressive power, game-solving complexity, and extensions with advanced guards like VASS.

Contribution

It characterizes the expressive power of HCS, analyzes the complexity of game solving, and explores the decidability of reachability with VASS guards.

Findings

HCS with finite automata guards are as expressive as regular languages but more succinct.

Solving games on HCS is EXPTIME-complete for omega-regular conditions.

Reachability with deterministic VASS guards is EXPSPACE-complete; undecidable with reachability-VASS.

Abstract

We study verification problems for history-constrained systems (HCS), a model of guarded computation that uses nested systems. An outer system describes the process architecture in which a sequence of actions represents the communication between sub-systems through a global bus. Actions are either permitted or blocked locally by guards; these guards read and decide based on the sequence of actions so far in the global bus. When HCS have both the outer systems and the local guard controllers modelled by finite automata, we show they have the same expressive power as regular languages and finite automata, but they are exponentially more succinct. We also analyse games on this model, representing the interaction between environment and controller, and show that solving such games is EXPTIME-complete, where the lower bound already holds for reachability/safety games and the upper bound holds for any $\omega$-regular winning condition. Finally, we consider HCS with guards of greater expressive power, Vector Addition Systems with States (VASS). We show that with deterministic coverability-VASS guards the reachability problem is EXPSPACE-complete, while with reachability-VASS the problem is undecidable.