Aim and Scope

Program (titles and authors)

Visa issues

Scientific Committee

Program (incl. abstracts)

Accomodation

Sponsors

Schedule of talks

Travel support

Aim and Scope

The scientific scope of this Workshop is described in its title. It is the concluding meeting of the 4-year Indo-French project Timed-Discoveri, jointly funded by CNRS, the Foreign Affairs Ministry (France) and the Department of Science and Technology (Government of India). However, this meeting is open to all, whether they participated in the project's actions or not, and whether they are based in France, in India or elsewhere.

Program (click here for more details)

Dietmar Berwanger (LSV, ENS Cachan) The order of moves in a game: When does it matter?
Benedikt Bollig (LSV, ENS Cachan) Realizability of Concurrent Recursive Programs (Slides)
Patricia Bouyer (LSV, ENS Cachan) Quantitative timed games (Slides)
Philippe Darondeau (INRIA Rennes). Opacity control (Slides)
Volker Diekert (FMI, Stuttgart) Fragments of first-order logic over infinite words (Slides)
Deepak D'Souza (IISc Bangalore) Automata and Logics over Signals (Slides)
Paul Gastin (LSV, ENS Cachan). How to get decidability of distributed synthesis for asynchronous systems (Slides)(Handout)
Hugo Gimbert (LaBRI, U. Bordeaux) Qualitative Determinacy and Decidability of Stochastic Games with Partial Observation (Slides)
Stefan Haar (LSV, ENS Cachan). Diagnosability and a covering relation in occurrence nets (Slides)
Hrishikesh Karmakar (IIT Bombay). Improved state-count for determinization of non-deterministic Buchi automata: A Safra-tree based approach (Slides)
K. Narayan Kumar (CMI, Chennai) Analyzing time-constrained message sequence graphs (Slides)
Dietrich Kuske (IfI, Leipzig) Which local temporal logics for traces are tractable? (Slides)
Kamal Lodaya (IMSc, Chennai) Around dot-depth two (Slides)
Anca Muscholl (LaBRI, U. Bordeaux) A look at the control of asynchronous automata (Slides)
Joël Ouaknine (Computing Lab, Oxford). Time-Bounded Verification (J. Ouaknine unfortunately had to cancel his trip)
Paritosh Pandya (TIFR, Mumbai) A Sampling Approach to the Analysis of Metric Temporal Logic (Slides)
Soumya Paul (IMSc, Chennai). Thiagarajan's conjecture (Slides)
M. Praveen (IMSc, Chennai). Petri nets with small path property (Slides)
R. Ramanujam (IMSc, Chennai) Counting multiplicity over infinite alphabets (Slides)
Abhisekh Sankaran (IIT Bombay). A FOL Fragment for Safety Checking in Infinite State Systems (Slides)
Anil Seth (IIT, Kanpur). Parity Games on Multi-Stack Pushdown Systems
Vijay Suman (TIFR Bombay). Determinization and Expressiveness of Integer Reset Timed Automata with Silent Transitions (Slides)
Pascal Weil (LaBRI, U. Bordeaux) Independence monoids and recognizable trace languages (Slides)
Marc Zeitoun (LaBRI, U. Bordeaux) Tree Pattern Rewriting Systems (Slides)
Wiesiek Zielonka (LIAFA, Paris). Positional equilibria in infinite perfect information games (Slides)

Schedule of talks

Thursday 29 January 2009

09:30. Opening of the workshop
09:40. Paul Gastin (LSV, ENS Cachan). How to get decidability of distributed synthesis for asynchronous systems

10:20. Philippe Darondeau (INRIA, Rennes) Opacity control
11:00. coffee break
11:30. Soumya Paul (IMSc, Chennai). Thiagarajan's conjecture

12:00. Stefan Haar (LSV, ENS Cachan). Diagnosability and a covering relation in occurrence nets


12:40. Lunch

14:30. R. Ramanujam (IMSc, Chennai) Counting multiplicity over infinite alphabets

15:10. Vijay Suman (TIFR Bombay). Determinization and Expressiveness of Integer Reset Timed Automata with Silent Transitions

15:40. coffee break
16:10. Deepak D'Souza (IISc Bangalore) Automata and Logics over Signals

16:50. Paritosh Pandya (TIFR, Mumbai) A Sampling Approach to the Analysis of Metric Temporal Logic


17:30. Day ends.

