Heterogenous fibring of deductive systems is a longstanding open problem. A solution is presented using the new concept of abstract proof system encompassing commonly used kinds of deductive systems (such as Hilbert, Gentzen and Smullyan calculi). Some results on decidability and the relationship to effective consequence systems are shown. Joint work with A. Sernadas and L. Cruz-Filipe.

Conclusion of the previous talk.

Partiality is important in Mathematics and Computer Science. In the context of graphs, categories of partial graphs homomorphisms are usual but we take a different approach: partiality appears in the internal structure of objects, using an extension of Comma Categories. We define the category Grp of partial graphs (arcs with or without source/target nodes) and total morphisms. The generalization of the framework results in categories of internal partial graphs. We show that Grp is bicomplete. Partial graphs can be used to define computational models like automata. A category of partial automata is constructed. Using an extension of Span Composition it is possible to define the computations of automata.

Sufficient conditions for a sequent calculus to enjoy cut elimination are established for a wide class of first order based logics. The conditions result from the application of traditional cut elimination proof techniques to an arbitrary calculus composed by rules that must satisfy a number of reasonable conditions. Based on the cut elimination theorem, the subformula property and the consistency of these calculi are established.

After a brief review of the language and semantics of EQPL (exogenous quantum propositional logic), a weak complete axiomatization is presented. The proof of completeness is achieved by extending the Fagin-Halpern-Megiddo technique originally proposed in the context of probabilistic logic. Joint work with P. Mateus.

Conclusion of the previous talk.

How difficult is it to evaluate a first-order formula in a (finite) structure? Starting from this question, we introduce some of the central notions of parameterized complexity. Moreover, we present machine characterizations of some of its complexity classes.

The seminal work of Jan Rutten on a description of systems as coalgebras included also the possibility to specify a class of systems via coequations, the dual concept to equational specification of a class of algebras. A coequation is a subset of a cofree coalgebra - and a system satisfies the coequation iff it is injective w.r.t. the subset. This is dual to equations expressed via a congruence of a free algebra (and projectivity expressing that the equations are satisfied). We now develop a logic of coequations by formulating two simple inference rules, and proving that they are sound and complete. As a consequence, we dualize Birkhoff's characterization of equational theories as precisely the fully invariant congruences of the free algebra: we prove that a subset of a cofree coalgebra is a theory iff it is a fully invariant subcoalgebra.

Classical two-valued logic is very well-behaved. Sometimes it is just too much so. Several unwarranted presuppositions and expressive limitations of classical logic have motivated the introduction of many non-classical logics. Among those, paraconsistent logics are attractive in allowing for the consistency presupposition to be defeated and for a non-explosive negation to be expressed. [Some paraconsistent logics, the so-called Logics of Formal Inconsistency, can even express consistency at the object language level.] Now, if you espouse paraconsistency, it will not require from you any pledge of exclusivity. You can be fully loyal to paraconsistency while you flirt, say, with many-valuedness, or with modality. The first paraconsistent systems of deduction (Jaskowski 1948, Nelson 1959, da Costa 1963) failed both to have truth-functional semantics and to respect the replacement property, and for some time people had the impression that these failures were structural features of paraconsistency. We now know they are not. As time went by, we learned that finite-valued paraconsistent logics are feasible, and a similar thing can be said about self-extensional paraconsistent logics. My talk will reconstitute that exciting story to its latest developments. The main concentration will be on modal paraconsistency, where negated statements represent “admissible falsehoods”, as opposed to intuitionistic-like notions of “refutable truths”.

Vários problemas de afectação com preferências têm por modelo o problema dos casamentos estáveis (stable marriage problem) ou suas variantes. A versão clássica trata a formação de $n$ casais estáveis num grupo de $n$ homens e $n$ mulheres, ou seja, tais que não exista um par homem-mulher $ (h,m)$ tal que $h$ prefere $m$ à sua esposa e $m$ prefere $h$ ao seu esposo. Existem vários resultados interessantes sobre este problema, nomeadamente a caracterização da estrutura das soluções dalgumas variantes. Quando as listas de preferências mútuas estão totalmente ordenadas, o problema pode ser resolvido pelo algoritmo de Gale e Shapley (1962), sendo a sua complexidade quadrática em $n$. Mais recentemente, Iwama et al. (1999) e Manlove et al. (2002) provaram que, na presença de indiferença e pares inaceitáveis, algumas variantes são NP-complete ou NP-hard. São apresentados os resultados dum estudo motivado pela polémica suscitada pelo Concurso de Educadores de Infância e de Professores dos Ensinos Básico e Secundário para 2004/05, e ainda pela análise do algoritmo desenvolvido pela empresa que desbloqueou a situação e a intuição de que existia alguma relação entre o problema da elaboração de listas de colocações e o dos casamentos estáveis. Propõe-se uma definição de listas de colocações óptimas segundo os candidatos, no espírito do Decreto-Lei nº 35/2003 que regula o concurso, o qual prevê que os candidatos possam manisfestar igual preferência por várias posições. Mostra-se que tais listas podem ser obtidas em tempo polinomial, mas considerando a dimensão das instâncias reais deste problema, coloca-se a questão de saber se, a curto ou médio prazo, haverá necessidade de introduzir alterações à lei, de forma a garantir que o problema se possa resolver em tempo útil.

