Selected papers of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)

Editors: Stefan Milius, Joël Ouaknine

This special issue contains revised and extended versions of papers presented at the 32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017), held at Reykjavik University, Island in June 2017. A small number of papers from the proceedings were selected and their authors were invited to submit a full version of their paper to this special issue. Their topics span a range of topics typically represented at LICS: categorical semantics, descriptive complexity theory, and automata theory.

All submissions were refereed according to the usual standards of *Logical Methods in Computer Science*. We are grateful to the authors for their excellent submissions and to the reviewers for their efforts to evaluate and improve these papers. We also thank the program committee members and their subreviewers who reviewed the original conference submissions for their work.

Stefan Milius and Joël Ouaknine
Guest Editors

1. Capturing Polynomial Time using Modular Decomposition

Berit Grußien.

The question of whether there is a logic that captures polynomial time is one of the main open problems in descriptive complexity theory and database theory. In 2010 Grohe showed that fixed point logic with counting captures polynomial time on all classes of graphs with excluded minors. We now consider classes of graphs with excluded induced subgraphs. For such graph classes, an effective graph decomposition, called modular decomposition, was introduced by Gallai in 1976. The graphs that are non-decomposable with respect to modular decomposition are called prime. We present a tool, the Modular Decomposition Theorem, that reduces (definable) canonization of a graph class C to (definable) canonization of the class of prime graphs of C that are colored with binary relations on a linearly ordered set. By an application of the Modular Decomposition Theorem, we show that fixed point logic with counting captures polynomial time on the class of permutation graphs. Within the proof of the Modular Decomposition Theorem, we show that the modular decomposition of a graph is definable in symmetric transitive closure logic with counting. We obtain that the modular decomposition tree is computable in logarithmic space. It follows that cograph recognition and cograph canonization is computable in logarithmic space.

2. Regular Separability of One Counter Automata

Wojciech Czerwiński ; Sławomir Lasota.

The regular separability problem asks, for two given languages, if there exists a regular language including one of them but disjoint from the other. Our main result is decidability, and PSpace-completeness, of the regular separability problem for languages of one counter automata without zero tests (also known as one counter nets). This contrasts with undecidability of the regularity problem for one counter nets, and with undecidability of the regular separability problem for one counter automata, which is our second result.

3. A categorical semantics for causal structure

Aleks Kissinger ; Sander Uijlen.

We present a categorical construction for modelling causal structures within a general class of process theories that include the theory of classical probabilistic processes as well as quantum theory. Unlike prior constructions within categorical quantum mechanics, the objects of this theory encode fine-grained causal relationships between subsystems and give a new method for expressing and deriving consequences for a broad class of causal structures. We show that this framework enables one to define families of processes which are consistent with arbitrary acyclic causal orderings. In particular, one can define one-way signalling (a.k.a. semi-causal) processes, non-signalling processes, and quantum $n$-combs. Furthermore, our framework is general enough to accommodate recently-proposed generalisations of classical and quantum theory where processes only need to have a fixed causal ordering locally, but globally allow indefinite causal ordering. To illustrate this point, we show that certain processes of this kind, such as the quantum switch, the process matrices of Oreshkov, Costa, and Brukner, and a classical three-party example due to Baumeler, Feix, and Wolf are all instances of a certain family of processes we refer to as $\textrm{SOC}_n$ in the appropriate category of higher-order causal processes. After defining these families of causal structures within our framework, we give derivations of their operational behaviour using simple, diagrammatic axioms.