Abstracts
Dec 09 2009, 14:30
Speaker: Paolo Baldan
Title: Open Petri nets, Compositionality and Asynchrony
Abstract:
Open Petri nets are a reactive Petri net model which allows for the representation of open systems, interacting with the surrounding environment. Open nets enrich basic Petri nets with a notion of interface and a corresponding composition operation. Interleaving and trulyconcurrent semantics can be shown to be compositional on open nets. We argue that interactions in open nets are inherently asynchronous, providing an encoding of (bound) asynchronous CCS into open nets. The encoding allows one to derive some results on the expressiveness of the two models and suggests some interesting connections between concurrency and asynchrony.
Nov 27 2009, 10:30
Speaker: Luca Aceto
Title: A Rule Format for Unit Elements
Abstract:
In this talk, I will discuss a generic rule format for Structural Operational Semantics in the style of Plotkin guaranteeing that certain basic programs act as left or rightunit elements for a set of binary operators. I will show the generality of the format by applying it to a wide range of operators from the literature on process calculi, which are prototype languages for the description of parallel processes.
Results like the one I will present serve multiple purposes. Firstly, they pave the way for a toolset that can mechanically prove semantic properties via syntactic means without involving user interaction. Secondly, they provide us with an insight as to the semantic nature of basic algebraic properties and its link to the syntax of the rules defining the operational semantics of languages. In other words, our rule formats may serve as a guideline for language designers who want to ensure, a priori, that the constructs under design enjoy certain basic algebraic properties.
This is joint work with Anna Ingolfsdottir (RU), MohammadReza Mousavi (TU Eindhoven) and Michel Reniers (TU Eindhoven) that will appear in the Proceedings of 'SOFSEM 2010: The 36th International Conference on Current Trends in Theory and Practice of Computing', Lecture Notes in Computer Science, SpringerVerlag, 2010.
Nov 25 2009, 10:00
Speaker: Jesus Aranda
Title: On the Expressivity of Infinite and Local Behaviour in Fragments of the Picalculus (Rehearsal PhD talk)
Abstract:
The picalculus [Miln99] is one the most influential formalisms for modelling and analyzing the behaviour of concurrent systems. This calculus provides a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. For example, the parallel composition term P  Q, which is built from the terms P and Q, represents the process that results from the parallel execution of the processes P and Q. Similarly, the restriction ( u x)P represents a process P with local resource x. The replication !P can be thought of as abbreviating the parallel composition P  P  P .... of an unbounded number of P processes.
As for other languagebased formalisms (e.g., logic, formal grammars and the lambdacalculus) a fundamental part of the research in process calculi involves the study of the expressiveness of fragments or variants of a given process calculus. In this dissertation we shall study the expressiveness of some variants of the picalculus focusing on the role of the terms used to represent local and infinite behaviour, namely restriction and replication.
The first part of this dissertation is devoted to the expressiveness of the zeroadic variant of the (polyadic) picalculus, i.e., CCS with replication (CCS!) [BGZ03].
Busi et al [BGZ04] show that CCS! is Turing powerful [BGZ04]. The result is obtained by encoding Random Access Machines (RAMs) in CCS!. The encoding is said to be nonfaithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving.
In this dissertation we shall study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that terminationpreserving CCS! processes can generate languages which are not Type 2. We finally conjecture that the languages generated by terminationpreserving CCS! processes are Type 1 .
We also observe that the encoding of RAMs [BGZ04] and several encoding of Turingpowerful formalisms in picalculus variants may generate an unbounded number of restrictions during the simulation of a given machine. This unboundedness arises from having restrictions under the scope of replication (or recursion) as in e.g., $!(nu x)P$ or $\mu X.( u x)(P  X)$. This suggests that such an interplay between these operators is fundamental for Turing completeness.
We shall also study the expressive power of restriction and its interplay with replication. We do this by considering several syntactic variants of CCS! which differ from each other in the use of restriction with respect to replication. We consider three syntactic variations of CCS! which do not allow the generation of unbounded number of restrictions: C1 is the fragment of CCS! not allowing restrictions under the scope of a replication, C2 is the restrictionfree fragment of CCS!. The third variant is C3 which extends C1 with Phillips' priority guards [Phillips:08].
We shall show that the use of an unboundedly many restrictions in CCS! is necessary for obtaining Turing expressiveness in the sense of Busi et al [BGZ04]. We do this by showing that there is no encoding of RAMs into C1 which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS! into C1 nor from C1 into C2 . Thus up to failures equivalence, we cannot encode a process with an unbounded number of restrictions into one with a bounded number of restrictions, nor one with a bounded number of restrictions into a restrictionfree process.
As lemmata for the above results we prove that convergence is decidable for C1 and that language equivalence is decidable for C2 but undecidable for C1 . As corollary it follows that convergence is decidable for restrictionfree CCS. Finally, we show the expressive power of priorities by providing a faithful encoding of RAMs in C3. Thus bearing witness to the expressive power of Phillips' priority guards [Phillips:08].
The second part of this dissertation is devoted to expressiveness of the asynchronous monadic picalculus, Api [Boudol92,HondaT91]. In [PSVV06] the authors studied the expressiveness of persistence in Api [Boudol92,HondaT91] wrt weak barbed congruence. The study is incomplete because it ignores divergence.
We shall present an expressiveness study of persistence in Api wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [PSVV06], we consider Api and three sublanguages of it, each capturing one source of persistence: the persistentinput Apicalculus (PIpi), the persistentoutput Apicalculus (POpi) and the persistent Apicalculus (Ppi). In [PSVV06] the authors showed encodings from Api into the semipersistent calculi (i.e., POpi and PIpi) correct wrt weak barbed congruence. We show that, under some general conditions related to compositionality of the encoding and preservation of the infinite behaviour, there cannot be an encoding from Api into a (semi)persistent calculus preserving the must testing semantics. We also prove that convergence and divergence are decidable for POpi (and Ppi). As a consequence there is no encoding preserving and reflecting divergence or convergence from Api into POpi (and Ppi). This study fills a gap on the expressiveness study of persistence in Api in [PSVV06].
REFERENCES
[BGZ04]N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion, replication, and iteration in process calculi. In ICALP04, volume 3142 of Lecture Notes in Computer Science, pages 307319. SpringerVerlag, 2004.
[Boudol92] G. Boudol. Asynchrony and the picalculus. Technical Report RR1702, INRIA Sophia Antipolis, 1992.
[HondaT91] K. Honda and M. Tokoro. An ob ject calculus for asynchronous communication. In P. America, editor, ECOOP, volume 512 of Lecture Notes in Computer Science, pages 133 147. Springer, 1991.
[Miln99] Milner, R.: Communicating and Mobile Systems: the picalculus. Cambridge University Press, Cambridge (1999).
[PSVV06] C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:5968, 2006.
[Phillips:08]I. Phillips: CCS with priority guards.J. Log. Algebr. Program. 75(1): 139165 (2008).
Nov 13 2009, 15:30
Speaker: Miguel Andres
Title: Probabilistic Anonymity and Admissible Schedulers.
Abstract:
When studying safety properties of (formal) protocol models, it is customary to view the scheduler as an adversary: an entity trying to falsify the safety property. We show that in the context of security protocols, and in particular of anonymizing protocols, this gives the adversary too much power; for instance, the contents of encrypted messages and internal computations by the parties should be considered invisible to the adversary.
We restrict the class of schedulers to a class of admissible schedulers which better model adversarial behaviour. These admissible schedulers base their decision solely on the past behaviour of the system that is visible to the adversary.
Using this, we propose a definition of anonymity: For all admissible schedulers the identity of the users and the observations of the adversary are independent stochastic variables. We also develop a proof technique for typical cases that can be used to prove anonymity: A system is anonymous if it is possible to `exchange' the behaviour of two users without the adversary `noticing'.
Nov 13 2009, 14:00
Speaker: Miguel Andres
Title: Computing the Leakage of InformationHiding Systems
Abstract:
We address the problem of computing the information leakage of a system in an efficient way. We propose two methods: one based on reducing the problem to reachability, and the other based on techniques from quantitative counterexample generation. The second approach can be used either for exact or approximate computation, and also provides feedback for debugging. These methods can be applied also in the case in which the input distribution is unknown.
We then consider the case of interacting systems and we point out that the definition of associated channel proposed in literature is not sound. We note that the notion of leakage, however, can still be defined in a consistent way, and we show that our methods extend smoothly to this case.
Nov 02 2009, 14:30
Speaker: Yuri Gurevich
Title: The ChurchTuring Thesis: Story and Recent Progress
Abstract:
The ChurchTuring thesis is one of the foundations of computer science. The thesis heralded the dawn of the computer revolution by enabling the construct of the universal Turing machine which led the way, at least conceptually, to the von Neumann architecture and first electronic computers. One way to state the ChurchTuring thesis is as follows: A Turing Machine computes every numerical function that is computable by means of a purely mechanical procedure. It is that remarkable and a priori implausible characterization that underlies the ubiquitous applicability of digital computers. But why do we believe the thesis? Careful analysis shows that the existing arguments are insufficient. Kurt GÃ¶del surmised that it might be possible to state axioms which embody the generally accepted properties of computability, and to prove the thesis on that basis. That is exactly what we did in a recent paper with Nachum Dershowitz of Tel Aviv University.
Beyond our proof, the story of the ChurchTuring thesis is fascinating and scattered in specialized and often obscure publications. I will try to do justice to that intellectual drama.
Oct 14 2009, 14:30
Speaker: Brigitte Pientka
Title: Beluga: programming with dependent types and higherorder data
Abstract:
The logical framework LF supports specifying formal systems and proofs about them using a simple, powerful technique, called higherorder abstract syntax (HOAS). Recently, it has been for example successfully used to specify and verify guarantees about the runtime behavior of mobile code. However, incorporating logical framework technology into functional programming to directly allow programmers to describe and reason about properties of programs from within the programming language itself has been a major challenge.
In this talk, I will present Beluga, a dependentlytyped functional language which supports programming with data specified in the logical framework LF. First, I will show how to implement normalization for typed lambdaterms in Beluga, and highlight its theoretical foundation based on contextual types. Second, I will discuss practical challenges regarding type reconstruction for dependently typed systems and summarize the status of our implementation.
Sep 30 2009, 10:30
Speaker: Ugo Montanari
Title: A Minimization Algorithm for Symbolic Bisimilarity
Abstract:
The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics is defined in terms of bisimilarity that, in the finite case, can be computed via the wellknown partition refinement algorithm. However, the behavior of interactive systems is in many cases infinite and thus checking bisimilarity in this way is unfeasible. Symbolic semantics allows to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some sources of infiniteness. Unfortunately, the standard partition refinement algorithm does not work with symbolic bisimilarity. Our algorithm is based on a notion of redundant symbolic transitions and computes bisimilarity and redundancy at the same time. The main peculiarity of the algorithm is that in the initial partition we have to insert not only the reachable states, but also those that are needed to check redundancy. Interestingly enough, both symbolic bisimilarity and minimization algorithm can be justified as standard bisimilarity and terminal sequence iterative algorithm for a functor working in a category of algebras, thus reducing the symbolic approach to a well known framework (Work in collaboration with Filippo Bonchi, CWI Amsterdam. The results are based on papers by Bonchi and Montanari at ESOP 2009 and CALCO 2009).
May 26 2009, 14:30
Speaker: Miguel Andres
Title: Conditional Probabilities over Probabilistic and Nondeterministic Systems
Abstract:
This paper introduces the logic cpCTL, which extends the probabilistic temporal logic pCTL with conditional probability, allowing one to express that the probability that phi is true given that psi is true is at least a. We interpret cpCTL over Markov Chain and Markov Decision Processes. While model checking cpCTL over Markov Chains can be done with existing techniques, those techniques do not carry over to Markov Decision Processes. We present a model checking algorithm for Markov Decision Processes. We also study the class of schedulers that suffice to find the maximum and minimum probability that phi is true given that psi is true. Finally, we present the notion of counterexamples for cpCTL model checking and provide a method for counterexample generation.
May 12 2009, 14:30
Speaker: Kai Bruennler
Title: Nested Sequents
Abstract:
We see how nested sequents, a natural generalisation of hypersequents, allow to develop a systematic proof theory for modal logics. As opposed to other prominent formalisms, such as the display calculus and labelled sequents, nested sequents stay inside the modal language and allow for proof systems which enjoy the subformula property in the literal sense.
May 05 2009, 14:30
Speaker: Joachim Parrow
Title: Three holy grails of programming models
Abstract:
I shall discuss three important paradigms for formulating models of programming languages, the technical problems involved in unifying them, and how it connects to recent work joint with Jesper Bengtson, Magnus Johansson and BjÃ¶rn Victor (LICS'09). This will also serve to put the picalculus in perspective by explaining its underlying motivations and real achievements and limitations. The intended audience should have a reasonable grasp on programming but needs not be familiar with any particular formal models.
Apr 03 2009, 14:30
Speaker: Pawel Sobocinski
Title: An introduction to the wire calculus
Abstract:
The wire calculus is a process algebra for modelling true concurrency and explicit network topologies. It can handle systems that combine different communication paradigms (synchronous, asynchronous) within a single specification. Technically, it can be understood roughly as taking Milner's CCS but with the familiar parallel composition operator removed and replaced with operators inspired by monoidal categories  tensor product and sequential composition. These operators handle the "coordination" aspects. The "computational" or "dynamic" aspects are handled with a unary CCSlike prefix operation and recursion. Like CCS, the semantics is given using labelled transition systems that are defined compositionally using the SOS approach.
The interesting differences from CCS include the fact that the wire calculus is a truly concurrent formalism (noninterleaving) and, due to the intrinsic property of reflexivity, there is only one kind of bisimulation: "strong" and "weak" bisimilarities coincide. In this talk I will introduce the wire calculus and motivate it with several familiar examples  synchronous circuits, Petri nets and CCS itself.
Mar 17 2009, 14:30
Speaker: Balaji Raman
Title: ApplicationSpecific Workload Shaping in ResourceConstrained Media Players
Abstract:
In this talk, I will present the main contributions of my PhD thesis, which I defended in January 2009 at School of Computing, National University of Singapore. The primary objective of this presentation is to find potential collaborators in this research direction, that is, systemlevel design for multimedia applications using network calculus. My thesis abstract below should help you get some idea about this talk. If you are interested, you can read the attached paper too.
Thesis Abstract
Much research in systemlevel design for multimedia devices are based on analysis with system models, but how insightful are they? System simulation is the prime technique used in computer architecture and embedded system design to explore potential design solutions and validate design choices. Unfortunately, simulation seldom gives real insight and strong guarantees on the dynamic behaviour of a system. On the other hand existing analytical models could not capture some important attributes of multimedia system. Consequently, the analysis with such mathematical models are not beneficial for efficient system design. An useful analysis with either simulation or analytical models should provide resource saving techniques. These methods can exploit the key characteristic features of the multimedia streams. The fluid nature in arrivals and inconstant processing requirements of data items are multimedia's inherent characteristic features. But, these characteristic features are predictable. So, the foreseeable properties could be studied to yield techniques that can significantly save onchip resources.
This thesis proposes techniques to shape multimedia workload so as to effectively utilize onchip resources such as processor and memory. These shaping techniques attempt to solve the problem in providing guarantees for highquality media output with minimal onchip resources. The research approach is to use analytical models and accurately capture the variable characteristics in arrival and execution of items in multimedia streams. Such mathematical models after analysis yield deepinsights to tune certain application parameters. Using this parameter tuning it is possible to reshape variable media workload to reduce processing and storage requirements. The central tenet of this parametric tuning is to adapt the workload such that only average or minimum processor cycle required for every multimedia data item is provided, and not the maximum.
Our results show that choosing the appropriate initial playout delay (after which the video starts) can lead to effective processor utilization. This delay parameter is typically arbitrarily chosen. Instead, we propose to estimate the value of the parameter such that it is sufficient to provide average cycle required for every data item. This delay, however, could be large and lead to huge buffer sizes. Hence we propose twoways to reduce the buffer sizes: (1) in a multiprocessor setup this delay parameter could be redistributed to different processors i.e., apart from the output device, the processors also start after some delay; and (2) allowing tolerable loss in quality. Both these methods show substantial reduction in buffer size. The model we have estimates
the delay parameter in all of the above mentioned techniques. Our mathematical framework fits well to deal with media streams in that it could express variability effortlessly and quickly explore costquality trade offs. These essential attributes of our model substantially brought out the benefits in workload shaping. An important advantage of the workload fitting techniques is from the probabilistic prototypes; relaxing constraints that guarantee full output quality yielded significant reductions in processing and memory requirements.
nossdav05.pdf
Mar 04 2009, 14:30
Speaker: Andrew Gacek
Title: A Framework for Specification, Prototyping, and Reasoning
Abstract:
This talk focuses on the specification of and reasoning about formal systems such as type assignment and evaluation semantics in programming languages. I introduce a logic which allows key aspects of such systems, including variable binding structure within the objects they deal with, to be specified directly and which allows reasoning to be performed over these specifications. Many of these reasoning tasks inductively analyze the structure of terms by instantiating bound variables with fresh free variables. I show how this can be captured in a logical setting through a process of moving binding from the term level to the proof level. It is often necessary in reasoning to be able to identify occurrences of variables captured by such proof level binders and to be able to distinguish between variable occurrences governed by different binders. I describe a new logical device that is capable of capturing such rich properties about binding, and I show how this device can naturally encode informal arguments based on free variable occurrences. Stepping back, I show how many similar features of specifications can be abstracted out by using an intermediate specification logic. I briefly describe how this intermediate specification logic can be given an operational semantics so that specifications can be animated automatically, and I explain how the specification logic can be exploited during reasoning to yield many interesting theorems "for free". Finally, I discuss the implementation of these ideas in the Abella theorem proving system and describe the applications of it that I have explored thus far.
Feb 11 2009, 14:30
Speaker: Marzia Buscemi
Title: A concurrent constraint picalculus: an overview.
Abstract:
We prensent the concurrent constraint picalculus (ccpi), a process calculus that combines two basic programming paradigms: namepassing calculi and CCP. Specifically, we extend CCP by adding synchronous communication and by providing a treatment of names in terms of restriction and structural axioms closer to nominal calculi than to variables with existential quantification. In the resulting framework, constraints can be generated either by a single party or by the synchronisation of two agents. Moreover, restricting the scope of names allows for local stores of constraints, which may become global as a consequence of synchronisations. Our approach relies on a system of named constraints that equip classical constraints with a suitable algebraic structure providing a richer mechanism of constraint combination. We will show some examples, including applications to Service Oriented Computing.
