A method is presented for checking global conditions for object system designs by checking the object models concerned, i.e. referred to in the condition, and their mutual communication requirements. The method deals with one object at a time, thus avoiding state space explosion. The approach is demonstrated using model checking, but the idea works for other approaches to verification or testing as well. A multi-object variant of CTL is used for expressing global conditions, making the system structure sufficiently visible to enable automatic translation into local conditions for the objects concerned, and for the communication requirements among them. The former as well as the latter can be verified independently using standard model checkers. The method is illustrated by a large example where our method shows a spectacular speedup over global model checking.
A modular sequent calculus labelled with truth values is defined for dealing with a wide class of modal systems. Completeness is established over an algebraic semantics. Some classes of frames are shown to be characterized precisely within the calculus. Normalization and cut elimination results are stated and discussed. This talk reports ongoing joint work with P. Mateus, C. Sernadas and L. Viganò.
We investigate the question of obtaining a binary semantics for many-valued logics, in the lines of the so-called "Suszko's Thesis". Taking into account the issue of separability of truth-values, we develop a general algorithmic method to transform any truth-functional finitely-valued semantics into a manageable form of (possibly) non-truth-functional binary semantics, conformant with a certain clausal specification, to which we call "dyadic semantics". We also hint at how a dyadic semantics directly induces a tableau decision procedure for the logic, and provide several application examples, covering Gödel, Lukasiewicz and Kleene logics, as well as some paraconsistent systems. This talk is on ongoing joint work with W.A. Carnielli, M.E. Coniglio and J. Marcos from GTAL, UniCamp, Brazil.
We extend the quiescent model with two operators denoting global liveness requirements: ! and [-]. When the operator ! is applied to a process term we obtain the maximum activation of the corresponding process. The operator [-] applied to a process term induces a transactional behaviour until the execution of some determined action. The suitable semantics domains (denotational, axiomatic, and operational) are obtained through the introduction of new sets of traces, new axioms and new transition rules. The final result is a trinity in the sense of Hennessy (equivalencies among the three semantics domains).
We define (set-theoretic) notions of intensional Henkin model and syntactic lambda-algebra for Moggi's partial lambda-calculus. These models are shown to be equivalent to the originally described categorical models via the global element construction; the proof makes use of a previously introduced construction of classifying categories. The set-theoretic semantics thus obtained is the foundation of the higher order algebraic specification language HasCASL, which combines specification and functional programming.
The GPAC model was one of the pioneer models for analog computation and was intended to be an abstract model for a computing device, the Differential Analyzer. In this seminar we further exploit this model. In particular we show that, provided we enrich the original model with a unit capable of generating a non-analytic function satisfying some simple conditions, then for each Turing machine we can find a GPAC that simulates any computation of this particular Turing machine. We will show in detail how this argument works and we will also discuss the possibility of introducing complexity measures for the GPAC that can be related with standard complexity measures.
Sufficient conditions are established for the completeness of (world) labelled first-order based logics. These conditions are shown to be preserved by fibring, leading to the preservation of completeness. A comparison with non-labeled approaches is outlined. Some examples are given involving modal and relevance logics.
It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement this algorithm on a computer; moreover, one runs the risk of making mistakes in the process. From a fully formalized constructive proof one can in theory automatically obtain a computer implementation of such an algorithm. As an example we consider the fundamental theorem of algebra; on the first attempts to extract a program from its formalization, the computer ran out of resources. We will discuss how we used logical techniques to extract a feasible(!) program. This example is used as a motivation for a broader perspective on how the formalization of mathematics should be done with program extraction in mind.
In his famous lecture in Paris 1900 Hilbert formulated 23 challenging mathematical problems which inspired many groundbraking mathematical investigations in the last century. Among these problems the 13th asked for nomographical solutions of certain function equations. Hilbert's own supposition was that for certain equations of higher degree no such solution can be constructed. Surprisingly, 57 years later it appeared that Hilbert was wrong when Kolmogorov suceeded to prove his Superposition Theorem which states that each multivariate continuous real-valued function can be represented as superposition and composition of one-dimensional continuous functions. Again 30 years later this theorem got an interesting application in the theory of neural networks. We will discuss a computable version of Kolmogorov's Superposition Theorem which states that each multivariate computable real-valued function can be represented as superposition and composition of one-dimensional computable real number functions. As a consequence we can characterize the computational power of feedforward neural networks with one hidden layer and computable activation functions precisely.
The state and situation calculus (SSC) that can be used for specifying distributed, reactive systems is shown to be quite convenient for reasoning about such specifications, not only for verification purposes but also when revising specifications found to be inappropriate. To this end, abductive reasoning techniques are established for SSC. This talk reports ongoing joint work with P. Gouveia.
The modular sequent calculus labelled with truth values for modal systems is revisited. Completeness is obtained over the natural algebraic semantics and over the traditional general Kripke semantics. A duality between the two semantics is established. A simple enrichment of the calculus is shown to be complete over standard Kripke semantics. Rules are given characterizing different properties of the accessibility relation among general frames. Analyticity of the calculus is discussed. This talk reports ongoing joint work with P. Mateus, C. Sernadas and L. Viganò.
This is an initial systematic study of the properties of negation from the point of view of abstract deductive systems. I will start the ball rolling by discussing the unifying representational formalism adopted, which involves multiple-consequence relations. I will then concentrate on what negation can be, showing the interrelations among a great number of positive contextual sub-classical properties of negation. All properties are important, but some are more important than others: I will argue next that more attention should be paid to negative properties in the specification of what a logic or a logical constant is.
Many of the familiar logical systems have an algebraic counterpart. A logic S is said to be algebraizable if there exists a quasivariety Alg(S) such that the consequence relation |- over S and the equational consequence relation |= over Alg(S) are interpretable in one another in a certain strong sense. For algebraizable logics S many metalogical properties of the logic S are known to transfer into natural algebraic properties of the associated class of structures Alg(S), and vice versa. For example, it is well-known that interpolation properties of an algebraizable logic S relate to amalgamation properties of Alg(S). A logical system has the Beth (definability) property if every “implicitly” definable notion has an explicit definition relative to the logic. Andreka, Németi and Sain first, and Hoogland later, explored the connection between the Beth property and the algebraic property EP of “epimorphisms being surjective”'. I will discuss the properties and their connection, and show how it carries over to a class of logics wider than the algebraizable ones. The results will be illustrated by applying them to various familiar non-classical logics.
Metaprogramming is programming on syntax, as we do to implement lambda-calculus reduction, or proof-search in a sequent logic. We bind names with lambda and generate eigenvariables with forall introduction in the two examples above. The usual notion of syntax is "abstract syntax tree" but this provide an unsatisfactory abstract model of these phenomena. There is a need for a notion of "abstract syntax tree" in which variable names may be literally bound and generated, in some suitable mathematical sense. I shall present Fraenkel-Mostowski (FM) sets, which is ZFA set theory (ZF set theory with atoms) with one extra axiom. I shall show how this set theory sustains an improved model of syntax in which binding and name-generation are set-theoretic phenomena whose application to sets representing abstract syntax trees coincides with our usual concrete constructions on syntax. I will conclude with a brief discussion of the significance of this discovery for programming and logic.
The definitions of recursive and G-recursive functions will be recalled. Then some fundamental results and properties of these functions will be presented. Especially their relation to Baire classes and effective Baire classes will be considered. The connections between these notions and analog computations will be analysed. The meaning of a differential recursion, minimalization operator and infinite limits in the above context will be discussed. Also the place of hierarchies of real recursive functions in descriptive set theory will be studied.
Combined logics are essential for reasoning about complex systems. In this work we analyze three mechanisms for combining logics (synchronization, parameterization and fibring) and show how they can be represented in the context of the theory of institutions by exploring the connections between them. For the purpose we adopt the notion of heterogeneous specification as a structured specification in a suitable Grothendieck institution, as proposed by R. Diaconescu. The talk reports ongoing joint work with C. Caleiro e J. Ramos.
We propose an alternative algebraic semantics for modal logic, using quantales. To this end, we start by introducing the notion of d-quantale, based on which we obtain a conservative extension of the traditional algebraic semantics of modal logic. This extension leads, in particular, to a generalization of the correspondence between Kripke structures and modal algebras, in a way that is useful for instance in understanding the specification of transition systems by means of branching temporal logic.
Interpolation in the context of sequent calculi labelled with truth values. Global interpolation, local interpolation and arrow interpolation and their relationship. Constructive (proof-theoretic) versus non-constructive (model-theoretic) proofs. General (constructive) result of interpolation for well behaved sequent calculi. The modal and first-order sequent calculi as particular examples. Preservation of interpolation when fibring logics.
I introduce Constraint Differentiation, a new technique for reducing search when model-checking security protocols. The technique is based on eliminating certain kinds of redundancies that arise in the search space when using symbolic exploration methods, in particular methods that employ constraints to represent and manipulate possible messages from an active intruder. Formally, we have proved that Constraint Differentiation terminates and is correct and complete, in that it preserves the set of reachable states so that all state-based properties holding before reduction (such as the existence of an attack) hold after reduction. Practically, we have integrated this technique into OFMC, a state-of-the-art model-checker, and demonstrated its effectiveness by extensive experimentation. Our results show that Constraint Differentiation substantially reduces search and considerably improves the performance of OFMC, enabling its application to a wider class of problems. The talk reports ongoing joint work with David Basin and Sebastian Moedersheim.
State merging algorithms have emerged as the solution of choice for the problem of inferring an unknown regular grammar consistent with a given set of labeled samples, a known NP-hard problem of great importance in the grammatical inference area. These methods derive a small deterministic finite automaton from a set of labeled strings by merging parts of the augmented prefix tree acceptor that corresponds to this set. Experimental and theoretical evidence have shown that the generalization ability exhibited by the resulting automata is highly correlated with the number of states in the final solution. In this talk, we survey existing algorithms that search the tree of possible mergings, and compare their performance in a number of existing benchmarks.
The correlation between interpolation theorems of logic and certain properties of the class of models related to the amalgamation property is well known. In classical sentential and first-order logic it takes the form of a correspondence between Craig's interpolation theorem and Robinson's joint consistency lemma. In the algebraic versions of these logics the joint consistency property can be replaced by the amalgamation property for Boolean algebras and locally finite cylindric algebras. The connection between interpolation and amalgamation has also been explored in the context of intermediate and modal logics, equational logic, and general deductive systems in the sense of Tarski. More recently, logical interpolation results have been shown to have interesting applications for the specification of abstract data types, especially with regard to the important problem of modularization. In the present paper we take advantage of the new domain of abstract algebraic logic to present a unified theory of interpolation, joint consistency, model extension, and amalgamation that comprehends all these results. In this general context the Craig interpolation property ramifies into several different interpolation-like properties, one of which is closely related to the familiar congruence extension property of universal algebra. We show how under quite weak conditions on the logical system, each interpolation property is equivalent to an extension or amalgamation-type property of the appropriate model class.
We investigate the behavioral proof theory of a general class of equational specification logics, the hidden equational logics (HELs). We point out the strict relationship between Abstract Algebraic Logic and the study of the Behavioral Equivalence in HELs by generalizing some concepts and tools of Abstract Algebraic Logic to Specification Theory. Among other results we characterize the behaviorally valid conditional equations of a HEL as those conditional equations which, in a natural sense, do not increase the deductive power of the logic when they are added as new rules of inference. We also characterize the HELs whose behavior is specifiable by a (non-hidden) equational logic in terms of a special class of equivalential logics.
It is well known that constructive proofs of mathematical statements implicitly contain an algorithm within them. However, actually obtaining a computer program from a formalized proof can be far from straightforward. In this talk, a constructive proof of the Fundamental Theorem of Algebra will be examined as a non trivial case study. The extracted program has many surprising properties, and it will be discussed how a careful look at this program can provide interesting insights on the process of formalization.
We present a parallel algorithm for the efficient extraction of binding-site consensus from genomic sequences. This algorithm is based on an existing approach for extracting structured motifs. A structured motif consists of an ordered collection of $p$ boxes, $p$ substitution rates and $p-1$ distances between successive boxes. The contents of the boxes, which represent the extracted motifs, are unknown at the start of the process and are found by the algorithm using a suffix tree as the fundamental data structure. By partitioning the structured motif searching space we divide the most demanding part of the algorithm by a number of processors that can be loosely coupled. In this way we obtain, under conditions that are easily met, a speedup that is linear on the number of available processing units. This speedup is verified by both theoretical and experimental analysis.
We present the "generalised multiary lambda-calculus" (gm-lambda), an extension of the lambda-calculus that corresponds, in the Curry-Howard sense, to a fragment of sequent calculus. Our system is obtained as a generalisation of a system of Schwichtenberg, by allowing a class of cuts and rules for cut- elimination. It also captures, as subsystems, other calculi already known in the literature. Indeed, one of the constructors of gm-lambda is a general kind of application, whose typing rule is an amalgamation of von Plato's generalised elimination rule and Herbelin's head-cut. The computational reading of such construction is as a function applied to a list of arguments and then explicitly substituted in another term. We define a set of permutative conversions, prove its confluence and termination and establish the permutability theorem: two gm-terms determine the same lambda-term iff they are inter-permutable. (This is joint work with Luis Pinto, UM.)
Let $G_1$ be the acyclic tournament with the topological sort $0\lt 1 \lt 2 \lt \dots \lt n \lt n+1$ defined on node set $N\cup \{0,n+1\}$, where $N=\{1,2,\dots,n\}$. The arcs of $G_1$ are therefore the pairs $(i,j)$, with $i \lt j$. Consider the (di)graph $G_2$ obtained by taking two copies of every arc in $G_1$ and colouring one blue and the other red. A 2-colour partition of $N$ (2-CP, for short) is a pair of a blue and a red (di)paths, both from $0$ to $n+1$, such that each node of $N$ is included in exactly one path. If each blue and red arc has a real cost, the cost of a 2-CP is the sum of the costs of the arcs in the two paths. We show that a minimum cost 2-CP may be found in polynomial time, and give a complete description of the convex hull of the incidence vectors of 2-colour partitions of $N$. There is a natural generalization of 2-CPs when $k\gt 2$ colours are present. We state some results on $k$-CPs.
In the last years, recursive functions over the reals [Moore] have been considered, first as a model of analog computation, and second to obtain analog characterizations of classical computational complexity classes [Campagnolo]. However, one of the operators introduced in the seminal paper by Cris Moore (in 1996), the minimalization operator, has not be considered: (a) although differential recursion (the analog counterpart of classical recurrence) is, in some extent, directly implementable in the General Purpose Analog Computer of Claude Shannon, analog minimalization is far from physical realizability, and (b) analog minimalization was borrowed from classical recursion theory and does not fit well the analytic realm of analog computation. In this paper we show that a most natural operator captured from Analysis - the operator of taking a limit - can be used properly to enhance the theory of recursion over the reals, providing good solutions to puzzling problems raised by the original model. Moreover, we show that the classical halting problem is analog solvable, a result that has some impact on the computational power of continuous dynamic systems. The talk reports ongoing joint work with J. Félix Costa.
Existe um contexto social que é motivado e originário dos sistemas de informação: aquilo que chamamos Sociedade da Informação (SI). Em democracia a regulação social exerce-se através do direito; por isso surgem imediatamente questões: Faz sentido falar de direitos específicos da SI ou basta transpor para o novo contexto os direitos actuais? Nesse caso, será necessário redifinir ou re-especificar direitos? Na SI bastam os mecanismos usuais de garantia de direitos ou são necessárias soluções alternativas; que soluções tecnológicas podem dar essas garantias? Procurarei motivar uma resposta tecnológica através de quatro exemplos/problemas: valor probatório dos documentos e das comunicações electrónicos, identificação dos cidadãos e protecção de dados pessoais, preservação da propriedade intelectual e voto electrónico.
Overview of the endogenous and exogenous approaches to the semantics of probabilistic logic. Language, semantics and deductive system of EPPL (Exogenous Probabilistic Propositional Logic). Evaluation of what can be expressed in EPPL. Outline of the proof of completeness. Brief reference to future developments of the proposed technique for probabilizing logics. The talk is a follow up of the presentation by A. Sernadas at the Portuguese Category Seminar 2003 in Coimbra and reports ongoing joint work with A. Sernadas, C. Sernadas and A. Pacheco.
This is a sequel to our previous two talks in the TC Seminar Series one year ago. In those talks we discussed two knot invariants, the knot quandle and counting colorings from the knot quandle to a labelling quandle. We stressed that since the knot quandle was given via a presentation it was not a good tool at telling knots apart. We also remarked that the apparently innocuous counting of colorings was in fact highly efficient in distinguishing knots - joint work with F. M. Dionisio. In this talk we discuss the one dimension higher analogs of knots, knotted surfaces i.e., the embeddings of spheres, tori, ... in four space. We will show that quandles and counting colorings are important invariants again in this setting. Finally we will show the results we obtained in telling apart elements from families of knotted surfaces - joint work with J. Bojarczuk.
We present an overview of a soon-to-start FCT-funded project centered on Contract Guided System Development, a software methodology that aims at producing provably correct applications. The methodology integrates specification, design, and verification, based on the concept of contracts. We intend to follow three complementary directions. The first develops a means to prove the correctness of a class with respect to its specification, written in an assertion language that is in turn expressive and easy to master. The second direction builds a formal specification of abstract data types that is effective in driving the identification of the contracts that must be verified by implementing classes. The third produces tools that generate Java interfaces equipped with contracts from ADT specifications, and that generate monitored classes from contract-annotated Java classes.
