Title and Abstracts of Invited Talks

Streaming String Transducers

Streaming string transducers dene (partial) functions from input strings to output strings. A streaming string transducer makes a single pass through the input string and uses a finite set of variables that range over strings from the output alphabet. At every step, the transducer processes an input symbol, and updates all the variables in parallel using assignments whose right-hand-sides are concatenations of output symbols and variables with the restriction that a variable can be used at most once in a right-hand-side expression. The expressiveness of streaming string transducers coincides with the class of "regular" transduc- tions that can be equivalently defined using two-way deterministic finite-state transducers and using monadic second-order logic. The problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by finite automata, are solvable in Pspace. These decision procedures also generalize to the model of streaming transducers over data strings|strings over symbols tagged with data values over a potentially infinite data domain that supports only the operations of equality and ordering. We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to such streaming data-string transducers. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.

This talk is based on results reported in [2] and [1].

References
1. Alur, R., Cerny, P.: Expressiveness of streaming string transducers. In: Proc. 30th FSTTCS, pp. 1-12 (2010)
2. Alur, R., Cerny, P.: Streaming transducers for algorithmic verification of single- pass list-processing programs. In: Proc. 38th POPL, pp. 599-610 (2011).

A Symbolic Logic with Exact Bounds for Cryptographic Protocols

This invited talk will describe a formal logic for reasoning about security properties of network protocols with proof rules indicating exact security bounds that could be used to choose key lengths or other concrete security parameters. The soundness proof for this logic, a variant of previous versions of Protocol Composition Logic (PCL), shows that derivable properties are guaranteed in a standard cryptographic model of protocol execution and resource-bounded attack. We will discuss the general system and present example axioms for dig- ital signatures and random nonces, with concrete security properties based on concrete security of signature schemes and pseudorandom number generators (PRG). The quantitative formal logic supports first-order reasoning and reasoning about protocol invariants, taking exact security bounds into account. Proofs constructed in this logic also provide conventional asymptotic security guarantees because of the way that exact bounds accumulate in proofs. As an illustrative example producing exact bounds, we use the formal logic to prove an authentication property with exact bounds of a signature-based challenge-response protocol.

This talk presents joint work with Anupam Datta (Carnegie Mellon University), Joseph Y. Halpern (Cornell University), and Arnab Roy (IBM Thomas J. Watson Research Center).

Acknowledgements. This work was partially supported by the National Science Foundation, the Air Force Oce of Scientific Research, and the Office ofNaval Research.

Univalent Foundations of Mathematics

Over the last two years deep and unexpected connections have been discovered between constructive type theories and classical homotopy theory. These connections open a way to construct new foundations of mathematics alternative to the ZFC. These foundations promise to resolve several seemingly unconnected problems|provide a support for categorical and higher categorical arguments directly on the level of the language, make formalizations of usual mathematics much more concise and much better adapted to the use with existing proof assistants such as Coq and finally to provide a uniform way to approach constructive and "classical" mathematics. I will try to describe the basic construction of a model of constructive type theories which underlies these innovations and provide some demonstration on how this model is used to develop mathematics in Coq.

Relational Concepts and the Logic of Reciprocity

Research in logical semantics of natural language has extensively studied the functions denoted by expressions like each other, one another or mutually. The common analysis takes such reciprocal expressions to denote $\langle 1,2\rangle$ generalized quantifiers over a given domain $E$, i.e. relations between subsets of $E$ and binary relations over $E$. One of the reoccurring problems has been that reciprocal expressions seem to denote different quantifiers in different sentences. For instance, the reciprocal expression each other means the different quantifiers $Q_1$ and $Q_2\subseteq \wp(E)\times\wp(E^2)$ in sentences (1) and (2), respectively.

(1) The girls know each other.
$Q_1 = \{\langle A,R\rangle : |A|\geq 2 \; \wedge \; \forall x,y \in A\,[x\not=y\rightarrow R(x,y)]\, \}$

(2) The girls are standing on each other.
$Q_2 = \{\langle A,R\rangle : |A|\geq 2 \; \wedge \; \forall x \in A\,\exists y\in A \, [x\not=y\wedge (R(x,y)\vee R(y,x))]\, \}$

Following previous work on reciprocals [1-4] I will suggest that the quantifier that a reciprocal expression denotes takes as parameter certain logical/cognitive semantic properties of relational concepts -- intensions of two place predicates. In simple cases this parametrization only involves familiar properties like asymmetry or acyclicity, cf. the relation stand on in (2). However, in more complex cases, also preferences of use and other contextual parameters should be formally described as affecting the logical semantics of reciprocity. The precise formalization of such parameters and their affects on the selection of reciprocal quantifiers will be analyzed, based on recent joint work, logical as well as experimental, with Nir Kerem, Eva Poortman, Sivan Sabato and Naama Friedmann.

