ABSTRACT. OWL is a logic-based ontology language standard designed to promote interoperability, particularly in the context of the (Semantic) Web. The standard has encouraged the development of numerous OWL reasoning systems, and such systems are already key components of many applications. The 2nd OWL Reasoner Evaluation Competition (ORE 2014) compares and evaluates 11 OWL reasoning systems on a data set containing a wide range of ontologies from the web, obtained through a standard web crawl and the Google Custom Search API, and a snapshot from the well known BioPortal repository. Some user submitted ontologies spice up the corpus with particularly relevant and difficult test cases. The ontologies in the test set are binned by profiles to enable the participation of reasoners specialised on the EL and DL profiles of OWL. The evaluation is performed in three different categories that cover the important tasks of ontology classification, consistency checking, and ontology realisation (i.e., the computation of entailed types of individuals).

ABSTRACT. The 9th SMT competition seeks to spur interest, usefulness, and capability of SMT solvers in application-centric contexts. This year's competition has 20 solvers from 14 participating teams (a record number) with problems drawn from 147K benchmarks in 34 different logics; problems are expressed in a common, standardized format (SMTLIBv2). There are tracks measuring sequential and parallel performance and emulating batch and interactive application environments. The benchmarks are increasingly supplied by application environments that use SMT solvers to discharge constraint problems and verification conditions that arise in software verification, scheduling, component placement and other domains. The competition is run over a period of a month using the StarExec computation cluster. This year there is also a separate, experimental sibling competition on Separation Logic solvers and problems, also using the concrete syntax of SMTLIBv2 benchmarks.

ABSTRACT. Probabilistic model checking (PMC) is a well-established and powerful method for the automated quantitative analysis of parallel distributed systems. Classical PMC-approaches focus on computing probabilities and expectations inMarkovian models annotated with numerical values for costs and utility, such as energy and performance. Usually, the utility gained and the costs invested are dependent and a trade-off analysis is of utter interest. In this paper, we provide an overview on various kinds of nonstandard multi-objective formalisms that enable to specify and reason about the trade-off between costs and utility. In particular, we present the concepts of quantiles, conditional probabilities and expectations as well as objectives on the ratio between accumulated costs and utility. Such multi-objective properties have drawn very few attention in the context of PMC and hence, there is hardly any tool support in state-of-the-art model checkers. Furthermore, we broaden our results towards combined quantile queries, computing conditional probabilities those conditions are expressed as formulas in probabilistic computation tree logic, and the computation of ratios which can be expected on the long-run.

ABSTRACT. It is shown that for any fixed $i>0$, the $\Sigma_{i+1}$-fragment of Presburger arithmetic, \emph{i.e.}, its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for $\Sigma^{\text{EXP}}_{i}$, the $i$-th level of the weak EXP hierarchy. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer \& Rabin in 1974. The second part of the paper applies some techniques developed in the first part in order to establish bounds on sets of naturals definable in the $\Sigma_1$-fragment of Presburger arithmetic: given a $\Sigma_1$-formula $\Phi(x)$, it is shown that the set of solutions is an ultimately periodic set whose period can be doubly-exponentially bounded from below and above.

ABSTRACT. This paper studies the discriminating power offered by higher-order concurrent languages, and contrasts this power with those offered by higher-order sequential languages (à la lambda-calculus) and by first-order concurrent languages (à la CCS). The concurrent higher-order languages that we focus on are Higher-Order pi-calculus (HOpi), which supports higher-order communication, and an extension of HOpi with passivation, a simple higher-order construct that allows one to obtain location-dependent process behaviours. The comparison is carried out by providing embeddings of first-order processes into the various languages, and then examining the resulting contextual equivalences induced on such processes. As first-order processes we consider both Labeled Transition Systems (LTSs) and Reactive Probabilistic Labeled Transition Systems (RPLTSs). The hierarchy of discriminating powers so obtained for RPLTSs is finer than that for LTSs; for instance, in the latter case, the additional discriminating power offered by passivation in concurrency is captured, in sequential languages, by the difference between the call-by-name and call-by-value evaluation strategies of an extended typed lambda-calculus.

