Dec 09 2009, 14:30
Speaker: Paolo Baldan
Title: Open Petri nets, Compositionality and Asynchrony
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 truly-concurrent 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
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 right-unit 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 tool-set 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, Springer-Verlag, 2010.
Nov 25 2009, 10:00
Speaker: Jesus Aranda
Title: On the Expressivity of Infinite and Local Behaviour in Fragments of the Pi-calculus (Rehearsal PhD talk)
The pi-calculus [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 language-based formalisms (e.g., logic, formal grammars and the lambda-calculus) 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 pi-calculus 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 zero-adic variant of the (polyadic) pi-calculus, 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 non-faithful 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 termination-preserving CCS! processes can generate languages which are not Type 2. We finally conjecture that the languages generated by termination-preserving CCS! processes are Type 1 .
We also observe that the encoding of RAMs [BGZ04] and several encoding of Turing-powerful formalisms in pi-calculus 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 restriction-free 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 restriction-free 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 restriction-free 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 pi-calculus, 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 sub-languages of it, each capturing one source of persistence: the persistent-input Api-calculus (PIpi), the persistent-output Api-calculus (POpi) and the persistent Api-calculus (Ppi). In [PSVV06] the authors showed encodings from Api into the semi-persistent 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].
[BGZ04]N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion, replication, and iteration in process calculi. In ICALP-04, volume 3142 of Lecture Notes in Computer Science, pages 307-319. Springer-Verlag, 2004.
[Boudol92] G. Boudol. Asynchrony and the pi-calculus. Technical Report RR-1702, 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 pi-calculus. 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:59-68, 2006.
[Phillips:08]I. Phillips: CCS with priority guards.J. Log. Algebr. Program. 75(1): 139-165 (2008).
Nov 13 2009, 15:30
Speaker: Miguel Andres
Title: Probabilistic Anonymity and Admissible Schedulers.
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 Information-Hiding Systems
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 Church-Turing Thesis: Story and Recent Progress
The Church-Turing 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 Church-Turing 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 Church-Turing 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 higher-order data
The logical framework LF supports specifying formal systems and proofs about them using a simple, powerful technique, called higher-order abstract syntax (HOAS). Recently, it has been for example successfully used to specify and verify guarantees about the run-time 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 dependently-typed functional language which supports programming with data specified in the logical framework LF. First, I will show how to implement normalization for typed lambda-terms 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
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 well-known 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
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
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
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 pi-calculus 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
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 CCS-like 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 (non-interleaving) 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: Application-Specific Workload Shaping in Resource-Constrained Media Players
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, system-level 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.
Much research in system-level 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 on-chip resources.
This thesis proposes techniques to shape multimedia workload so as to effectively utilize on-chip resources such as processor and memory. These shaping techniques attempt to solve the problem in providing guarantees for high-quality media output with minimal on-chip 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 deep-insights 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 two-ways to reduce the buffer sizes: (1) in a multi-processor set-up 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 cost-quality 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.
Mar 04 2009, 14:30
Speaker: Andrew Gacek
Title: A Framework for Specification, Prototyping, and Reasoning
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 pi-calculus: an overview.
We prensent the concurrent constraint pi-calculus (cc-pi), a process calculus that combines two basic programming paradigms: name-passing 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.