When can we say that two distinct logical systems are, nevertheless, essentially the "same"? In this talk we discuss the notion of "sameness" between logical systems, bearing in mind the expressive power of their associated spaces of theories, but without neglecting their syntactical dimension. Departing from a categorial analysis of the question, we introduce the new notion of equipollence between logical systems. We use several examples to illustrate our proposal and to support its comparison to other proposals in the literature, namely Pollard's notion of homeomorphism, Pelletier's notion of translational equivalence (or synonymity), as well as with Post-equivalence, based on the definability of Boolean functions. This talk is on joint work with R. Gonçalves.

Both the formal and computational models of cryptography contain the notion of message equivalence or indistinguishability. When can we say that two equivalent formal messages are mapped into two indistinguishable computational distributions? I.e., when is an encryption scheme sound? So far, none of the existing soundness results holds when the graph of encryption keys of one of the messages is cyclic. In this talk we will see that an encryption scheme provides soundness in the presence of key cycles if it also satisfies the recently-introduced notion of key-dependent message (KDM) security. We also show that soundness in the presence of key-cycles (and KDM security) neither implies nor is implied by the "usual" notions of security, namely chosen ciphertext security (CCA-2). Therefore, soundness for key-cycles is only possible using new notions of security. This talk is joint work with G. Bana, J. Herzog and A. Scedrov.

Todos nós, portugueses, seguimos com atenção o concurso de colocação dos docentes dos ensinos pré-escolar, básico e secundário, ano lectivo de 2004/2005. Pelo que na altura veio a público, ficou claro que no âmago da questão encontrava-se um problema de natureza técnica, matemática, que não fora devidamente valorizado pelo Ministério da Educação. Nesta palestra, pretendemos identificar as questões de índole matemática que se levantam num concurso para colocação de docentes. Em primeiro lugar, iremos perceber como é que da legislação vigente se passa para uma especificação formal. Identificaremos duas especificações possíveis, ambas conformes com a lei, chamando óptima localmente verificável a uma e lexicograficamente óptima à outra. Estas duas especificações têm propriedades diferentes e resultam em colocações diferentes. Em segundo lugar, indicaremos algoritmos para cumprir cada uma das duas especificações. E, em terceiro lugar, enquadraremos o problema da colocação de docentes no contexto dos emparelhamentos estáveis e de peso mínimo, tão queridos dos matemáticos.

The fibring of two sequent calculi can be obtained by combining the languages of both calculi and taking all rules allowed in either calculus. However, proofs in the fibring thus defined have no relationship to proofs in the components, so that these are essentially different objects. In this talk, we propose a novel definition of fibring of two sequent calculi where the notion of derivation is primitive and show that a proof in the fibring is essentially a finite set of proofs in the components structured in a meaningful way. Using this definition we can easily show that fibring preserves cut elimination and decidability of the calculi. This talk is joint work with C. Sernadas.

We consider behavioural pseudo-metrics (a robust variant on bisimulations) for probabilistic transition systems coalgebraically. Our approach relies on Makkai-Pare's theory of accessible categories, which ensures that the free-mean-algebra functor on complete metric spaces admits a final coalgebra. In this talk, I will review the basics of the categorical theory and outline some of the results. Joint with Franck van Breugel, Michael Makkai and James Worrel.

We investigate the intermediate logic RN of the Rieger-Nishimura ladder — the 1-universal model of intuitionistic propositional calculus. The Heyting algebra dual to the Rieger-Nishimura ladder is the 1-generated free Heyting algebra. Is is easy to show that RN is the greatest 1-conservative extension of intuitionistic propositional calculus IPC. The logic RN was first studied by Kuznetsov and Gerciu, Gerciu, and independently by Kracht, whose papers claim interesting results but contain at best sketch proofs, some of which have serious flaws. We provide a systematic study of RN and its extensions. Joint work with Guram and Nick Bezhanishvili.

According to the intuitive definition of combination of logics, the combination of two logics is the smallest conservative extension of both on the combined language. Combining the logic of conjunction with the logic of disjunction by using obvious methods (combination of their Gentzenian rules of their truth-tables) leads to a logic in which distributivity holds, such a logic therefore cannot be considered as the proper combination of the logics of conjunction and disjunction. In this talk I will present several methods to combine properly these two logics: combination of neo-Gentzenian systems, product of matrices and use of non-distributive matrices. Joint work with Ana Teresa Martins.