References
[1] Dalrymple, M., Kanazawa, M., Kim, Y., Mchombo, S., Peters, S.: Reciprocal expressions and the concept of reciprocity. Linguistics and Philosophy 21, 159--210 (1998).
[2] Kerem, N., Friedmann, N., Winter, Y.: Typicality effects and the logic of reciprocity. In: Proceedings of SALT19 (Semantics and Linguistic Theory) (to appear).
[3] Sabato, S., Winter, Y.: From semantic restrictions to reciprocal meanings. In: Proceedings of FG-MOL (2005).
[4] Winter, Y.: Plural predication and the Strongest Meaning Hypothesis. Journal of Semantics 18, 333--365 (2001).

Logic in the Time of WWW: an OWL View

This paper analyses the classical automated reasoning problem---given a theory $\mathcal{T}$, a set $\mathcal{A}$ of ground atoms and a formula $\varphi$, decide whether $(\mathcal{T}, \mathcal{A}) \models \varphi$---in the context of the \OWLT{} Web Ontology Language and ontology-based data access (OBDA).
In a typical OBDA scenario, $\mathcal{T}$ is an \OWLT{} `ontology' providing a user-oriented view of raw data $\mathcal{A}$, and $\varphi(\vec{x})$ is a query with answer variables $\vec{x}$. Unlike classical automated reasoning, an important requirement for OBDA is that it should scale to large amounts of data and preferably be as efficient as standard relational database management systems.
There are various ways of formalising this requirement, which give rise to different fragments of first-order logic suitable for OBDA. For example, according to the \emph{query-rewriting approach} of [1], given $\mathcal{T}$, $\mathcal{A}$ and $\varphi(\vec{x})$, one has to compute a new query $\varphi'(\vec{x})$, independently of $\mathcal{A}$, such that, for any tuple $\vec{a}$, $(\mathcal{T}, \mathcal{A}) \models \varphi(\vec{a})$ iff $\mathcal{A} \models \varphi'(\vec{a})$. As a result, this approach can only be applicable to the languages for which query-answering belongs to the class $\ACz$ for \emph{data complexity} (that is, if only $\mathcal{A}$ is regarded as input, whereas both $\mathcal{T}$ and $\varphi$ are regarded as fixed). In the \emph{combined approach} to OBDA [4,2], given $\mathcal{T}$, $\mathcal{A}$ and $\varphi(\vec{x})$, one has to compute new (i) $\mathcal{A}'\supseteq \mathcal{A}$ in polynomial time in $\mathcal{T}$ and $\mathcal{A}$, and (ii) $\varphi'(\vec{x})$ in polynomial tome in $\mathcal{T}$ and $\varphi$ such that, for any tuple $\vec{a}$, $(\mathcal{T}, \mathcal{A}) \models \varphi(\vec{a})$ iff $\mathcal{A}' \models \varphi'(\vec{a})$. The combined approach can be used for languages with polynomial query-answering.
One focus of this paper is on the fragments of first-order logic complying with such conditions imposed on OBDA.
Another focus is on the following problem: given theories $\mathcal{T}_1$, $\mathcal{T}_2$ and a signature $\Sigma$, decide whether, for all $\mathcal{A}$ and $\varphi(\vec{x})$ formulated in the language of $\Sigma$, we have $(\mathcal{T}_1, \mathcal{A}) \models \varphi(\vec{a})$ iff $(\mathcal{T}_2, \mathcal{A}) \models \varphi(\vec{a})$ (that is: $\mathcal{T}_1$ and $\mathcal{T}_2$ give the same answers to any $\Sigma$-query over the same $\Sigma$-data). In the \OWLT{} setting, an efficient solution to this problem would facilitate various stages of ontology developing and maintenance such as ontology versioning, refining, reusing, or module extraction [3]

References
[1] Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning and efficient query answering in description logics: The DL-Lite family. J. of Automated Reasoning 39, 385{429 (2007).
[2] Kontchakov, R., Lutz, C., Toman, D.,Wolter, F., Zakharyaschev, M.: The combined approach to query answering in DL-Lite. In: KR (2010)
[3] Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison and module extraction, with an application to DL-Lite. AI 174, 1093-1141 (2010)

Last modified: April 22, 12:04pm GMT-3.