Computer Science Logic 2015
Berlin, 7-10 September 2015
Technische Universität Berlin

Monday, 7 September 2015

9:00 Martin Abadi
Martin Abadi
The Prophecy of Timely Rollback
Show abstract

Techniques for rollback recovery play a central role in ensuring fault-tolerance 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 data-parallel 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 logspace-computable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simply-typed and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higher-order languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode first-order 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
Simone Bova, Barnaby Martin
First-Order 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 first-order sentences on finite abelian groups is fixed-parameter tractable, when parameterized by the size of the sentence. We also prove that model checking monadic second-order sentences on finite abelian groups finitely presented by integer matrices is not fixed-parameter tractable (under standard assumptions in parameterized complexity).

11:30 Anuj Dawar, Pengming Wang
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 polynomial-time solvable optimisation problem, or to an NP-hard 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 fixed-point 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 complexity-theoretic 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 Disjunction-free Intuitionistic Logic
Show abstract

The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary 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 cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.

14:30 Stefan Hetzl, Sebastian Zivota
Stefan Hetzl, Sebastian Zivota
Tree grammars for the elimination of non-prenex 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_1-cuts in classical first-order logic corresponds to computing the language of a particular type of tree grammars. The present paper extends this connection to arbitrary (i.e. non-prenex) cuts without quantifier alternations. The key to treating non-prenex 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:30 Coffee break (Room H 3005)
16:00 Filip Mazowiecki, Cristian Riveros
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 so-called 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 two-way transducers and FO-transductions
Show abstract

Deterministic two-way transducers on finite words have been shown by Engelfriet and Hoogeboom to have the same expressive power as MSO-transductions. We introduce a notion of aperiodicity for these transducers and we show that aperiodic transducers correspond exactly to FO-transductions. This lifts to transducers the classical equivalence for languages between FO-definability, recognition by aperiodic monoids and acceptance by counter-free automata.

17:00 Orna Kupferman, Gal Vardi
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 bad-prefix 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 bad-prefixes and thus do not have finite counterexamples.

We extend the notion of finite counterexamples to non-safety properties. We study counterable languages -- ones that have at least one bad-prefix. 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 bad-prefixes for counterable languages, and (3) develop algorithms for detecting bad-prefixes for counterable languages. We solve the problems for languages given by means of LTL formulas or nondeterministic Büchi automata. In particular, our EXPSPACE-completeness proof for the problem of deciding whether a given LTL formula is counterable, and hence also for deciding whether it is liveness, settles a long-standing open problem.

We also make finite counterexamples more relevant and helpful by introducing two variants of the traditional definition of bad-prefixes. 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
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, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary 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 EXPSPACE-hardness 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)