Program (titles and authors) |
||
Program (incl. abstracts) |
||
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)
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.
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)
The workshop is sponsored by
the Indo-French project Timed-Discoveri, and through this project by CNRS, the Foreign Affairs Ministry (France) and the Department of Science and Technology (Government of India);
Sub-project 4, Formal approaches for computer systems, of the Ile-de-France/Inde project of the ARCUS program (Région Ile-de-France and Foreign Affairs Ministry, France);
the Academic alliance between Chennai Mathematical Institute and Tata Consultancy Services.
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 S_{i}
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 S_{i}
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},
FO^{2}
∩ Σ_{2}
(and
by duality FO^{2}
∩ Π_{2}),
and FO^{2}.
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 ﬁnite 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 ﬁnal 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.
Participants from outside India need a visa to enter India.
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.
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.