In recent years, a number of works have appeared that provide formal definitions of the notion of channel and how different kinds of channels (e.g. authentic, confidential, secure) can be employed in security protocols and web services as a means of securing the communication. In this talk, I will present work that allows us to specify the properties of message exchanges over different kinds of channels, either as an assumption or as a goal, and where communicating agents can use their real names or some pseudonyms. Joint work with Sebastian Moedersheim.

The branching-time logic BCTL* is obtained by referring to a more general semantics than that of CTL* ; namely we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard CTL* validity semantics. In this talk, I will present a sound and complete (labeled) natural deduction system for the until-free version of BCTL* and I will show that it enjoys some good proof-theoretical properties.

The talk will report on the first developments towards the implementation of a fully automated program for the extraction of adequate proof-theoretical counterparts for sufficiently expressive logics characterized by way of a finite set of finite-valued truth-tables. Our implementation has been performed in *ML*, and its application gives rise to an *Isabelle* theory formalizing a given finite-valued logic in terms of classic-like two-signed tableau rules. Intended extensions, improvements and refinements of both our algorithm and its implementation will be commented upon. Joint work with D. Mendonça.

Starting with the work of Pillay (1988) the main line of research on definable groups has been guided by the analogy with real Lie groups. However there are also some striking differences: the correspondence between Lie groups and Lie algebras works well in the simple and semisimple case, but fails in the abelian case. To remedy this, there have been two lines of attack in the study of definable groups. One through the study of generic subsets, a kind of substitute for the Haar measure, the other through the study of the Euler characteristic and other homotopy invariants of a definable group. The two lines of research are highly intertwined and advances in each side have been possible through the advances on the other side. I will give an overwiew of the work of several authors on these topics and if time permits I will present some new results in collaboration with M. Mamino and M. Otero. The prerequisites will be kept to a minimum.

A long term goal of the research in computer science is the analysis and verification of complex systems. These can be theories of mathematics, programs, reactive oder hybrid systems, or large databases. Correctness proofs for such systems can often be reduced to reasoning in complex logical theories (e.g. combinations of numerical theories, theories of data types, certain theories of functions). As the resulting proof tasks are usually large, it is extremely important to have efficient decision procedures. In this talk we discuss situations in which efficient reasoning in complex theories is possible. We consider a special type of extensions of a base theory, which we call local extensions, where hierarchic reasoning is possible (i.e., we can reduce the task of proving satisfiability of (ground) formulae in the extension to proving satisfiability of formulae in the base theory). We give several examples of theories important for computer science or mathematics which have this property. We show that the decidability (and complexity) of the universal fragment of a local theory extension can be expressed in terms of the decidability (resp. complexity) of a suitable fragment of the base theory. We also briefly mention possibilities of modular reasoning in combinations of local theory extensions, as well as possibilities of obtaining interpolants in a hierarchical manner, and some applications in verification and in knowledge representation.

In this talk we investigate the problem of computing the domain of attraction of a continuous-time flow on $\mathbb{R}^2$ for a given attractor. We consider an operator that takes two inputs, the description of the flow and a cover of the attractor, and that outputs the domain of attraction for the given attractor. We show that: (i) if we consider only (structurally) stable systems, the operator is computable; (ii) if we allow all systems defined by $C^1$-functions, the operator is not computable. We also address the problem of computing limit cycles on these systems.

In today’s changing environments organizational design must take into account the fact that business processes are incomplete by nature and that they should be managed in such a way that they do not restrain human intervention. In this seminar we propose the embedding of the features of social software, such as wiki-like features, in the modeling and execution tools of business processes. These features will foster people empowerment in the execution and bottom-up design of business process. Research issues on the implementation of the tool and its methodological impact on Business Process Management are discussed.

The first semantics for modal logic was put forward by Lukasiewicz. It was a three-valued semantics. Later on he proposed also a four-valued semantics. This approach to modal logic was dismissed due to: (1) the oddity of Lukasiewicz's systems (2) the result by Dugundji showing that S5 cannot be characterized by a finite matrix (3) the rise of Kripke semantics. I will show in this talk that: (a) we can built quite intuitive four-valued semantics for modal logic (b) it makes sense to develop modal logics based on finite matrices (c) the equation "modal logic = possible world semantics" is questionable.

