Abstract:

Well-structured transition systems (WSTS) are a general class of infinite-state systems where termination, boundedness and coverability are decidable, using simple algorithms that work forwards and backwards. These algorithms cannot decide more complex problems like the place-boundedness problem and the computation of the cover (the downward closer of the reachability set).

To achieve this goal, we consider complete WSTS where the set of states is a complete well ordering (with other technical but realistic hypotheses).

We will then describe a simple, conceptual forward analysis procedure for infinite-complete WSTS. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set of X. We show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets.

We will first provide a survey about the theory of WSTS and then we will focus on complete WSTS.

Abstract: In recent years, several approaches have been proposed for automatic verification of infinite-state systems. In a parallel development, there has been an extensive research effort for the design and analysis of models with stochastic behaviors. We consider verification of Markov chains with infinite state spaces. We describe a general framework that can handle probabilistic versions of several classical models such as Petri nets, lossy channel systems, push-down automata, and noisy Turing machines. We consider both safety, liveness, and limiting behavior problems for these classes of systems. Furthermore, we describe algorithms to solve general versions of the problems in the context of stochastic games.

Abstract:

We propose a model that captures the behavior of real-time recursive systems. To that end, we introduce dense-timed pushdown automata that extend the classical models of pushdown automata and timed automata, in the sense that the automaton operates on a finite set of real-valued clocks, and each symbol in the stack is equipped with a real-valued clock representing its "age". The model induces a transition system that is infinite in two dimensions, namely it gives rise to a stack with an unbounded number of symbols each of which with a real-valued clock. The main contribution of the paper is an EXPTIME-complete algorithm for solving the reachability problem for dense-timed pushdown automata.

Abstract: We describe a common and uniform principle that explains the decidability of several decision problems. The main ingredient of our approach is representing *solutions* to the problem with labelled graphs that are definable in Monadic Second Order logic (MSO). For an appropriate graph encoding, it turns out that an instance of the problem has a positive answer if there is a solution whose graph representation has bounded tree-width. This allows us to reduce all those problems to the satisfiability problem of MSO on graphs of bounded tree-width (which is decidable due to Seese's theorem). We illustrate this approach for several decidable automata with auxiliary storage (stacks and queues) and for integer linear programming. We conclude with a conjecture whose positive answer will allow to extend this principle to a larger class of automata. (The material covered in this talk subsumes recent work conducted with P. Madhusudan, and Salvatore La Torre; as well as ongoing work with Constantin Enea, Omar Inverso, and Peter Habermehl)

Abstract: Classic and current theoretical solutions to the synthesis problem are focussed on synthesizing transition systems and not programs. Programs are compact and often the true aim in many synthesis problems, while the transition systems that correspond to them are often large and not very useful as synthesized artefacts. Consequently, current practical techniques first synthesize a transition system, and then extract a more compact representation from it. We reformulate the synthesis of reactive systems directly in terms of program synthesis, and develop a theory to show that the problem of synthesizing programs over a fixed set of Boolean variables in a simple imperative programming language is decidable for regular omega-specifications. We also present results for synthesizing programs with recursion against both regular specifications as well as visibly-pushdown language specifications. We also show applications to program repair, and conclude with open problems in synthesizing distributed programs. We end with a proposal of using Occam's razor and synthesis over bounded domains to achieve synthesis over unbounded domains.

Abstract: To be added.

Abstract: We will explore some restrictions on multi-pushdown systems that result in exponential-time algorithms for model checking linear time properties.

Abstract: Model checking is a powerful technique for analyzing reachability and temporal properties of finite state systems. But in case of infinite state systems, in general, the well known algorithms for model-checking of finite state systems need not terminate, even when applied to the reachability problem. Many practical systems can naturally be modeled as counter systems, where the domain of counter values is possibly infinite. In this work we identify a class of counter systems, and propose new techniques to check whether a system from this class satisfies a given CTL formula. The key novelty of our technique is that we are able to use reachability analysis techniques for counter systems, which are well-studied in the literature, as a subroutine in our CTL-checking algorithm. This enables us to work on a class of counter systems that is a strict superset of a current state-of-the-art approach.

Abstract: The Regular Post Embedding Problem (PEP) asks whether the intersection of a given rational relation with the embedding relation is nonempty. PEP is decidable but with very high complexity, F_{\omega^\omega} in the fast-growing hierarchy. PEP has close connections with reachability problems on lossy channel systems. A new proof of decidability of PEP bounds the length of the shortest solution by a computable function of the input, and shows decidability for a generalization of PEP. This generalization has applications to unidirectional lossy channel systems.