Friday 30 January

09:30. K. Narayan Kumar (CMI, Chennai) Analyzing time-constrained message sequence graphs

10:10. Patricia Bouyer (LSV, ENS Cachan) Quantitative timed games

10:50. coffee break
11:10. Dietmar Berwanger (LSV, ENS Cachan) The order of moves in a game: When does it matter?

11:50. Wiesiek Zielonka (LIAFA, Paris). Positional equilibria in infinite perfect information games

12:30. Lunch

14:30. Anil Seth (IIT, Kanpur). Parity Games on Multi-Stack Pushdown Systems

15:10. Hugo Gimbert (LaBRI, U. Bordeaux) Qualitative Determinacy and Decidability of Stochastic Games with Partial Observation


15:50. coffee break
16:20. Hrishikesh Karmakar (IIT Bombay). Improved state-count for determinization of non-deterministic Buchi automata: A Safra-tree based approach

16:50. Abhisekh Sankaran (IIT Bombay). A FOL Fragment for Safety Checking in Infinite State Systems

17:20. Talks end, conference dinner will follow.

Saturday 31 January
09:30. Anca Muscholl (LaBRI, U. Bordeaux) A look at the control of asynchronous automata

10:10. Benedikt Bollig (LSV, ENS Cachan) Realizability of Concurrent Recursive Programs

10:50. M. Praveen (IMSc, Chennai). Petri nets with small path property

11:20. coffee break
11:40. Dietrich Kuske (IfI, Leipzig) Which local temporal logics for traces are tractable?
12:20. Pascal Weil (LaBRI, U. Bordeaux) Independence monoids and recognizable trace languages


13:00. Lunch

14:30. Volker Diekert (FMI, Stuttgart) Fragments of first-order logic over infinite words

15:10. Kamal Lodaya (IMSc, Chennai) Around dot-depth two


15:50. coffee break
16:20. Marc Zeitoun (LaBRI, U. Bordeaux) Tree Pattern Rewriting Systems
17:00. Workshop ends.

Scientific Committee

Patricia Bouyer (LSV, ENS Cachan)
Deepak D'Souza (CSA, IISc Bangalore)
Paul Gastin (LSV, ENS Cachan)
Kamal Lodaya (IMSc, Chennai)
K. Narayan Kumar (CMI, Chennai)
Madhavan Mukund (CMI, Chennai, co-chair)
Igor Walukiewicz (LaBRI, U. Bordeaux)
Pascal Weil (LaBRI, U. Bordeaux, co-chair)

Sponsors

The workshop is sponsored by

Detailed program

Dietmar Berwanger (LSV, ENS Cachan) The order of moves in a game: When does it matter?
Noncooperative game theory features two basic models of interaction which reflect extremal views on the order of moves in a play. In strategic games, all players choose their strategy simultaneously, whereas in extensive games, they move sequentially. However, due to imperfect information, players may be uncertain about the outcome of a previous move; this allows to model a sequence of moves as if it was executed simultaneously.
In this talk, we address the following question: which sequences of moves in an extensive game can be viewed as inherently simultaneous? We survey classical approaches for answering this question, based on Thomson transformations and the concept of effectivity-function equivalence. We discuss extensions and applications of these techniques to infinite games on graphs.

Benedikt Bollig (LSV, ENS Cachan). Realizability of Concurrent Recursive Programs
(Joint work with Manuela-Lidia Grindei and Peter Habermehl.)
In this talk, we present concurrent visibly pushdown automata (CVPA), a combination of visibly pushdown automata and Zielonka's asynchronous automata: local processes, each modeled as a visibly pushdown automaton, synchronize by executing certain actions (e.g., writing a global variable) simultaneously, whereas others may be taken autonomously. CVPA are actually a special case of multi-stack visibly pushdown automata (MVPA) as introduced and studied recently by La Torre, Madhusudan, and Parlato, who show that MVPA constitute a robust class of context-sensitive languages when restricting the domain of input words to certain k-phase executions.
We consider CVPA as a model of concurrent recursive programs and MVPA as specifications. Thus, we are interested in transforming an MVPA into an equivalent CVPA, if possible. Indeed, one can lift Zielonka's theorem to the recursive setting: for every MVPA language L that is closed under permutation rewriting of independent actions, there is a CVPA A such that L(A) = L. Unfortunately, it is in general undecidable if L is closed in this way. We will therefore restrict a specification to k-phase executions, which can be decomposed into k phases having all processes able to evolve in each phase but only one process can return from a procedure. In this restricted setting, we identify a decidable sufficient criterion that guarantees that the closure of the specification can be recognized by a CVPA. The same restriction also permits a logical characterization of CVPA in terms of an MSO logic over nested traces, which are Mazurkiewicz traces equipped with multiple nesting relations.

