CRI Workshop on Semantics in Computation  

In Honor of Jeffery Zucker

McMaster University, Canada

Wednesday, 23rd December, 9:45 – 18:30
Room  570 – Education Building –University of Haifa

On Tarskian Structures in Concurrency (How to Classify Bakery like Protocols)


Uri Abraham

Ben-Gurion University, Israel


We shall argue that predicate languages and their Tarskian structures have an important place for the study of concurrency. The argument is based on an example. We analyze two algorithms that are intuitively similar and seem to employ the same idea:  Lamport's Bakery Algorithm and the Ricart and Agrawala algorithm. On one hand, they are quite different because one uses
shared memory and the other message passing for communication. Yet it is intuitively obvious that they are in some sense very similar, and belong to the same "family of Bakery Algorithms''.

Our aim is to express, in a formal way, this similarity by describing abstract high-level properties that are shared by the two algorithms. For this aim we use a predicate language to express properties that are satisfied by every Tarskian system execution that models a run by either one of the protocols—properties that are strong enough to ensure that the mutual exclusion property holds in these runs.

Following this example, we discuss the thesis that Tarskian structures, which are so abundant in all fields of mathematics, can also find a place in the study of concurrency.






Non-deterministic Matrices and Modular Semantics of Rules


Arnon Avron

Tel Aviv University, Israel


We show how one can provide, in many cases, simple modular semantics for rules of inference, so that the semantics of a system is obtained by joining the semantics of its rules in the most straightforward way. Our main tool for this task is the use of finite non-deterministic matrices, which are multi-valued structures in which the value assigned by a valuation to a complex formula can be chosen non- deterministically out of a certain nonempty set of options.








Role of Computational Type Theory in the Semantics of Languages and Systems


Prof. Robert Constable

Cornell University, USA


Type theories play a major role in modeling and reasoning about software systems, programming languages, and natural languages. For instance, the HOL type theory based on Church's simplification of Russell's theory of types is applied in verifying properties of software with the widely used HOL theorem provers; HOL provers are also used in formalizing mathematics.

Type theories such as the Calculus of Inductive Constructions (CIC) and Computational Type Theory (CTT) are constructive logics, and the theorem provers based on them allow the extraction of correct-by-construction software. These type theories use the propositions-as-types principle which was also the basis of the Automath type system to which Jeff Zucker made major contributions.

This lecture will illustrate recent advances in CTT and show how they contribute to providing the semantics of distributed systems and to verifying the protocols that are the basis of cloud computing.  In particular we look at the basis for security protocols and the connections to nominal logics, and we examine the semantic basis for co-inductive types and their role in the semantics of processes, another subject which Jeff Zucker has advanced. We also look at the foundational issues raised by a constructive theory of domains as the basis for programming language semantics.







Formalizing Analog Algorithms


Nachum Dershowitz

Tel Aviv University, Israel


I will discuss an attempt at the formalization of analog algorithms, in their wide generality, by extending the framework of abstract state machines, due to Yuri Gurevich, to continuous-time models.




Understanding Aspects: Their Semantics, Specifications, and Verification


Prof. Shmuel Katz

Technion, Israel


An aspect is an extension to object-oriented languages that allows a modular definition of code treating a concern which either cuts across the normal class hierarchy of a system or that would otherwise be scattered within irrelevant code. Denotational, abstract state machine, and system transformer semantic views of aspects are presented, and the implications for the specification and verification of aspects are considered.






Monitoring Partial Order Snapshots


Doron Peled

Bar-Ilan University, Israel


Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Examples of such properties are serializability of a database or snapshots. Recently, a modest extension for LTL by an operator that expresses snapshots has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot (also called a slice or a cut) was passed, perhaps not in the observed (interleaved) execution sequence, but possibly in a (trace) equivalent one. A model checking algorithm was suggested for a subset of this logic, with PSPACE complexity in the size of the system and the checked formula. For the whole logic, a solution that is in EXSPACE in the size of the system (PSPACE in the number of its global states) was given.

In this paper, we provide a model checking algorithm in PSPACE in the size of a system of communicating sequential processes when restricting snapshots to boolean combinations of local properties of each process. Concerning size of the formula, it is PSPACE for the case of snapshot properties expressed in DNF, and EXPSPACE where a translation to DNF is necessary.






Fixed-point Semantics for Analogue Computation on Metric Algebras


Jeffery Zucker

McMaster University, Canada


We define a general concept of a network of analog modules connected by channels, processing data from a metric space A, and operating with respect to a global continuous clock T. The network's inputs and outputs are continuous streams u: T ® A, and its input-output behaviour is modeled by a functional F on the set C[T,A] of all continuous streams equipped with the compact-open topology.  We give a semantics which involves solving a fixed point equation over C[T,A] using a contraction principle.  We show that if the module
functions are continuous then so is the network function F. This is significant in terms of Hadamard's principle.  We present a case study involving mechanical systems.

We introduce two computation models on C[T,A]: one "concrete", in the sense of recursive analysis, and the other "abstract", based on a high level programming
language on C[T,A].  We show that these models are equivalent, and that if the module functions are computable (w.r.t. either of them) then so is F.

This is joint work with J.V. Tucker (Swansea).