Time 
Speaker 
Affiliation 
Title and Abstract 
9:00am 
Alain Finkel 
ENS Cachan 
The Theory of Complete WSTS 
Abstract:
Wellstructured transition systems (WSTS) are a general class of
infinitestate 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
placeboundedness 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 infinitecomplete WSTS. This computes the socalled 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
KarpMiller 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.

9:45am 
Parosh Aziz Abdulla 
Uppsala University 
Infinite State Probabilistic Systems

Abstract:
In recent years, several approaches have been proposed for automatic
verification of infinitestate 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,
pushdown 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.

10:30am 
Tea/Coffee Break 
11:00am 
Mohamed Faouzi Atig 
Uppsala University 
DenseTimed Pushdown Automata

Abstract:
We propose a model that captures the behavior of realtime
recursive systems. To that end, we introduce densetimed 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 realvalued clocks, and each symbol in the stack is
equipped with a realvalued 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 realvalued clock. The
main contribution of the paper is an EXPTIMEcomplete algorithm
for solving the reachability problem for densetimed pushdown
automata.

11:45am 
Gennaro Parlato 
University of Southampton 
The TreeWidth of Decidable Problems 
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 treewidth. This allows us to reduce all
those problems to the satisfiability problem of MSO on graphs of bounded
treewidth (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)

12:30pm 
Lunch 
2:00pm 
Madhusudan Parthasarathy 
University of Illinois, UrbanaChampaign 
Synthesizing Programs over Bounded Data Domains 
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 ﬁrst 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 omegaspecifications. We
also present results for synthesizing programs with recursion against both regular
specifications as well as visiblypushdown 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.

2:45pm 
Nishant Sinha 
IBM Research, Bangalore 
Bigstep, Goaldriven Bounded ModelChecking for Software.

Abstract: To be added.

3:30pm 
Tea/Coffee Break 
3:50pm 
Prakash Saivasan 
Chennai Mathematical Institute 
Verifying multipushdown systems

Abstract: We will explore some restrictions on multipushdown systems
that result in exponentialtime algorithms for model checking linear
time properties.

4:20pm 
K. Vasanta 
Indian Institute of Science, Bangalore 
Modelchecking Presburger Counter Systems Using Accelerations

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 modelchecking 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 wellstudied in the
literature, as a subroutine in our CTLchecking algorithm. This enables us
to work on a class of counter systems that is a strict superset of a
current stateoftheart approach.

4:50pm 
Prateek
Karandikar 
Chennai Mathematical Institute 
An introduction to the Post Embedding Problem

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 fastgrowing 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.
