23.3 Reachability problem for thin 1-GVASS

By Wojciech Czerwiński

The reachability problem for 1-dimensional Pushdown Vector Addition Systems (1-PVASS) is a big open problem. Here I propose another problem, which seems much simpler, but hopefully can shed a light into reachability of 1-PVASS. Instead of 1-PVASS we consider 1-dimensional Grammar Vector Addition Systems, (1-GVASS) which are equivalent wrt. the reachability problem to 1-PVASS.

The problem is formulated as follows: we are given a context-free grammar G with terminals being integers and two natural numbers a, b. The question is whether there exists a witness word \(w \in Z^*\) such that:

  1. for each prefix v of w the expression (a + the sum of letters of v) is nonnegative;
  2. a + sum of letters of w = b.

Continue Reading →

23.4 Bounds on the length of a coverability path in VASS

By Wojciech Czerwiński

By the classic Rackoff argument in d-dimensional Vector Addition System with States (d-VASS) V if there is a path starting in configuration s and covering configuration t then there is also a covering path of length at most Mk, where M is the maximal number occurring on transitions of VASS and in configurations s and t, while \(k \approx 2^d\). Therefore for each fixed d there is a path of length polynomial in M.

We conjecture that a much stronger property holds, that there is always a covering path of length \(f(size(V)) \cdot (size(s) + size(t)\), namely depending in some way on the size of VASS V, but only linear with respect to the size of source s and target t.

I think this conjecture is hard to prove despite of a simple formulation and progress on it could led to a deep understanding of runs of VASS.

23.1 TARGET in asynchronous shared-memory systems

By Nicolas Waldburger

An asynchronous shared-memory system is composed of \(n\) processes that interact by reading from and writing to a shared memory. This shared memory is composed of \(r\) registers, each containing one symbol at a time from the finite alphabet \(D\). All processes are anonymous and identical; they are described by the same finite automaton, called protocol. The transitions of the automaton are labelled by actions of the form \(read_i(d)\) or \(write_i(d)\) with \(i \in \{1,\dots,r\}\) and \(d \in D\).

Continue Reading →

23.5 Linear loop synthesis: When d variables are not enough.

By Anton Varonka

Linear loops (or linear dynamical systems) are an established computational model in our community. We typically understand under a linear loop a simple while loop with a single linear update as shown next.

\[\textbf{x}:= \textbf{s}; \; while \; true \; do \; \textbf{x} := M \cdot \textbf{x};\]

Here, \(\textbf{x} = (x_1, \dots, x_d)\) is a vector of rational-valued loop variables and the matrix \(M \in \mathbb{Q}^{d \times d}\) denotes a linear transformation of \(\mathbb{Q}^d\).

In the loop synthesis problem, a polynomial \(p \in \mathbb{Q}[x_1, \dots, x_d]\) in \(d\) variables is given. The goal is to generate a linear loop (that is, both the update matrix \(M\) and the initialisation vector \(s\)) such that \(p(x_1(n), \dots, x_d(n)) = 0\) holds after \(n\)-th iteration of the loop for all \(n \in \mathbb{N}\).

Continue Reading →

23.2 $o(n^2)$-time algorithm for coverability in 1-VASS

By Henry Sinclair-Banks

A 1-dimensional Vector Addition System with States (1-VASS) can be seen as an directed and integer weighted graph that is equipped with a non-negative integer counter.

A configuration of a 1-VASS is a pair $(q, x)$ that is the current node $q$ and the current non-negative counter value $x$.

A run in a 1-VASS is a sequence of configurations $(q_0, x_0), (q_1, x_1), \ldots, (q_k, x_k)$ where for each $i \in \{ 1, \ldots, k\}$, there is an edge from $x_{i-1}$ to $x_i$ with weight $x_i - x_{i-1}$.

Continue Reading →

22.1 Complexity of fixed VAS reachability

By Ismaël Jecker

A vector addition system is a finite set of vectors $V = \{ v_1,v_2,\ldots,v_n \} \in \mathbb{Z}^d$ with $d \in \mathbb{N}$. Given two positions $s,t \in \mathbb{N}^d$, a run of $V$ from $s$ to $t$ is a sequence $s = c_0, c_1, c_2, \ldots, c_m = t$ of positions $c_i \in \mathbb{N}^d$ where each position is obtained by adding an element of $V$ to the previous one: $c_{i} - c_{i-1} \in V$ for every $1 \leq i \leq m$. Is the following statement correct:

Conjecture: For every vector addition system $V$, there exists a constant $C_V$ such that for every pair of positions $s$ and $t$, if there exists at least one run of $V$ from $s$ to $t$, one of these runs has a length smaller than $C_V \cdot \big(||s|| + ||t|| \big)$.

22.2 Paired Counter Automata

By Andrei Draghici

Consider a DFA $A$ together with $d$ pairs off counters $(x_1,y_1),\dots,(x_d,y_d)$. Each transition of $A$ is labelled with an update function for all counters. The update functions for the x-counters are $id:n\rightarrow n$ and $++ : n\rightarrow n+1$. The update function for the y-counters are $id:n\rightarrow n$, $\times 2:n\rightarrow 2n$ and $\times 2+1:n\rightarrow 2n+1$. An accepting configuration is a configuration in which we are in an accepting state and all the counter pairs have the same value, i.e. $x_1=y_1,\dots,x_d=y_d$.

Question: is the emptiness problem for this class of automata decidable?

22.3 Universal coverability for Orthant VAS

By David Purser

An orthant is a region in $\mathbb{R}^d$ in which every vector in the orthant has the same sign in each dimension. In a vector addition system sum vectors taken non-deterministically from a given set, providing the sum remains in the positive orthant (all vectors positive). Z-VAS can visit all orthants, but the set of vectors that can be applied is the same in every orthant.

An orthant VAS has a different set of vectors for each orthant. Any vector from the set of the current orthant can be applied, the result of which may be in the same orthant, or another orthant.

Continue Reading →

22.4 Reconfigurable broadcast networks (RBN)

By Chana Weil-Kennedy

Reconfigurable broadcast networks (RBN) are networks consisting of finite-state, anonymous agents that communicate by broadcast. An agent broadcasts a message which is received by its neighbors (one step is a broadcast plus multiple simultaneous receives). The neighbor topology can change (reconfigure) between any step.

Continue Reading →

22.5 Decidability of $(\min,+)$-weighted automata determinization

By Shaull Almagor

Is the following problem decidable: Given $A$, a weighted automaton (WA) over the $(\min,+)$ semiring, answer whether $A$ has an equivalent deterministic WA?

Remarks: The problem is equivalent when considering only automata with weights in $\{0,1\}$ (a.k.a. distance automata). The problem is known to be decidable for polynomially-ambiguous WA. For the general case of exponentially-ambiguous WA, we don't even have any interesting examples where determinization incurs a significant state explosion.