ABSTRACT. We study the "approximability" of unbounded temporal operators with time-bounded operators, as soon as some time bounds tend to infinity. More specifically, for formulas in the fragments PLTL$_\Diamond$ and PLTL$_\Box$ of the Parametric Linear temporal Logic of Alur et al., we provide algorithms for computing the limit entropy as all parameters tend to ∞. As a consequence, we can decide the problem whether the limit entropy of a formula in one of the two fragments coincides with that of its time-unbounded transformation, obtained by replacing each occurrence of a time-bounded operator into its time-unbounded version. The algorithms proceed by translation of the two fragments of PLTL into two classes of discrete-time timed automata and analysis of their strongly-connected components.

ABSTRACT. Many important performance and reliability measures can be formalized as the accumulated values of weight functions. In this paper, we introduce an extension of linear time logic including past (LTL) with new operators that impose constraints on the accumulated weight along path fragments. The fragments are characterized by regular conditions formalized by deterministic finite automata (monitor DFA). This new logic covers properties expressible by several recently proposed formalisms. We study the model-checking problem for weighted transition systems, Markov chains and Markov decision processes with rational weights. While the general problem is undecidable, we provide algorithms and sharp complexity bounds for several sublogics that arise by restricting the monitoring DFA.

ABSTRACT. Context semantics is a tool inspired by Girard' s geometry of interaction. It has had many applications from study of optimal reduction to proofs of complexity bounds. However, context semantics have been defined only on lambda-calculus and linear logic. In order to study other languages, in particular languages with more primitives (built-in arithmetics, pattern matching,…) we define a context semantics for a broader framework: interaction nets. These are a well-behaved class of graph rewriting systems. Here, two applications are explored. First, we define a notion of weight, based on context semantics paths, which bounds the length of reduction of nets. This could be used to prove strong complexity bounds for interaction net systems. Then, we define a denotational semantics for a large class of interaction net systems.

ABSTRACT. We graft synchronization onto the most concrete model of Girard’s Geometry of Interaction, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling synchronization points, and a multi-token abstract machine model for it. Interestingly, a correctness criterion ensures the absence of deadlock, this way linking logical and operational properties in a novel way.

ABSTRACT. In Girard's original presentation, proof structures of Linear Logic are hypergraphs whose hyperedges are labeld by logical rules and vertices represent the connections between these logical rules. Presentations of proof structures based on interaction nets have the same kind of graphical flavour. Other presentations of proof structures use terms instead of graphs or hypergraphs. The atomic ingredient of these terms are variables related by axiom links. However, the correctness criteria developped so far are adapted to the graphical presentations of proof structures and not to their term-based presentations. We propose a new correctnes criterion for constant-free Multiplicative Linear Logic with Mix which applies to a coherence space structure that a term-based proof structure induces on the set of its variables in a straightforward way.

ABSTRACT. We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is non-elementary already in the affine case, and match this lower bound for the full propositional affine linear logic, proving its Tower-completeness. We also show that provability in propositional contractive linear logic is Ackermann-complete.

ABSTRACT. Abstract--- We focus on (partial) functions that map input strings to a monoid such as the set of integers with addition and the set of output strings with concatenation. The notion of regularity for such functions has been defined using two-way finite-state transducers, (one-way) cost register automata, and MSO-definable graph transformations. In this paper, we give an algebraic and machine-independent characterization of this class analogous to the definition of regular languages by regular expressions. When the monoid is commutative, we prove that every regular function can be constructed from constant functions using the combinators of choice, split sum, and iterated sum, that are analogs of union, concatenation, and Kleene-*, respectively, but enforce unique (or unambiguous) parsing. Our main result is for the general case of non-commutative monoids, which is of particular interest for capturing regular string-to-string transformations for document processing. We prove that the following additional combinators suffice for constructing all regular functions: (1) the left-additive versions of split sum and iterated sum, which allow transformations such as string reversal; (2) sum of functions, which allows transformations such as copying of strings; and (3) function composition, or alternatively, a new concept of chained sum, which allows output values from adjacent blocks to mix.

The uploaded PDF is the concetation of the short and full versions of the paper.

ABSTRACT. We investigate the computational power of periodically iterated morphisms, also known as D0L systems with periodic control, PerD0L systems for short. These systems give rise to a class of one-sided infinite sequences, called PerD0L words. We construct a PerD0L word with exponential subword complexity, thereby answering a question raised by (Lepisto 1993) on the existence of such words. We solve another open problem concerning the decidability of the first-order theories of PerD0L words (Muchnik, Pritykin, Semenov 2009); we show it is already undecidable whether a certain letter occurs in a PerD0L word. This stands in sharp contrast to the situation for D0L words (purely morphic words), which are known to have at most quadratic subword complexity, and for which the monadic theory is decidable.