Patricia Bouyer (LSV, ENS Cachan). Quantitative timed games
In this talk I will present the model of weighted timed games, which is used to represent resources (like energy or cost) in timed systems. I will give an overview of the results that have been obtained these last couple of years, that concern the optimization and the management of those resources.

Philippe Darondeau (INRIA Rennes). Opacity Control
(Joint work with E. Badouel, M. Bednarczyk, A. Borzyskowski, B. Caillaud, J. Dubreil, H. Marchand)
Given a transition system G labelled on Σ, a subset S of L(G) is opaque w.r.t. a subalphabet Σ' if all projections of words of S on Σ' coincide with projections of words of L(G)\S on Σ'. Thus, if S is opaque, the fact that the current trajectory of G belongs to S is not revealed to an inquisitive user who observes the actions in Σ'. The notion of opacity was introduced by Laurent Mazare. The general problem which we address is the control of opacity. The main difficulty arises from the assumption that G and any controller possibly set on G are known to the external user(s). We dealt up to now with two subproblems as follows.
In the first case, we consider several secret sets Si and subalphabets Σ'i, but we suppose that all actions in Σ are observed and may be controlled by the controller. We state sufficient conditions under which one can compute the most permissive controller enforcing jointly the opacity of all secret sets Si w.r.t. the corresponding subalphabets Σ'i.
In the second case, we consider a single secret S and a single alphabet Σ', but we suppose that the supervisor can observe, resp. control specific subsets Σo and Σc, respectively of Σ and Σo. We show that if L(G) and S are regular and Σ' is a subset of Σo, then the most permissive controller enforcing the opacity of S is regular and effectively computable.
We finally discuss how both approaches could be combined and what kinds of problems might be investigated in future works.

Volker Diekert (FMI, Stuttgart). Fragments of first-order logic over infinite words
(Joint work with Manfred Kufleitner)
We give topological and algebraic characterizations as well as language theoretic descriptions of the following subclasses of first-order logic for languages over infinite words: Σ2, Δ2, FO2 ∩ Σ2 (and by duality FO2 ∩ Π2), and FO2. These descriptions extend the respective results for finite words. Our characterizations combine algebraic, topological, and language theoretic properties. In particular, we relate the above fragments to language classes of certain (unambiguous) polynomials.

Deepak D'Souza (IISc Bangalore). Automata and Logics over Signals
We extend some of the classical connections between automata and logic due to Buchi and McNaughton and Papert, to languages of finitely varying functions or "signals". In particular we introduce a natural class of automata for generating signals called ST-NFA's, and show that it coincides in terms of language-definability with a natural monadic second-order logic interpreted over finitely varying functions. We also identify a "counter-free" subclass of ST-NFA's which characterize the first-order definable languages of finitely varying functions. Our proofs mainly factor through the classical results for word languages. These results have applications in automata characterisations for continuously interpreted real-time logics like Metric Temporal Logic (MTL).

Paul Gastin (LSV, ENS Cachan). How to get decidability of distributed synthesis for asynchronous systems
We study the synthesis problem in an asynchronous distributed setting: a finite set of processes interact locally with an uncontrollable environment and communicate with each other by sending signals -- actions that are immediately received by the target process. The synthesis problem is to come up with a local strategy for each process such that the resulting behaviours of the system meet a given specification. We consider external specifications over partial orders. External means that specifications only relate input and output actions from and to the environment and not signals exchanged by processes. We also ask for some closure properties of the specification. We present this new setting for studying the distributed synthesis problem, and give decidability results: the non-distributed case, and the subclass of networks where communication happens through a strongly connected graph. We believe that this framework for distributed synthesis yields decidability results for many more architectures.

