ANR 12IS02001
PACE meeting, february 9th, 2014, Lyon
*
The meeting will take place at École Normale Supérieure, site Monod,
Amphi B (3rd floor). See
this
page for directions.
- 10h15 Welcome everybody, happy new year
- 10h30
Yuxi Fu "Dividing Line between Decidable Pushdown Automata and
Undecidable Ones"
Senizergues has proved that language equivalence is decidable for disjoint $\epsilon$-deterministic PDA. Stirling has showed that strong bisimilarity is decidable for PDA. On the negative side Srba demonstrated that the weak bisimilarity is undecidable for normed PDA. Later Jancar and Srba established the undecidability of the weak bisimilarity for the disjoint $\epsilon$-pushing PDA and the disjoint $\epsilon$-popping PDA. These decidability and undecidability results are extended in the present talk. The extension is achieved by looking at the equivalence checking issue of the branching bisimilarity for several variants of PDA. - 11h15 break
- 11h30 Catuscia Palamidessi, "A generalized differential privacy principle, and applications to location privacy"
- 12h15 Thomas Given-Wilson, "Modeling Security" slides
- 12h45
lunch
- 14h00 Paul Brunet, "Kleene Algebra with Converse" slides
- 14h30
Guoqiang Li, "Nested Timed Automata"
slides
A NeTA is a pushdown system whose stack symbols are timed automata (TAs). It either behaves as the top TA in the stack, or switches from one TA to another by pushing, popping, or changing the top TA of the stack. Different from existing component-based context-switch models such as recursive timed automata and timed recursive state machines, when time passage happens, all clocks of TAs in the stack elapse uniformly. We show that the safety property of NeTAs is decidable by encoding NeTAs to the dense timed pushdown automata. NeTAs provide a natural way to analyze the recursive behaviors of component-based timed systems with structure retained. We illustrate this advantage by the deadline analysis of nested interrupts. - 15h00
Alessandro Rioli, "Operational techniques for the equivalence of linear
higher-order functional programs"
A range of different methods for checking equivalence between terms of linear higher-order functional programs is developed. More specifically, context equivalence and applicative bisimilarity are examined in a typed environment. The study is carried out in both the deterministic and probabilistic settings, with an eye to the analysis of quantum computation. " - 15h30 break
- 15h45
Yuxin Deng, "Probabilistic bisimilarity revisited"
slides
For reactive probabilistic processes it is known that bisimilarity coincides with simulation equivalence. The proofs of this folklore result in the literature are often very involved. In the current work we give an elementary proof that employs only some basic concepts of set theory. We also provide a simple modal characterisation of bisimilarity. - 16h15 Raphaëlle Crubillé, "Probabilistic Applicative Bisimulation and Call-by-Value Lambda Calculi" slides
- 16h45
Ugo Dal Lago, "Probabilistic Recursion Theory and Implicit Complexity"
We show that probabilistic computable functions, i.e., those functions outputting distributions and computed by probabilistic Turing machines, can be characterized by a natural generalization of Church and Kleene's partial recursive functions. The obtained algebra, following Leivant, can be restricted as to capture the notion of polytime samplable distributions, a key notion in average - case complexity and cryptography. - ~17h30
end
- 20h00 social dinner
Participants
F. Bonchi, P. Brunet, R. Crubillé U. Dal Lago, L. Deng, Y. Deng, Y. Fu, T. Given-Wilson, C. He, D. Hirschkoff, G. Li, JM. Madiot, C. Palamidessi, D. Pous, A. Rioli, D. Sangiorgi, F. Valencia, V. Vignudelli, X. Xu, F. Zanasi