Abstracts

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.

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].

REFERENCES

[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).

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'.

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.

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.

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.

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.

Thesis Abstract 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.

nossdav05.pdf