Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over time. In this paper, we study the verification of the evolution of conditional-independence (CI) propositions against temporal logic specifications. To this end, we consider two specification formalisms over CI propositions: linear temporal logic (LTL), and non-deterministic Büchi automata (NBAs). This problem has two variants. Stochastic CI properties take the given concrete probability distributions into account, while structural CI properties are viewed purely in terms of the graphical structure of the DBN. We show that deciding whether a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, which is a long-standing open problem in number theory. On the other hand, we show that verifying the evolution of structural CI propositions against LTL and NBA specifications is in PSPACE, and is hard for both NP and coNP. We also identify natural restrictions on the graphical structure of the DBN that make the verification of structural CI properties tractable.

The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs, which remained stubbornly open for a decade, was recently shown to be undecidable. In this article, we show that the Value Problem is decidable when considering two-clock almost non-Zeno wtgs.

Population protocols are a distributed computation model in which a collection of anonymous, finite-state agents interact in randomly chosen pairs and update their states according to a fixed transition function. The computation is defined by the eventual stabilization of the population to a consensus that represents the output. In practice, it is natural to allow each agent to carry a unique identifier and compare it with that of another agent before interacting. We model this extension by having agents be totally ordered and interactions between two agents to be fireable only if their pair of identifiers falls in some condition set. For instance, PP[<] allows for two agents to interact only if the first one appears before the second one. We study population protocols over ordered agents PP[𝒩] where 𝒩 is a set of predicates available to restrict transition firing. We also study IO-PP[𝒩], the immediate observation fragment of PP[𝒩] where only one agent changes state per interaction. Our main result is that IO-PP[<] recognizes exactly the unambiguous star-free languages, which admits many other characterizations, such as two-variable first-order logic or two-way deterministic partially-ordered automata. We also provide a logic and an automaton model that fits in PP[<]. We further show that if the successor predicate appears in a set 𝒩 of NSPACE(n)-computable predicates, then IO-PP[𝒩] = PP[𝒩] = NSPACE(n). Finally, we investigate the problem of deciding whether a given population protocol always stabilizes to a consensus. While this problem is decidable for unordered population protocols, we show that this is undecidable already for PP[<] and IO-PP[+1], but conditionally decidable for IO-PP[<].

We express the piecewise complexity of words using tools and concepts from tropical algebra. This allows us to define a notion of piecewise signature of a word that has size log(n)m^{O(1)} where m is the alphabet size and n is the length of the word. The piecewise signature of a concatenation can be computed from the signatures of its components, allowing a polynomial-time algorithm for computing the piecewise complexity of SLP-compressed words.

Well-partial orders, and the ordinal invariants used to measure them, are relevant in set theory, program verification, proof theory and many other areas of computer science and mathematics. In this article we focus on a common data structure in programming, finite multisets of some well partial order. There are two natural orders one can define on the set of finite multisets of a partial order: the multiset embedding and the multiset ordering. Though the maximal order type of these orders is already known, other ordinal invariants remain mostly unknown. Our main contributions are expressions to compute compositionally the width of the multiset embedding and the height of the multiset ordering. Furthermore, we provide a new ordinal invariant useful for characterizing the width of the multiset ordering.