In our previous work we have studied several coinductive operational semantics, all of which are proved equivalent, for the While language to describe terminating as well as non-terminating program executions. The operational semantics keep track of all the intermediate states that an execution goes through as a trace (a sequence of states). The trace is finite for a terminating execution and infinite for a non-terminating execution. In this talk I present a Hoare-logic for While, which is proved sound and complete with respect to those operational semantics. As usual, our Hoare-triple consists of a precondition, a statement and a postcondition. The precondition is a predicate on initial states, whereas the postcondition is a predicate on traces. Since a trace contains the full information about an execution, the logic can talk about for instance if an execution is terminating or if an variable is updated infinitely often. My talk will start by introducing a coinductive big-step relational semantics, then present the Hoare-logic. I will explain some interesting design issues on the logic and our strategy for proving its completeness, that we have discovered through many failed attempts. All the results have been formalized in Coq. This is a joint work with Tarmo Uustalu.

Kernel of a digraph (directed graph) is a subset K of its nodes which is a) independet (no edges between nodes in K) and b) dominated by every outside node (having at least one edge to some node in K). (*) Every propositional theory T can be represented as a digraph G and every digraph G as a theory T in such a way that the models of T and kernels of G are in a one-to-one correspondence (and can be constructed from each other). In the finite case of (*), I briefly suggest applications for the algorithm design (transfer of techniques between SAT and kernel-search) as well as for a simple (purely propositional) yet adequate analysis of truth-referential paradoxes. (*) holds also for infinitary propositional logic, relating it to digraphs where nodes may have infinite out-degree. I sketch arguments for a series of equivalences (over $\operatorname{RCA}_0$) between (i) versions of the axiom of choice and (ii) kernel existence in various classes of digraphs.

In this talk we address some central problems of combination of logics through the study of a very simple but highly informative case, the combination of the logic of disjunction (LD) and the logic of conjunction (LC). At first it seems that it would be very easy to combine such logics, but the following problem arises: if we combine LC and LD in a straightforward way, distributivity between both connectives holds. On the other hand, distributivity does not arise if we use the usual notion of extension between consequence relations. The spontaneous generation of distributivity is in fact a paradox and a problem, because the standard view of combination of logics is that the combined logic is the smallest one defined on the combined language, which extends the two combined logics. One could think that there is no paradox because the logic of conjunction and disjunction is necessary distributive, but also someone who knows a bit of lattice theory is aware that non-distributivity is perfectly possible. An analogous phenomenon occurs with the so-called absorption laws, which are generated by the straightforward combination of logics LC and LD and they are valid even in the logic of lattices. On the other hand, these laws do not hold in the least extension of LC and LD. A detailed discussion about this phenomenon, as well as some elucidation for it, is given. This is a join work with Jean-Yves Béziau.

A knot is a closed curve in $\mathbb{R}^3$ which does not intersect itself. If two curves can be deformed continuously one into the other, these represent the same knot. One objective in Knot Theory is to distinguish them up to a continuous deformation. To do this, we use invariants, one of them being the number of r-colorings. A $r$-coloring is an assignment of integers in $\mathbb{Z}_r$ (colors) to the arcs of a knot diagram (projection of a knot in $\mathbb{R}^2$), such that, at each crossing twice the color of the over arc equals $(\mod r)$ the sum of the colors of the under arcs. Assigning the same color to each of the arcs always sets a trivial coloring. But, when do non-trivial colorings exist? And what will be the minimum number of colors used in a non-trivial coloring? To determine this invariant we would have to compute the minimum number of colors for all the (infinitely many) diagrams of a knot! However, it is possible to estimate this minimum for some classes of knots and, sometimes, calculate its exact value. In this talk we will present our results on minimum number of colors for the Turk's head knot.

Sufficient conditions are provided for quantifier elimination to hold in a theory. These conditions are obtained by abstracting away the details present in several specific proofs of quantifier elimination. Category theory was used in some parts in order to make the conditions as general as possible so that they can be applied in a wide range of situations. The conditions have two main purposes:

1. to ensure that satisfaction of existential formulas is reflected by an embedding; and
2. to guarantee the existence of a minimal model extending specific models.

The first goal is obtained by requiring that a theory is $\exists$-adequate and the second by imposing the existence of an adjunction.

Joint work with João Rasga.

In the sequel of the talk of Cristina Sernadas we proceed by recognizing that, in some cases, a minimal model extending another can be obtained by iterating a certain construction, like for instance in the context of algebraically closed fields with the Artin's construction. We provide conditions that guarantee the existence of a $\omega$-limit functor identifying such an extension, when the theories are in $\forall_2$. The conditions are over the base functor and not the limit functor. The results are illustrated by showing that the theory of ACFs enjoy quantifier elimination. Joint work with Cristina Sernadas.