23.6 Target for pushdown RBN

By Corto Mascle

Reconfigurable Broadcast Networks (RBN) are a model for large groups of identical agents communicating via unreliable broadcast. A pushdown RBN (PRBN) is simply one where each agent is modeled by a pushdown transition system. A PRBN on a message alphabet \(\mathcal{M}\) is described by a pushdown automaton \(\mathcal{A}\) over the alphabet \( \{br(m), rec(m) | m \in \mathcal{M} \}\). Configurations of \(\mathcal{A}\), i.e., pairs \((q, \sigma)\) of state and stack content, are called local configurations.\(\\ \)

A configuration of the PRBN is a function from a finite set of agents \(\mathbb{A}\) to local configurations. A run starts with an arbitrarily large set of agents, all in the initial state with an empty stack . A step consists of one agent taking a transition with a broadcast \(br(m)\), and each other agent either not moving or taking a transition \(rec(m)\) (in other words, one agent broadcasts and other agents non-deterministically receive the broadcast or not).\(\\ \)

Continue Reading →

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 →