Hugo Gimbert (LaBRI, U. Bordeaux). Qualitative Determinacy and Decidability of Stochastic Games with Partial Observation
(Joint work with Nathalie Bertrand and Blaise Genest.)
We consider the standard model of finite two-person zero-sum stochastic games with signals. We are interested in the existence of almost-surely winning or positively winning strategies, under reachability, safety, Buchi or co-Buchi winning objectives.
We prove two qualitative determinacy results. First, in a reachability game either player 1 can achieve almost surely the reachability objective, or player 2 can ensure almost surely the complimentary safety objective, or both players have positively winning strategies. Second, in a Buchi game if player 1 cannot achieve almost surely the Buchi objective, then player 2 can ensure positively the complimentary co-Buchi objective.
We prove that players only need strategies with finite-memory, whose sizes range from no memory at all to doubly-exponential size, with matching lower bounds. We provide fix-point algorithms to decide which player has an almost surely winning or positive winning strategy and compute the finite memory strategy. Complexity ranges from EXPTIME to 2EXPTIME with matching lower bounds, and better complexity can be achieved for some special cases where one of the players is better informed than her opponent.

Stefan Haar (LSV, ENS Cachan). Diagnosability and a covering relation in occurrence nets
In the context of asynchronous fault diagnosis for large networks, [Benveniste/Fabre/Jard/Haar 2003] introduced a methodology that uses alarm-labeled Petri net unfoldings for on-line computation of nonsequential behaviours that explain the observed alarm patterns. Following this approach, the diagnosability problem consists in deciding whether the system's visible events - i.e. whose labels are observable - suffice to determine whether or not a given invisible fault has occurred. The talk will discuss methods for analyzing asynchronous diagnosability, and concentrate on how the structure of occurrence nets can be used. We say that event a covers event b iff every run containing a must contain b, be it prior to, posterior to, or concurrent with a, and show how the covering relation can be effectively computed; work in progress on the subject will be presented.

Hrishikesh Karmakar (IIT Bombay). Improved state-count for determinization of non-deterministic Buchi automata: A Safra-tree based approach
We present a determinization scheme, which constructs a deterministic parity automaton equivalent to a given non-deterministic Buchi automaton. Our approach to determinization uses a modified version of the trees used by Safra in his celebrated determinization construction. We introduce a new tree compaction procedure under which vertices in modified Safra trees are reordered, without compromising on correctness of the determinization construction. As a consequence of this tree compaction, we demonstrate that node names in modified Safra trees depend on the positions of nodes in a certain natural total ordering of the nodes and thus can be inferred without the need to store node names explicitly in states of the deterministic parity automaton. This can be thought of as a new node naming scheme similar to but better than Piterman's node naming scheme for Safra trees. As a result, we demonstrate a determinization construction for non-deterministic Buchi automata that is asymptotically better than Piterman's variant of the Safra construction.

K. Narayan Kumar (CMI, Chennai). Analyzing time-constrained message sequence graphs
(Joint work with Paul Gastin and Madhavan Mukund)
Channel boundedness is a necessary condition for a message-passing system to exhibit regular, finite-state behaviour at the global level. For Message Sequence Graphs (MSGs), the most basic form of High-level Message Sequence Charts (HMSCs), channel boundedness can be characterized in terms of structural conditions on the underlying graph. We consider MSGs enriched with timing constraints between events. These constraints restrict the global behaviour and can impose channel boundedness even when it is not guaranteed by the graph structure of the MSG. We show that we can use MSGs with timing constraints to simulate computations of a two-counter machine. As a consequence, even the more fundamental problem of reachability, which is trivial for untimed MSGs, becomes undecidable when we add timing constraints. Different forms of channel boundedness also then turn out to be undecidable, using reductions from the reachability problem.

Manfred Kufleitner (FMI, Stuttgart). The height of factorization forests
We show that for every homomorphism from A+ to S where S is a finite semigroup there exists a factorization forest of height at most 3 |S | − HS, where HS is the number of H-classes of S and we show that this bound is tight, i.e., for every pair of numbers HS ≤ n we give a semigroup S with n elements and HS -many H-classes such that the height of every factorization forest for S is at least 3 |S | − HS .

Dietrich Kuske (IfI, Leipzig). Which local temporal logics for traces are tractable?
(Joint work with Paul Gastin)
Over the years, many local temporal logics for traces have been proposed and shown to have a satisfiability problem in PSPACE (or EXPTIME) using rather different methods. In this talk, I will report on our attempts to identify a unifying kernel of all these results.

