- 13h30: Randomness for free by Laurent Doyen
- 14h15: When are timed automata determinizable ? by Thomas Brihaye
- 15h00: Coffee Break
- 15h30: Realizability of real-time logics by Gilles Geeraerts
- 16h15: Volume and Entropy of Regular Timed Languages by Aldric Degorre
- 17h00: On Classical, Real-Time, and Time-Bounded Verification by Joel Ouaknine

- 09h30: Decision Procedures for Alternating Timed Automata by Mark Jenkins
- 10h00: Automata based veriﬁcation over linearly ordered data domains by Szimon Toruńczyk
- 10h30: Coffee break
- 11h00: Distributed Dynamic Condition Response Structures by Raghava Rao Mukkamala
- 11h30: Algorithmic learning in verification and synthesis by Daniel Neider
- 12h00: Lunch Break
- 13h30 The covering and boundedness problems for branching vector addition systems by Ranko Lazic
- 14h15: Iterated Regret Minimization in Game Graphs by Tristan Le Gall
- 15h00: Safety properties for querying XML streams by Olivier Gauwin

- 09h00: Free time for discussions

**When are timed automata determinizable ?**by Thomas BrihayeIt 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 DegorreFor timed languages, we deﬁne size measures: volume for languages with a ﬁxed ﬁnite 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 DoyenWe 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 GauwinAs 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 GeeraertsWe 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 JenkinsAlternating 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 LazicCovering, 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 GallIterated 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 NeiderIn 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 OuaknineI 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 MukkamalaThe 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 veriﬁcation over linearly ordered data domains**by Szimon ToruńczykWe work over linearly ordered data domains equipped with ﬁnitely many unary predicates and constants. We consider nondeterministic automata processing words and storing ﬁnitely many variables ranging over the domain. During a transition, these automata can compare the data values of the current conﬁguration with those of the previous conﬁguration using the linear order, the unary predicates and the constants. We show that emptiness for such automata is decidable, both over ﬁnite and inﬁnite words, under reasonable computability assumptions on the linear order. Finally, we show how our automata model can be used for verifying properties of workﬂow speciﬁcations in the presence of an underlying database. (join work with Luc Segouﬁn, INRIA, France)