ABSTRACT. Two-player games on graphs provide the mathematical foundation for the study of reactive systems. In the quantitative framework, an objective assigns a value to every play, and the goal of player 1 is to minimize the value of the objective. In this framework, there are two relevant synthesis problems to consider: the quantitative analysis problem is to compute the minimal (or infimum) value that player 1 can assure, and the boolean analysis problem asks whether player 1 can assure that the value of the objective is at most r (for a given threshold r). Mean-payoff expression games are played on a multidimensional weighted graph. An atomic mean-payoff expression objective is the mean-payoff value (the long-run average weight) of a certain dimension, and the class of mean-payoff expressions is the closure of atomic mean-payoff expressions under the algebraic operations of max, min, numerical complement and sum. In this work, we study for the first time the strategy synthesis problems for games with robust quantitative objectives, namely, games with mean-payoff expression objectives. While in general, optimal strategies for these games require infinite-memory, in synthesis we are typically interested in the construction of a finite-state system. Hence, we consider games in which player 1 is restricted to finite-memory strategies, and our main contribution is as follows. We prove that for mean-payoff expressions, the quantitative analysis problem is computable, and the boolean analysis problem is inter-reducible with Hilbert's tenth problem over rationals --- a fundamental long-standing open problem in computer science and mathematics.

ABSTRACT. To ensure consistency and decidability of type checking, proof assistants impose a requirement of productivity on corecursive definitions. In this paper we investigate a type-based alternative to the existing syntactic productivity checks of Coq and Agda, using a combination of guarded recursion and quantification over clocks. This approach was developed by Atkey and McBride in the simply typed setting, here we extend it to a calculus with dependent types. Building on previous work on the topos-of-trees model we construct a model of the calculus using a family of presheaf toposes, each of which can be seen as a multi-dimensional version of the topos-of-trees. As part of the model construction we must solve the coherence problem for modelling dependent types in locally cartesian closed categories simulatiously in a whole family of locally cartesian closed categories. We do this by embedding all the categories in a large one and applying a recent approach to the coherence problem due to Streicher and Voevodsky.

ABSTRACT. Negation is not involutive in the λC calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements.
We introduce polarised, untyped, calculi compatible with extensionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The involution is due to the ℓ delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a constructive interpretation to falsity. We describe the isomorphism there is between A and ¬¬A, and thus between ¬∀ and ∃¬.

ABSTRACT. Homotopy type theory is an extension of Martin-L\"of type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of \emph{Eilenberg-MacLane spaces}. For an abelian group $G$, an Eilenberg-MacLane space $K(G,n)$ is a space (type) whose $n^{th}$ homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in $G$. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.

ABSTRACT. It is an interesting program to investigate the relationship between the proof theory of second order arithmetic and more general second order systems (e.g. theories of sets and classes such as von Neumann-Bernays-Goedel set theory and Morse-Kelley set theory). Which proof-theoretic results can be lifted from second order arithmetic to theories of sets and classes, for which is this not the case, and what are the reasons? What is specific of second order number theory and what additional insights can we gain?

One of the crucial questions is how to distinguish between "small" and "large" in the various contexts. In second order arithmetic, the small objects are the natural numbers whereas the large objects are the infinite sets of natural numbers. Hence it seems natural to identify the small objects in sets and classes with sets and the large objects with proper classes.

As long as only comparatively weak systems are concerned, the moving up from second order arithmetic to sets and classes seems to be a matter of routine. However, as soon as well orderings enter the picture, the situation becomes interesting. In second order arithmetic, every $\Pi^1_1$ statement is equivalent to the question whether a specific arithmetic relation is well ordered; on the other hand, in set theory a simple elementary formulas expresses the well foundedness of a given relation.

We propose studying the (new) notion of weak well order in sets and classes as the proof-theoretically adequate analogue of well order in second order arithmetic. To support this claim several results about inductions and recursions in connection with weak well orders will be presented. This is joint work with D. Flumini.

ABSTRACT. We discuss the automation of inductive proof.