Kamal Lodaya (IMSc, Chennai) Around dot depth two
(Joint work with Paritosh Pandya and Simoni Shah, TIFR, Mumbai)
Brzozowski and Cohen showed that there is an infinite "dot depth" hierarchy inside the starfree languages, based on the alternation of boolean and concatenation operations. It is still open how to algorithmically characterize the dot depth k languages, for k > 1. A precise connection to the quantifier alternation hierarchy of first order logic over words FO[<] was worked out by Thomas, Pin and Weil. From the work of Therien and Wilke we know that first order logic with two variables and linear order FO2[<] corresponds to the unambiguous languages of Schutzenberger, built up using boolean operations and unambiguous concatenation. These languages are inside dot depth two. Interval temporal logic is a formalism similar to the starfree expressions and the complexity of its satisfiability is non-elementary. We define a version of interval temporal logic with deterministic concatenation operators and show that it matches the unambiguous languages and FO2[<]. The complexity of satisfiability drops to NP. A small extension of our ideas characterizes FO2[<,S], the first order logic with two variables, linear order and successor. How does this extension relate to the dot depth two languages?

Anca Muscholl (LaBRI, U. Bordeaux). A look at the control of asynchronous automata
We consider two variants of the control problem for asynchronous automata -- the process-based version introduced by Madhusudan et al, and the action-based version proposed by Gastin et al. We consider the relationships between the two problem settings and show that the process-based version can be reduced to the action-version. For the process-based problem, Madhusudan et al. showed decidability for a restricted automata family by an encoding into MSOL over event structures. We show that the same ideas apply in the action-based case. Morever, we report on some recent progress on Thiagarajan's conjecture about characterizing asynchronous automata with decidable MSO: we show that his conjecture holds for co-graph dependence alphabets.

Paritosh Pandya (TIFR, Mumbai). A Sampling Approach to the Analysis of Metric Temporal Logic
Metric Temporal Logic is a well studied real-time logic. It can be defined with various notions of time such as continuous, sampled (pointwise) or discrete. Moreover time can be strictly monotonic or weakly monotonic. We give a uniform presentation of these metric logics. We propose sampling and digitization techniques for abstracting the undecidable continuous timed MTL into decidable discrete time MTL. The sampling abstraction relies upon a Nyquist-like sufficiently oversampled representation of continuous timed behaviours.

Soumya Paul (IMSc, Chennai). Thiagarajan's conjecture
(joint work with Kamal Lodaya)
We give a proof of Thiagarajan's conjecture: we show that every regular event structure admits a 1-safe folding.

M. Praveen (IMSc, Chennai). Petri nets with small path property
It is known that if a final marking is reachable from an initial marking in a k-safe Petri net, it is reachable through a path that is linear in k and exponential in the number of places. Another class of nets, the structurally partially bounded nets, also has similar properties. We identify that although this common property is used to get efficient reachability algorithms for the reachability problem in these subclasses, they are incomparable.

R. Ramanujam (IMSc, Chennai) Counting multiplicity over infinite alphabets
Verification of infinite state systems involves working with automata over infinite alphabets (where the alphabet corresponds to some unbounded data). Specification of finite state machines equipped with some extra machinery for managing unbounded data is an interesting problem and there have been a few proposals of this kind. We consider one where the emphasis is on counting the multiplicity of occurrences of data elements in words (subject to constraints). We show decidability of emptiness checking for this class and compare it with other classes of automata over infinite alphabets.

Abhisekh Sankaran (IIT Bombay). A FOL Fragment for Safety Checking in Infinite State Systems
We describe a semantic fragment EBS and a decidable syntactic sub-fragment QPS of First-Order Logic (FOL) with equality. These fragments are motivated by formulae that arise in bounded induction and bounded model checking of safety properties in certain infinite state systems. We study the relation between these fragments and their relation to other fragments of FO logic. Finally, we illustrate safety checking in a database application using QPS.

Anil Seth (IIT, Kanpur). Parity Games on Multi-Stack Pushdown Systems
(This work is to appear in LFCS 2009.)
Multi-Stack pushdown systems can be used to model programs with threads and recursion. Model checking of such systems, in their full generality, is undecidable. In recent years model checking of these systems under the restriction of bounded context switching has been studied.

