-
When are timed automata determinizable ?
by Thomas Brihaye
It is well known that timed automata are not determinizable. In this
talk, we present an abstract procedure which, given a timed automaton,
produces a language-equivalent deterministic infinite timed tree. We
prove that under a certain boundedness condition, the infinite timed
tree can be reduced into a classical deterministic timed
automaton. The boundedness condition is satisfied by several
subclasses of timed automata, some of them were known to be
determinizable (event-clock timed automata, automata with integer
resets), but some others were not. We prove for instance that strongly
non-Zeno timed automata can be determinized. As a corollary of those
constructions, we get for those classes the decidability of the
universality and of the inclusion problems, and compute their
complexities (the inclusion problem is for instance EXPSPACE-complete
for strongly non-Zeno timed automata). This is a joint work with
Ch. Baier, N. Bertrand and P. Bouyer.
- Volume and Entropy of
Regular Timed Languages
by Aldric Degorre
For timed languages, we define size measures: volume for languages
with a fixed finite number of events, and entropy (growth rate) as
asymptotic measure for an unbounded number of events. These measures
can be used for quantitative comparison of languages, and the entropy
can be viewed as information contents of a timed language. For languages
accepted by deterministic timed automata, we give exact formulas for
volumes. Next, we characterize the entropy, using methods of functional
analysis, as a logarithm of the leading eigenvalue (spectral radius) of
a positive integral operator. We devise several methods to compute the
entropy: a symbolical one for so-called “1-1/2 -clock” automata, and two
numerical ones: one using techniques of functional analysis, another based
on discretization. We give an information-theoretic interpretation of the
entropy in terms of Kolmogorov complexity.
- Randomness for free
by Laurent Doyen
We consider two-player zero-sum games on graphs. These games can be
classified
on the basis of the information of the players and on the mode of
interaction
between them.
According to information the classification is as follows:
(a) partial-observation (both players have partial view of the game);
(b) one-sided complete-observation (one player has complete observation);
(c) complete-observation (both players have complete view of the game).
According to the mode of interaction we have the following classification:
(a) concurrent (both players interact simultaneously);
(b) turn-based (the players interact in turn).
The two sources of randomness in such games are randomness in transition
function and randomness in strategies.
In general, randomized strategies are more powerful than deterministic
strategies, and randomness in transitions gives more general classes of
games.
In this work we present a complete characterization for the classes of
games
where randomness is not helpful in:
(a) the transition function (probabilistic transition can be simulated
by deterministic transition);
(b) strategies (pure strategies are as powerful as randomized strategies).
As a consequence of our characterization we obtain new undecidability
results for these games.
-
Safety properties for querying XML streams
by Olivier Gauwin
As XML documents become huge, new techniques for processing them in a
streaming manner arise. Querying is a basic task in XML processing, and
consists in selecting nodes in the XML document, modeled as a tree.
Streaming XML consists in discovering this tree through a pre-order
traversal. Outputting selected nodes at the earliest possible time point
is required, in order to reach minimal memory cost. A dual problem is
the earliest rejection of failed candidate nodes. We show how these
requirements relate to safety properties. We study queries defined by
visibly pushdown automata (VPAs). For queries defined by deterministic
VPAs, we provide two alternative algorithms computing the safety
property in polynomial time, thus permitting tractable earliest query
answering. Both techniques can be lifted to deterministic pushdown
automata. For queries defined by non-deterministic VPAs, earliest
rejection remains tractable, unlike earliest selection. This is joint
work with Joachim Niehren and Sophie Tison.
- Realizability of real-time
logics by Gilles Geeraerts
We study the realizability problem
for specifications of reactive systems expressed in real-time linear
temporal logics. The logics we consider are subsets of MITL (Metric
Interval Temporal Logic), a logic for which the satisfiability and
validity problems are decidable, a necessary condition for the
realizability problem to be decidable. On the positive side, we show
that the realizability of LTL extended with past real-time formulas is
decidable in 2EXPTIME, with a matching lower bound. On the negative
side, we show that a simple extension of this decidable fragment with
future real-time formulas leads to undecidability. In particular, our
results imply that the realizability problem is undecidable for ECL
(Event Clock Logic), and therefore also for MITL
- Decision Procedures for
Alternating Timed Automata by Mark Jenkins
Alternating timed automata extend Alur-Dill timed automata to obtain closure
under all Boolean operations. However, over dense infinite time domains
(such as the reals) they have an undecidable language emptiness problem.
Our main result is that the restriction to bounded time restores
decidability of the language emptiness problem. The proof of this involves
solving a parametrized version of Church's synthesis problem over bounded
real time. This problem is expressed as a McNaughton game played over timed
words with a monadic winning condition.
- The covering and boundedness
problems for branching vector addition systems
by Ranko Lazic
Covering, boundedness and reachability are three fundamental problems
for vector addition systems (VAS). In 1976, Lipton established that
they are EXPSPACE-hard for VAS (or equivalently, for Petri nets). The
lower bound was matched by Rackoff two years later, when he showed
that covering and boundedness are in EXPSPACE. Although reachability
was proved decidable for VAS by Meyer and Kosaraju several years
later, little else is known about its complexity.
For branching vector addition systems (BVAS), an intriguing novel
model of computation, not even decidability of reachability is known
yet. However, covering and boundedness were shown decidable in 2005
by Verma and Goubault-Larrecq. We show that their complexity for BVAS
is 2EXPTIME.
Joint work with Stephane Demri, Marcin Jurdzinski, and Oded Lachish.
-
Iterated Regret Minimization in Game Graphs
by Tristan Le Gall
Iterated regret minimization has been introduced recently by
J.Y. Halpern and R. Pass in classical strategic games. For many games
of interest, this new solution concept provides solutions that are
judged more reasonable than solutions offered by traditional game
concepts -- such as Nash equilibrium --. Although computing iterated
regret on explicit matrix game is conceptually and computationally
easy, nothing is known about computing the iterated regret on games
whose matrices are defined implicitly using game tree, game DAG or,
more generally game graphs. In this paper, we investigate iterated
regret minimization for infinite duration two-player quantitative
non-zero sum games played on graphs.
We consider reachability objectives that are not necessarily
antagonist. Edges are weighted by integers -- one for each player --,
and the payoffs are defined by the sum of the weights along the
paths. Depending on the class of graphs, we give either polynomial or
pseudo-polynomial time algorithms to compute a strategy that
minimizes the regret for a fixed player. We finally give algorithms
to compute the strategies of the two players that minimize the
iterated regret for trees, and for graphs with strictly positive
weights only.
- Algorithmic learning in
verification and synthesis
by Daniel Neider
In my PhD research, I study the applicability of techniques known from
algorithmic learning to the field of verification and synthesis. In
particular, I am working on solving two-person, zero-sum reachability games
on graphs. Although there exist efficient linear time algorithms for this
problem, such algorithms perform poorly on really huge game graphs.
Moreover, for infinite graphs there are no algorithms known that always
guarantee to compute the attractor (if it exists). In such situations,
algorithmic learning can offer a valuable alternative.
My approach is to encode game graphs symbolically and use methods known from
algorithmic learning. In my talk I would like to present a method that
learns attractor sets in reachability games on (finite or infinite) game
graphs, which are represented by automatic transducers.
- On Classical, Real-Time, and
Time-Bounded Verification
by Joel Ouaknine
I will survey the classical, real-time, and time-bounded theories of
verification, highlighting key differences and similarities among
them, and giving an overview presentation of the solution to a
longstanding open problem in the field.
This is joint work with Alex Rabinovich and James Worrell.
- Distributed Dynamic
Condition Response Structures
by Raghava Rao
Mukkamala
The key difference between
declarative and imperative process languages is that the control flow
for the declarative languages is defined implicitly as a set of
constraints or rules where as for the imperative languages, it is
defined explicitly, e.g. as a flow diagram or a sequence of state
changing commands. There is a long tradition for using declarative
logic based languages to schedule transactions in the database
community and also several authors have noted that it could be an
advantage to also use a declarative approach to specify workflow and
business processes.
Recently, we have proposed distributed dynamic condition response
structures (DCR) as a declarative process model inspired by the
workflow language employed by our industrial partner and
conservatively generalizing labelled event structures. The model adds
to event structures the possibility to 1) finitely specify repeated,
possibly infinite behavior, 2) finitely specify fine-grained
acceptance conditions for (possibly infinite) runs and 3) distribute
events via roles. We have also proposed a graphical notation inspired
by related work by van der Aalst et al and formalize the execution
semantics as a labelled transition system. In this talk, I will
present our work dynamic condition response structures as a
declarative process language based on labelled event structures.
- Automata based verification
over linearly ordered data domains
by Szimon Toruńczyk
We work over linearly ordered data domains equipped with finitely many
unary predicates and constants. We consider nondeterministic automata
processing words and storing finitely many variables ranging over the
domain. During a transition, these automata can compare the data
values of the current configuration with those of the previous
configuration using the linear order, the unary predicates and the
constants. We show that emptiness for such automata is decidable,
both over finite and infinite words, under reasonable computability
assumptions on the linear order. Finally, we show how our automata
model can be used for verifying properties of workflow specifications
in the presence of an underlying database. (join work with Luc
Segoufin, INRIA, France)