Monday, 7 September 2015
Show all abstracts Proceedings Close all abstracts
9:00  Martin Abadi 
The Prophecy of Timely Rollback
Show abstract Techniques for rollback recovery play a central role in ensuring faulttolerance in many distributed systems. This talk addresses the formal specification and analysis of those techniques. In particular, we will discuss the relevance of prophecy variables (auxiliary program variables whose values are defined in terms of current program state and future behavior) to reasoning about systems with undo operations. We will then focus on a model for dataparallel computation with a notion of virtual time. In this model, rollbacks allow the selective undo of work at particular virtual times. A refinement theorem ensures the consistency of rollbacks. This talk is largely based on joint work with Michael Isard. 

10:00  Damiano Mazza 
Simple Parsimonious Types and Logarithmic Space
Show abstract We present a functional characterization of deterministic logspacecomputable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simplytyped and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higherorder languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode firstorder logic with deterministic closure), whereas soundness is established by executing terms on a token machine (using the geometry of interaction). 

10:30  Coffee break (Room H 3005)  
11:00  Simone Bova, Barnaby Martin 
FirstOrder Queries on Finite Abelian Groups
Show abstract We study the computational problem of checking whether a logical sentence is true in a finite abelian group. We prove that model checking firstorder sentences on finite abelian groups is fixedparameter tractable, when parameterized by the size of the sentence. We also prove that model checking monadic secondorder sentences on finite abelian groups finitely presented by integer matrices is not fixedparameter tractable (under standard assumptions in parameterized complexity). 

11:30  Anuj Dawar, Pengming Wang 
A Definability Dichotomy for Finite Valued CSPs
Show abstract Finite valued constraint satisfaction problems are a formalism for describing many natural optimisation problems, where constraints on the values that variables can take come with rational weights and the aim is to find an assignment of minimal cost. Thapper and Živný have recently established a complexity dichotomy for valued constraint languages. They show that each such languages either gives rise to a polynomialtime solvable optimisation problem, or to an NPhard one, and establish a criterion to distinguish the two cases. We refine the dichotomy by showing that all optimisation problems in the first class are definable in fixedpoint language with counting, while all languages in the second class are not definable, even in infinitary logic with counting. Our definability dichotomy is not conditional on any complexitytheoretic assumption. 

