ABSTRACT. Linear recurrence sequences (LRS), such as the Fibonacci numbers, permeate vast areas of mathematics and computer science. In this talk, we consider three natural decision problems for LRS, namely the Skolem Problem (does a given LRS have a zero?), the Positivity Problem (are all terms of a given LRS positive?), and the Ultimate Positivity Problem (are all but finitely many terms of a given LRS positive?). Such problems (and assorted variants) have applications in a wide array of scientific areas, such as theoretical biology (analysis of L-systems, population dynamics), economics (stability of supply-and-demand equilibria in cyclical markets, multiplier-accelerator models), software verification (termination of linear programs), probabilistic model checking (reachability and approximation in Markov chains, stochastic logics), quantum computing (threshold problems for quantum automata), discrete linear dynamical systems (reachability and invariance problems), as well as combinatorics, statistical physics, formal languages, etc.

ABSTRACT. Distributed systems are often parameterized by the number of participating processes, and thus the parameterized model checking problem is equivalent to model checking an infinite state system. A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finite-state systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Buchi word automaton), and establish tight bounds on the sizes of such automata.

ABSTRACT. We investigate the complexity of the model checking problem for local temporal logics and communicating finite-state machines (CFMs). The input is a number of processes π, a temporal formula F, a CFM C, and a bound β on the maximal number of pending messages allowed. The question is whether all message sequence charts (MSCs) which are accepted by C and for which there exists an execution with β-bounded channels fulfill F.

We show that this problem can be solved in space polynomial in C, β, and F and exponential in π regarding temporal logics consisting of the usual modalities used in the context of concurrent systems.

We also state that if the modalities of the underlying temporal logic can be defined using formulas from the n-th level of the monadic quantifier alternation hierarchy, the uniform model checking problem (where the temporal logic is part of the input) is hard for (n+1)-fold exponential space and can be solved in (n+3)-fold exponential space. If we fix the temporal logic and the number of processes, we obtain matching upper and lower bounds.

ABSTRACT. We consider decision problems for deterministic pushdown automata over the unary alphabet (udpda, for short). Udpda are a simple computation model that accept exactly the unary regular languages, but can be exponentially more succinct than finite-state automata.

We complete the complexity landscape for udpda by showing that emptiness (and thus universality) is P-hard, equivalence and compressed membership problems are P-complete, and inclusion is coNP-complete. Our upper bounds are based on a translation theorem between udpda and straight-line programs over the binary alphabet (SLPs). We show that the characteristic sequence of any udpda can be represented as a pair of SLPs---one for the prefix, one for the lasso---that have size linear in the size of the udpda and can be computed in polynomial time. Hence, decision problems on udpda are reduced to decision problems on SLPs. Conversely, any SLP can be converted in logarithmic space into a udpda, and this forms the basis for our lower bound proofs. We show coNP-hardness of the ordered matching problem for SLPs, from which we derive coNP-hardness for inclusion. In addition, we complete the complexity landscape for unary nondeterministic pushdown automata by showing that the universality problem is Pi2P-hard, using a new class of integer expressions.

Our techniques have applications beyond udpda. We show that our results imply Pi2P-completeness for a natural fragment of Presburger arithmetic and coNP lower bounds for compressed matching problems with one-character wildcards.

ABSTRACT. Recent work on automata with abstract storage revealed a class of storage mechanisms that proves quite expressive and amenable to various kinds of algorithmic analysis. The storage mechanisms in this class are obtained by \emph{building stacks} and \emph{adding blind counters}.

The former is to construct a new mechanism that stores a stack whose entries are configurations of an old mechanism. One can then manipulate the topmost entry, pop it if empty, or start a new one on top. Adding a blind counter to an old mechanism yields a new mechanism in which the old one and a blind counter can be used simultaneously. We call the resulting model \emph{stacked counter automaton}.

This talk presents results on expressivity, Parikh images, membership problems, and the computability of downward closures.

ABSTRACT. Roughly speaking a finite automaton on infinite trees is a finite memory machine that takes as input an infinite node-labelled binary tree and processes it in a top-down fashion as follows. It starts at the root of the tree in its initial state, and picks (possibly nondeterministically) two successor states, one per son, according to the current control state, the letter at the current node and the transition relation. Then the computation proceeds in parallel from both sons, and so on. Hence, a run of the automaton on an input tree is a labelling of this tree by control states of the automaton, that should satisfy the local constrains imposed by the transition relation. A branch in a run is accepting if the omega-word obtained by reading the states along the branch satisfies some acceptance condition (typically an omega-regular condition such as a Büchi or a parity condition). A run is accepting if *all* branches are accepting. Finally, a tree is accepted by the automaton if *there exists* an accepting run over this tree. Hence, there are three natural levers on which one can act to define alternative families of tree automata / tree languages. - The first lever is local with respect to the run: it is the conditionrequired for a branch to be accepting. - The second lever is global with respect to the run: it is the condition required for a run to be accepting. - The third lever has to do with the set of runs: it is the condition required for a tree to be accepted (wrt the set of runs over it). For the usual definition of tree automata the three lever are: parity condition on branches / all branches accepting for run / there exists an accepting run. In this talk I will mainly focus on the second and third levers and propose variants of them. More precisely (time depending): - second lever: count the number of accepting/rejecting branches (cardinality constraint), topologically measure the largeness of the set of accepting/rejecting branches, measure (à la Lebesgue) the set of accepting/rejecting branches. - third lever (possibly combined with the second lever): alternating and probabilistic models. I will explain how decidability results can be obtained by extending the well-known equivalence between games and tree automata (that I will recall first!). This will lead us, in several situations, to leave the usual than perfect-information turn based two-player framework: in particular we will have to deal with stochastic aspects and/or imperfect information.

ABSTRACT. see pdf

ABSTRACT. Abstract is in the pdf file. My submission is quiet unusual, as I propose 2 topics (closely related). I hope that one of them will suit to this year AISS programme.

ABSTRACT. One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.