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 →

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 →

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 →

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 →

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 →

Let $A$ be an automaton and write, for any word $w$, $f_w$ for the function that maps any state $q$ to the state reached by reaching $w$ from $q$.

The membership problem MEMB($V$) for a class $V$ of deterministic automata is the following:

• Given: An automaton $A \in V$ and a function $f\colon Q \to Q$ from states to states
• Question: Is there a word $w$ such that $f_w = f$?

In the late 1980s, Beaudry, together with McKenzie and Thérien, studied the problem for most natural classes $V$ (e.g., groups and aperiodic automata). Quoting Beaudry, McKenzie, Thérien, 1992:

"For each $V$ aperiodic, the computational complexity of MEMB($V$) turns out to look familiar. Only five possibilities occur as $V$ ranges over the whole aperiodic sublattice: With one family of NP-hard exceptions whose exact status is still unresolved, any such MEMB($V$) is either PSPACE-complete, NP-complete, P-complete or in AC$⁰$."

Continue Reading →

The following is a problem inspired from quantitative program verification. It is more vague than ``Prove or disprove whether XYZ holds'', but in turn has real applications in probabilistic verification. I posed this problem several times to several different machine learning experts and none of them were able (or interested) to help me with this problem. I now hope that the automata (learning) experts can help me out.

Continue Reading →