12:00  Sjoerd Cranen, Bas Luttik, Tim Willemse 
Evidence for fixpoint logic
Show abstract For many modal logics, dedicated model checkers offer diagnostics (e.g., counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking. 

12:30  Lunch break  
14:00  Matthias Baaz, Christian Fermüller 
Elementary Elimination of Prenex Cuts in Disjunctionfree Intuitionistic Logic
Show abstract The size of shortest cutfree proofs of firstorder formulas in intuitionistic sequent calculus is known to be nonelementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cutfree proofs for disjunctionfree intuitionistic logic for the case where the cutformulas of the original proof are prenex. Moreover, we establish nonelementary lower bounds for classical disjunctionfree proofs with prenex cutformulas and intuitionistic disjunctionfree proofs with nonprenex cutformulas. 

14:30  Stefan Hetzl, Sebastian Zivota 
Tree grammars for the elimination of nonprenex cuts
Show abstract Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs with prenex Pi_1cuts in classical firstorder logic corresponds to computing the language of a particular type of tree grammars. The present paper extends this connection to arbitrary (i.e. nonprenex) cuts without quantifier alternations. The key to treating nonprenex cuts lies in using a new class of tree grammars, constraint grammars, which describe the relationship of the applicability of its productions by a propositional formula. 

15:00  Aleksy Schubert, Wil Dekkers, Henk Barendregt 
Automata Theoretic Account of Proof Search
Show abstract Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automatatheoretic model for inhabitant search, which can be viewed as proof search by the CurryHoward isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata. 

15:30  Coffee break (Room H 3005)  
16:00  Filip Mazowiecki, Cristian Riveros 
Maximal partition logic: towards a logical characterization of copyless cost register automata
Show abstract It is highly desirable for a computational model to have a logic characterization like in the seminal work from Buchi that connects MSO with finite automata. For example, weighted automata are the quantitative extension of finite automata for computing functions over words and they can be naturally characterized by a subframent of weighted logic introduced by Droste and Gastin. Recently, cost register automata (CRA) were introduced by Alur et all as an alternative model for weighted automata. In hope of finding decidable subclasses of weighted automata, they proposed to restrict their model with the socalled copyless restriction. Unfortunately, copyless CRA do not enjoy good closure properties and, therefore, a logical characterization of this class seems to be unlikely. In this paper, we introduce a new logic called maximal partition logic (MPL) for studying the expressiveness of copyless CRA. In contrast from the previous approaches (i.e. weighted logics), MPL is based on a new set of "regular" quantifiers that partition a word into maximal subwords, compute the output of a subformula over each subword separately, and then aggregate these outputs with a semiring operation. We study the expressiveness of MPL and compare it with weighted logics. Furthermore, we show that MPL is equally expressive to a natural subclass of copyless CRA. This shows the first logical characterization of copyless CRA and it gives a better understanding of the copyless restriction in weighted automata. 

16:30  Olivier Carton, Luc Dartois 
Aperiodic twoway transducers and FOtransductions
Show abstract Deterministic twoway transducers on finite words have been shown by Engelfriet and Hoogeboom to have the same expressive power as MSOtransductions. We introduce a notion of aperiodicity for these transducers and we show that aperiodic transducers correspond exactly to FOtransductions. This lifts to transducers the classical equivalence for languages between FOdefinability, recognition by aperiodic monoids and acceptance by counterfree automata. 

17:00  Orna Kupferman, Gal Vardi 
On Relative and Probabilistic Finite Counterability
Show abstract A counterexample to the satisfaction of a linear property $\psi$ in a system $\S$ is an infinite computation of $\S$ that violates $\psi$. Counterexamples are of great help in detecting design errors and in modeling methodologies such as CEGAR. When $\psi$ is a safety property, a counterexample to its satisfaction need not be infinite. Rather, it is a badprefix for $\psi$: a finite word all whose extensions violate $\psi$. The existence of finite counterexamples is very helpful in practice. Liveness properties do not have badprefixes and thus do not have finite counterexamples. We extend the notion of finite counterexamples to nonsafety properties. We study counterable languages  ones that have at least one badprefix. Thus, a language is counterable iff it is not liveness. Three natural problems arise: (1) Given a language, decide whether it is counterable, (2) study the length of minimal badprefixes for counterable languages, and (3) develop algorithms for detecting badprefixes for counterable languages. We solve the problems for languages given by means of LTL formulas or nondeterministic Büchi automata. In particular, our EXPSPACEcompleteness proof for the problem of deciding whether a given LTL formula is counterable, and hence also for deciding whether it is liveness, settles a longstanding open problem. We also make finite counterexamples more relevant and helpful by introducing two variants of the traditional definition of badprefixes. The first adds a probabilistic component to the definition. There, a prefix is bad if almost all its extensions violate the property. The second makes it relative to the system. There, a prefix is bad if all its extensions in the system violate the property. We also study the combination of the probabilistic and relative variants. Our framework suggests new variants also of safety and liveness languages. We solve the above three problems for the different variants. Interestingly, the probabilistic variant not only increases the chances to return finite counterexamples, but also makes the solution of the three problems exponentially easier. 

17:30  Alberto Molinari, Angelo Montanari, Adriano Peron 
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives
Show abstract Model checking is commonly recognized as one of the most effective tool in system verification. While it has been systematically investigated in the context of classical, pointbased temporal logics, it is still largely unexplored in the interval logic setting. Recently, a nonelementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACEhardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones. 

19:00  Welcome Reception (Room H 3005, same as the coffee breaks) 