Recently, bounded phase multi-stack pushdown automata have been studied. The restriction of bounded phase is more liberal than bounded context switching. In this talk we present parity games over bounded phase multi-stack pushdown systems. Extending a technique of Walukiewicz to solve games over single stack pushdown systems, we show that parity games over multi-stack pushdown systems are effectively solvable and winning strategy in these games can be effectively synthesized. We show some applications of our result, including a new proof of a known result that emptiness problem for bounded phase multi-stack automata is decidable.

Vijay Suman (TIFR Bombay). Determinization and Expressiveness of Integer Reset Timed Automata with Silent Transitions
Joint work with Paritosh K. Pandya
Epsilon-IRTA are a subclass of timed automata with silent moves. They are useful for modelling global sparse time base used in time-triggered architecture and distributed business processes. In a previous paper [irta_langincl], the language inclusion problem L(A) \subseteq L(B) was shown to be decidable when A is an epsilon-timed automata and B is an epsilon-IRTA.
In this work, we address the determinization, complementation and epsilon-removal questions for epsilon-IRTA. We introduce a new variant of timed automata called GRTA. We show that for every epsilon-IRTA we can effectively construct a language equivalent 1-clock, deterministic GRTA with periodic time guards (but having no epsilon moves). The construction gives rise to at most a double exponential blowup inthe number of locations. We also show that every GRTA with periodic guards can be reduced to a language equivalent epsilon-IRTA with at most double the number of locations.
Thus, epsilon-IRTA, Periodic GRTA, and deterministic 1-clock periodic GRTA have the same expressive power and they are all expressively complete with respect to the regular delta-tick-languages. Equivalence of deterministic and nondeterministic automata also gives us that these automata are closed under the boolean operations.

Pascal Weil (LaBRI, U. Bordeaux)
(Joint work with Manfred Kufleitner)
We propose a new approach of recognizable trace languages, based on the consideration of an algebraic structure that is richer than the usual monoids, and which accounts for the important independence structure on the trace monoid. Using this new algebraic structure, which we call independence monoids, or I-monoids, we are able to give a robust definition of varieties of trace languages and to prove an Eilenberg-type theorem. We put this to use to generalize a result of Pin and Weil on the polynomial closure of a variety of languages, which had already been extended to certain particular classes of trace languages by Kufleitner. Our new approach makes it possible to follow the word language proof scheme, and to avoid the obstacles that arose in Kufleitner's earlier work. A corollary of this work is to relate the analogue of the dot-depth hierarchy for star-free trace languages, with the quantifier alternation hierarchy of first-order logic.

Marc Zeitoun (LaBRI, U. Bordeaux). Tree Pattern Rewriting Systems
(Joint work with Blaise Genest, Anca Muscholl, and Olivier Serre)
Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XML-based applications have become pervasive, for instance with the ever growing importance of web services. We define here Tree Pattern Rewriting Systems (TPRS) as an abstract model of dynamic XML-based documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system (T, R), a tree pattern P and some integer k such that any reachable document from T has depth at most k, it is decidable (albeit of non elementary complexity) whether some tree matching P is reachable from T.

Wiesiek Zielonka (LIAFA, Paris). Positional equilibria in infinite perfect information games
(Joint work with Hugo Gimbert)
We consider infinite perfect information games that are played on finite arenas by two strictly antagonistic players. Some games in this class (like parity or mean-payoff games) admit positional equilibria, i.e. equilibria where both players use positional (memoryless) strategies. Although the initial proofs of the existence of positional equilibria were very game specific, without any discernible similarities, later on it became clear that, at least in some cases, it is possible to give uniform existence proofs.
This raised the question if it is possible to give one uniform existence proof for all games with positional equilibria, or, in other words, if it is possible to characterize payoff mappings (preference relations) which admit positional equilibria.
We present such a characterization of preference relations with positional equilibria, this characterization is exact, i.e. we provide conditions that are at the same time necessary and sufficient. These conditions are more usable and comprehensible than conditions that we presented at CONCUR 2005.

Visa issues

Participants from outside India need a visa to enter India.

Accomodation

Indian PhD students will be accommodated at IMSc

Indian faculty will be accommodated at IMSc

Faculty/postdocs from outside India will be accommodated at the Quality Hotel Sabari Classic.

Wifi internet access will be available at all of these locations.

Travel support

Students from India will be reimbursed 3AC train fare.

Indian faculty who need travel support can request apex airfare. Please write to Kamal Lodaya and Madhavan Mukund if you need travel support.

Pascal Weil/Madhavan Mukund Created October 9, 2008. Last updated May 6, 2009.