ICE 2011

June 9th, 2011      Reykjavik, Iceland (satellilte of DisCoTec'11) organised with Artist partners 

Programme

ICE 2011 programme

Slot Duration Talk
09:00 – 09:10 (00:10) Opening
09:10 – 10:00 (00:50) Epistemic Strategies and Games on Concurrent Processes.
Prakash Panangaden (invited talk)
10:00 – 10:30 (00:30) Coffee break
10:30 – 11:00 (00:30) Innocent Strategies as Sheaves and Interactive Equivalences for CCS.
Tom Hirschowitz and Damien Pous
11:00 – 11:30 (00:30) Interaction and Observation, Categorically.
Vincenzo Ciancia
11:30 – 11:40 (00:10) Short coffee break
11:40 – 12:10 (00:30) SOS for Graph Rewriting.
Tobias Heindel and Andrei Dorman
12:10 – 12:40 (00:30) Polymorphic Endpoint Types for Copyless Message Passing.
Luca Padovani and Viviana Bono
12:40 – 14:00 (01:20) Lunch
14:00 – 15:00 (01:00) A Uniform Framework for Modeling Processes Behaviors and their Performances.
Rocco de Nicola (Joint Invited Talk with PACO 2011)
15:00 – 15:30 (00:30) On the Reaction Time of Some Synchronous Systems.
Ilias Garnier, Christophe Aussagues, Vincent David and Guy Vidal-Naquet
15:30 – 16:00 (00:30) Semantic Models of Connectors: A Study on Equivalence.
Sung-Shik T. Q. Jongmans and Farhad Arbab
16:00 – 16:30 (00:30) Coffee break
16:30 – 17:20 (00:50) Formal Analysis of Quantum Systems using Process Calculus.
Simon Gay (Invited Talk)
17:20 – 17:30 (00:10) Short coffee break
17:30 – 18:00 (00:30) Amending Contracts for Choreographies.
Laura Bocchi, Julien Lange and Emilio Tuosto
18:00 – 18:30 (00:30) Contracts in Distributed Systems.
Massimo Bartoletti, Emilio Tuosto and Roberto Zunino
18:30 – 18:40 (00:10) Closing
20:00 Social Event

Presentation names in the above table link to the slides used by the speakers (courtesy of the said speakers). Be aware that some of them are quite big, the complete package is approximately 49Mb.

Invited talks

  • Rocco De Nicola (University of Florence, Italy; joint invited talk with PACO 2011) "A Uniform Framework for Modeling Processes Behaviors and their Performances"
    Abstract: Labeled transition systems (LTS) are typically used as behavioral models of nondeterministic processes, with labeled transitions defining a one-step state-to-state reachability relation. This model is made more general by modifying the transition relation in such a way that it associates with any source state and transition label a reachability distribution, i.e., a function mapping each possible target state to a value of some domain that expresses the degree of one-step reachability of that target state from the source one. The resulting model, called ULTraS from Uniform Labeled Transition System, can then be specialized, by selecting suitable domains, to a number of widely used behavioral models representing fully nondeterministic, fully probabilistic and fully stochastic processes, but also processes combining nondeterminism and probability or nondeterminism and stochasticity.
    We will show how ULTraS can be used to model stochastic process calculi when the reachability distribution does represent the rate of the exponential distribution characterizing the execution time of the performed action. By defining appropriate operators on reachability distributions, we will provide compositional operational semantics of representative fragments of the major stochastic calculi and shed light on their differences and similarities.
    The uniform treatment of different operational models can be extended uniformly to model classical behavioral equivalences like bisimulation, trace, and testing. These equivalences will be defined over ULTraS parametrically with respect to some measure function that expresses the degree of multi-step reachability of a set of states. It will be then shown that the specializations of bisimulation, trace, and testing equivalences over ULTraS, obtained for the various types of process by selecting suitable measure functions, coincide with some of the well known behavioral equivalences defined in the literature, thus emphasizing the adequacy of ULTraS as a unifying behavioral model.
    This is the outcome of joint work with M. Bernardo, D. Latella, M. Loreti, M. Massink.
  • Simon Gay (University of Glasgow, UK) "Formal Analysis of Quantum Systems using Process Calculus and Model-Checking"
    Abstract Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods: formal logics for specification, formal modelling languages, separation of levels of abstraction, compositional analysis, and so on.
    I will argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and present the results of initial investigation using two techniques: behavioural equivalence in process calculus, and model-checking.
  • Prakash Panangaden (Oxford University, UK on sabbatical leave from McGill University, Canada) "Epistemic Strategies and Games on Concurrent Processes"
    Abstract: We develop a game semantics for process algebra with two interacting agents. The purpose of our semantics is to make manifest the role of knowledge and information flow in the interactions between agents and to control the information available to interacting agents. We define games and strategies on process algebras, so that two agents interacting according to their strategies determine the execution of the process, replacing the traditional scheduler. We show that different restrictions on strategies represent different amounts of information being available to a scheduler. We also show that a certain class of strategies corresponds to the syntactic schedulers of Chatzikokolakis and Palamidessi, which were developed to overcome problems with traditional schedulers modelling interaction. The restrictions on these strategies have an explicit epistemic flavour. This is joint work with Konstantinos Chatzikokolakis and Sophia Knight, both at INRIA Saclay.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet