Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

History-Constrained Systems

Louwe B. Kuijer, David Purser, Henry Sinclair-Banks, Patrick Totzke

TL;DR

This work considers HCS with guards of greater expressive power, Vector Addition Systems with States (VASS), and shows that with deterministic coverability-VASS guards the reachability problem is EXPSPACE-complete, while with reachability-VASS the problem is undecidable.

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 $ω$-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.

History-Constrained Systems

TL;DR

This work considers HCS with guards of greater expressive power, Vector Addition Systems with States (VASS), and shows that with deterministic coverability-VASS guards the reachability problem is EXPSPACE-complete, while with reachability-VASS the problem is undecidable.

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 -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.
Paper Structure (13 sections, 1 theorem, 3 figures)

This paper contains 13 sections, 1 theorem, 3 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Regular guards.
  4. Guards with counters.
  5. Related work
  6. Preliminaries
  7. History-Constrained Systems
  8. Finite Automata
  9. HCS Specified with Finite Automata
  10. Emptiness and Reachability
  11. Examples
  12. Expressivity of HCS
  13. The Expressivity of Regular Guards

Key Result

theorem thmcountertheorem

Given an NFA[NFA] $A$, we can construct an exponential size DFA $D$ such that $L(D) = L(A)$.

Figures (3)

  • Figure 1: Three layer HCS traffic light model. The outer system is a single state to hold each controller; "T1:*" represents all actions for traffic light 1. The middle layer represents the controller of each individual traffic light (the full mechanism of the traffic light controller (grey edges) is not depicted). The innermost system guards the "turn green" commands to ensure that the other set of lights have turned to red. The system enforces safety by ensuring that whenever a traffic light attempts to turn green, the other traffic light has turned to red. Unlabelled self-loops represent all actions other than those specified.
  • Figure 2: Four-eyes approval workflow represented as both an HCS (left) and as a finite automaton (right). Approvals arrive in an unknown order, the finite automaton must explicitly encode this in the state, while the HCS can store this information on just the relevant edges. Three approvers would enlarge the finite automaton significantly, while the HCS needs just one more guarded transition. Unlabelled self-loops represent all actions other than those specified.
  • Figure 3: Examples $U_1$ and $U_2$ sharing guards $L_1$, $L_2$, and $L_3$. Whenever we do not specify a guard, then one should assume we use the trivial guard $L_t = \Sigma^*$.

Theorems & Definitions (1)

  • theorem thmcountertheorem