View: session overviewtalk overviewside by side with other conferences
09:15  TradeOff Analysis Meets Probabilistic Model Checking SPEAKER: Christel Baier ABSTRACT. Probabilistic model checking (PMC) is a wellestablished and powerful method for the automated quantitative analysis of parallel distributed systems. Classical PMCapproaches 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 tradeoff analysis is of utter interest. In this paper, we provide an overview on various kinds of nonstandard multiobjective formalisms that enable to specify and reason about the tradeoff 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 multiobjective properties have drawn very few attention in the context of PMC and hence, there is hardly any tool support in stateoftheart 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 longrun.

10:45  Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy SPEAKER: Christoph Haase 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 doublyexponentially bounded from below and above. 
11:15  On the Discriminating Power of Passivation and HigherOrder Interaction SPEAKER: Valeria Vignudelli ABSTRACT. This paper studies the discriminating power offered by higherorder concurrent languages, and contrasts this power with those offered by higherorder sequential languages (à la lambdacalculus) and by firstorder concurrent languages (à la CCS). The concurrent higherorder languages that we focus on are HigherOrder picalculus (HOpi), which supports higherorder communication, and an extension of HOpi with passivation, a simple higherorder construct that allows one to obtain locationdependent process behaviours. The comparison is carried out by providing embeddings of firstorder processes into the various languages, and then examining the resulting contextual equivalences induced on such processes. As firstorder 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 callbyname and callbyvalue evaluation strategies of an extended typed lambdacalculus. 
11:45  Asymptotic behaviour in temporal logic SPEAKER: Aldric Degorre ABSTRACT. We study the "approximability" of unbounded temporal operators with timebounded 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 timeunbounded transformation, obtained by replacing each occurrence of a timebounded operator into its timeunbounded version. The algorithms proceed by translation of the two fragments of PLTL into two classes of discretetime timed automata and analysis of their stronglyconnected components. 
12:15  Weight Monitoring with Linear Temporal Logic: Complexity and Decidability SPEAKER: Sascha Wunderlich 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 modelchecking 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. 
10:45  On Context Semantics for Interaction Nets SPEAKER: Matthieu Perrinel 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 lambdacalculus and linear logic. In order to study other languages, in particular languages with more primitives (builtin arithmetics, pattern matching,…) we define a context semantics for a broader framework: interaction nets. These are a wellbehaved 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. 
11:15  The Geometry of Synchronization SPEAKER: unknown ABSTRACT. We graft synchronization onto the most concrete model of Girard’s Geometry of Interaction, namely token machines. This is realized by introducing proofnets for SMLL, an extension of multiplicative linear logic with a speciﬁc construct modeling synchronization points, and a multitoken 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. 
11:45  A new correctness criterion for MLL proof nets SPEAKER: Thomas Ehrhard 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 termbased presentations. We propose a new correctnes criterion for constantfree Multiplicative Linear Logic with Mix which applies to a coherence space structure that a termbased proof structure induces on the set of its variables in a straightforward way. 
12:15  NonElementary Complexities for Branching VASS, MELL, and Extensions SPEAKER: Ranko Lazić ABSTRACT. We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new nonelementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is nonelementary already in the affine case, and match this lower bound for the full propositional affine linear logic, proving its Towercompleteness. We also show that provability in propositional contractive linear logic is Ackermanncomplete. 
14:30  Regular Combinators for String Transformations SPEAKER: Rajeev Alur 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 twoway finitestate transducers, (oneway) cost register automata, and MSOdefinable graph transformations. In this paper, we give an algebraic and machineindependent 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 noncommutative monoids, which is of particular interest for capturing regular stringtostring transformations for document processing. We prove that the following additional combinators suffice for constructing all regular functions: (1) the leftadditive 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. 
15:00  On Periodically Iterated Morphisms SPEAKER: unknown 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 onesided 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 firstorder 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. 
15:30  FiniteMemory Strategy Synthesis for Robust Multidimensional MeanPayoff Objectives SPEAKER: Yaron Velner ABSTRACT. Twoplayer 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). Meanpayoff expression games are played on a multidimensional weighted graph. An atomic meanpayoff expression objective is the meanpayoff value (the longrun average weight) of a certain dimension, and the class of meanpayoff expressions is the closure of atomic meanpayoff 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 meanpayoff expression objectives. While in general, optimal strategies for these games require infinitememory, in synthesis we are typically interested in the construction of a finitestate system. Hence, we consider games in which player 1 is restricted to finitememory strategies, and our main contribution is as follows. We prove that for meanpayoff expressions, the quantitative analysis problem is computable, and the boolean analysis problem is interreducible with Hilbert's tenth problem over rationals  a fundamental longstanding open problem in computer science and mathematics. 
14:30  A type theory for productive coprogramming via guarded recursion SPEAKER: Rasmus Ejlers Møgelberg 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 typebased 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 toposoftrees model we construct a model of the calculus using a family of presheaf toposes, each of which can be seen as a multidimensional version of the toposoftrees. 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. 
15:00  FormulaeasTypes for an Involutive Negation SPEAKER: Guillaume MunchMaccagnoni ABSTRACT. Negation is not involutive in the λC calculus because it does not distinguish captured stacks from continuations. We show that there is a formulaeastypes correspondence between the involutive negation in proof theory, and a notion of highlevel access to the stacks studied by Felleisen and Clements. 
15:30  EilenbergMacLane Spaces in Homotopy Type Theory SPEAKER: unknown ABSTRACT. Homotopy type theory is an extension of MartinL\"of type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopytheoretic theorems, in a way that is very amenable to computerchecked proofs in proof assistants such as Coq and Agda. In this paper, we give a computerchecked construction of \emph{EilenbergMacLane spaces}. For an abelian group $G$, an EilenbergMacLane 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. 
14:30  Weak well orders and related inductions SPEAKER: Gerhard Jaeger 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 NeumannBernaysGoedel set theory and MorseKelley set theory). Which prooftheoretic 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 prooftheoretically 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. 
15:15  Automating inductive proof SPEAKER: Alan Bundy ABSTRACT. We discuss the automation of inductive proof. 
16:30  Citations for the TestofTime Award from 1994 SPEAKER: Dexter Kozen 
17:00  The Ackermann Award 2014 SPEAKER: Anuj Dawar 