We present an approach to integrating security into the system design process. Namely, models are made of system designs along with their security requirements, and security architectures are automatically generated from the resulting security-design models. We call the resulting approach "Model Driven Security" as it represents a specialization of model driven development to the domain of system security. To illustrate these ideas we present SecureUML, a modeling language based on UML for modeling system designs along with their security requirements. From SecureUML models, we automatically generate security architectures, built from declarative and procedural access control mechanisms, for distributed middleware-based applications. The process has been implemented in the ArcStyler tool, which generates security infrastructures based on Sun's Enterprise Java Bean standard. We report on case studies using this tool, which illustrate the flexibility and power of our approach.

Neste trabalho são generalizados os métodos de Kalmár e de Henkin para a construção de sistemas lógicos polivalentes com um número arbitrário de valores de verdade. Para tanto, motivados pela teoria de subconjuntos fuzzy, são definidos novos conectivos que generalizam a negação e é introduzido o novo conceito de consistência polivalente que permitirá a discussão da completude, que, no caso infinito-valente dependerá da solução de um determinado problema de extensão que formularemos. Finalmente, é discutida a possibilidade de sistemas paraconsistentes polivalentes.

Modal logic has a good claim to being the logic of choice for describing the reactive behaviour of systems modeled as coalgebras. Logics with modal operators obtained from so-called predicate liftings have been shown to be invariant under behavioral equivalence. Expressivity results stating that, conversely, logically indistinguishable states are behaviorally equivalent depend on the existence of separating sets of predicate liftings for the signature functor at hand. A new classification result for predicate liftings leads to an easy criterion for the existence of such separating sets, and allows one to give simple examples of functors that fail to admit expressive normal or monotone modal logics, respectively, or in fact an expressive (unary) modal logic at all. A remedy to this is to move on to polyadic modal logic, where modal operators may take more than one argument formula. Every accessible functor admits an expressive polyadic modal logic. Moreover, expressive polyadic modal logics are, unlike unary modal logics, compositional. The latter result is best understood in the terminology of syntax constructors and one-step semantics as introduced by Cirstea and Pattinson; it states essentially that polyadic modal logic is closed under the composition of syntax constructors.

Secret or private information may be leaked to an external attacker through the timing behaviour of the system running the untrusted code. We present a transformation technique for preventing timing leaks in finite-state probabilistic systems while preserving the semantics of the original system. The transformation involves the introduction of new "padded" control paths for patching time leaks and attempts to minimise the resulting additional running time overhead. Contrary to previous similar proposals, our padding technique is probabilistic in the sense that the transformation algorithm introduces time leak fixes only with a certain probability whenever they appear to be necessary. The resulting processes are therefore not always perfectly secure; we can nevertheless provide an estimate of their vulnerability by recording and accumulating the probabilities of the applied patches. This allows us to optimise the trade-off between vulnerability against timing attacks and additional costs such as running time, system size, etc.

One of the most important limitations concerning analog computation is the lack of a unifying paradigm. Indeed, while several models of analog computation are known, few connections were established between them. Here we explore this topic and show equivalence between two models, Shannon’s General Purpose Analog Computer (GPAC) and Computable Analysis. In particular, we show that if we modify the notion of computability in the GPAC, and add some mild conditions on the model, then we get exactly the class of functions computable according to Computable Analysis. This talk describes ongoing work with Olivier Bournez and Emmanuel Hainry (done under the supervision of M. Campagnolo and J. Buescu).

AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability. I will survey the different components of the AVISPA Tool, and the underlying analysis techniques, and demonstrate its use on a number of relevant examples.

Formal methods are still expected to improve the practice of software engineering. The areas in which formal methods will play important roles include at least: (1) distributed component software, (2) network/system security, (3) embedded systems. Formal methods are better supported by formal specification languages equipped with formal verification capability. CafeOBJ is a formal specification language equipped with verification methodologies based on algebraic specification technique. CafeOBJ is an executable wide spectrum language based on multiple logical foundations; mainly based on initial and hidden algebras. Static aspects of systems are specified in terms of initial algebras, and dynamic aspects of systems are specified in terms of hidden algebras. CafeOBJ is the first algebraic specification language which incorporates observational (or behavioral) specifications based on hidden algebras in a serious way. Observational specifications in CafeOBJ can be seen as a nice combination of static and dynamic specifications, and facilitate natural and transparent specification and verification of complex systems. This talk explains minimal fundamentals of CafeOBJ, an interactive equational proof method with it, and some practical applications of the method.

I will present a semantic framework for data abstraction and refinement for verifying safety properties of open programs. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its syntax. The fully abstract game semantics of the language is used for model-checking safety properties, and an interaction-sequence-based semantics is used for interpreting potentially spurious counterexamples and computing refined abstractions for the next iteration.

The notion of "most'', when expressed by quantitative means (usual generalized quantifiers), is incomplete and not definable in first-order logic. This justifies the interest on a qualitative approach to quantification, what can be done by the modulated quantifiers, interpreted by means of mathematical structures such as families of principal filters, families of ultrafilters, reduced topologies, etc. Several modulated logics, obtained by extending first-order logic through modulated quantifiers, have been recently studied, as the "Logic of Vast Majority", the "Logic of Many" and the "Logic of Plausibility", which formalize quantified assertions of the kind "for a good number of", "many", "almost everywhere", etc. We discuss the interest of such binding operators, which may be thought as "qualifiers" rather than quantifers, as new foundations for the notions of fuzziness and of majority in social choice theory with infinite voters, addressing some open questions and perspectives.

There are many proofs of various lower bounds on the usual Ramsey numbers. Combinatorialists have been concerned mainly with two issues, obtaining better bounds, and considering constructive versus non-constructive bounds. I will consider some logical aspects, beginning to answer the question: What is the difference between these bounds in terms of the axioms required to prove them? This sort of work fits in with the program of Reverse Mathematics, though here we work with the weaker theories of bounded arithmetic, since they are a more suitable context for finite combinatorics.

Let $K$ be an alternating knot of prime determinant $p$. Consider a minimal diagram, $D$, of $K$ i.e., a diagram of $K$ with least number of arcs. The Kauffman-Harary conjecture states that a $p$-coloring of $D$ assigns different colors to different arcs of any of its minimal diagrams. This conjecture has been proved to be true for rational knots and for Montesinos knots. In this talk we will report on recent work on calculating numbers of colorings and minima of colors without the restriction to minimal diagrams. This is joint work with Louis H. Kauffman.

Several non-supervised machine learning methods have been used in the analysis of gene expression data obtained from microarray experiments. Recently, biclustering, a non-supervised approach that performs simultaneous clustering on the row and column dimensions of the data matrix, has been shown to be remarkably effective in a variety of applications. The goal of biclustering is to find subgroups of genes and subgroups of conditions, where the genes exhibit highly correlated behaviors. These correlated behaviors correspond to expression patterns and can be used to identify relevant biological processes possibly involved in regulatory networks. In the most common settings, biclustering is an NP-complete problem, and heuristic approaches are usually used to obtain sub-optimal solutions using reasonable computational resources. In this talk, we examine a particular setting of the problem, where we are concerned with finding biclusters in time-series expression data. In this context, we are interested in finding biclusters with consecutive columns. The motivation for this problem is the fact that biological processes start and finish in an identifiable contiguous period of time, leading to increased (or decreased) activity of sets of genes that can be identified because they form biclusters with contiguous columns. The relevance of biclusters that span consecutive columns and their importance in the identification of gene regulatory processes is thus evident. For this particular setting of the problem, we present an algorithm based on string processing techniques that finds and reports all relevant biclusters in time linear on the size of the expression matrix.

A contract signing protocol lets two people exchange digital signatures on a pre-agreed text. Optimistic contract signing protocols enable signers to do so without invoking a third party. However, an adjudicating party remains available should one or both signers need timely resolution. We analyze optimistic contract signing protocols using a game-theoretic approach and prove a fundamental impossibility result: in any fair, optimistic, timely protocol, an optimistic player yields an advantage to a strategic opponent. This is joint work with John Mitchell, Andre Scedrov and Vitaly Shmatikov. If time permits, I shall discuss some work on multi-party contract signing protocols.

Following recent developments in the topic of generalized quantifiers, and also having in mind subsequent applications to the area of cleistic logic, we propose a conservative enrichment of first-order logic with almost-everywhere quantification, endowed with measure-theoretic semantics. The completeness of the axiomatization we provide is carried out using a variant of the Lindenbaum-Henkin technique. The independence of the axioms is analysed, and the almost-everywhere quantifier is classified using the taxonomy proposed by Carnielli et al. Joint work with J. Rasga and A. Sernadas.

A full-text index provides fast search for any pattern in a text. Traditional full-text indexes, however, have a serious problem with space usage. A recent trend is to develop indexes that exploit the compressibility of the text so that their size is a function of the size of the compressed text. This field has introduced the concept of self-indexes, which, in addition to providing index capabilities, are capable of replacing the original text. The two most successful lines of research are the ones exploring compressed suffix arrays and the Burrows-Wheeler transform. In this talk we will describe an algorithm that builds an index based on the well known Ziv-Lempel data compression technique. This algorithm represents a significant improvement over previous methods. We expect that it will be very competitive against the two mainstream approaches.