Logic in Computer Science (cs.LO)

• While quantum computers are expected to yield considerable advantages over classical devices, the precise features of quantum theory enabling these advantages remain unclear. Contextuality---the denial of a notion of classical physical reality---has emerged as a promising hypothesis. Magic states are quantum resources critical for practically achieving universal quantum computation. They exhibit the standard form of contextuality that is known to enable probabilistic advantages in a variety of computational and communicational tasks. Strong contextuality is an extremal form of contextuality describing systems that exhibit logically paradoxical behaviour. Here, we consider special magic states that deterministically enable quantum computation. After introducing number-theoretic techniques for constructing exotic quantum paradoxes, we present large classes of strongly contextual magic states that enable deterministic implementation of gates from the Clifford hierarchy. These surprising discoveries bolster a refinement of the resource theory of contextuality that emphasises the computational power of logical paradoxes.
• Quantum computing is moving rapidly to the point of deployment of technology. Functional quantum devices will require the ability to correct error in order to be scalable and effective. A leading choice of error correction, in particular for modular or distributed architectures, is the surface code with logical two-qubit operations realised via "lattice surgery". These operations consist of "merges" and "splits" acting non-unitarily on the logical states and are not easily captured by standard circuit notation. This raises the question of how best to reason about lattice surgery in order efficiently to use quantum states and operations in architectures with complex resource management issues. In this paper we demonstrate that the operations of the ZX calculus, a form of quantum diagrammatic reasoning designed using category theory, match exactly the operations of lattice surgery. Red and green "spider" nodes match rough and smooth merges and splits, and follow the axioms of a dagger special associative Frobenius algebra. Some lattice surgery operations can require non-trivial correction operations, which are captured natively in the use of the ZX calculus in the form of ensembles of diagrams. We give a first taste of the power of the calculus as a language for surgery by considering two operations (magic state use and producing a CNOT) and show how ZX diagram re-write rules give lattice surgery procedures for these operations that are novel, efficient, and highly configurable.
• An important class of contextuality arguments in quantum foundations are the All-versus-Nothing (AvN) proofs, generalising a construction originally due to Mermin. We present a general formulation of All-versus-Nothing arguments, and a complete characterisation of all such arguments which arise from stabiliser states. We show that every AvN argument for an n-qubit stabiliser state can be reduced to an AvN proof for a three-qubit state which is local Clifford-equivalent to the tripartite GHZ state. This is achieved through a combinatorial characterisation of AvN arguments, the AvN triple Theorem, whose proof makes use of the theory of graph states. This result enables the development of a computational method to generate all the AvN arguments in $\mathbb{Z}_2$ on n-qubit stabiliser states. We also present new insights into the stabiliser formalism and its connections with logic.
• The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics. The language is sound and complete: one can transform a stabilizer ZX-diagram into another one if and only if these two diagrams represent the same quantum evolution or quantum state. We show that the stabilizer ZX-calculus can be simplified, removing unnecessary equations while keeping only the essential axioms which potentially capture fundamental structures of quantum mechanics. We thus give a significantly smaller set of axioms and prove that meta-rules like only the topology matters', colour symmetry' and `upside-down symmetry', which were considered as axioms in previous versions of the language, can in fact be derived. In particular, we show that most of the remaining rules of the language are necessary, however leaving as an open question the necessity of two rules. These include, surprisingly, the bialgebra rule, which is an axiomatisation of complementarity, the cornerstone of the ZX-calculus. Furthermore, we show that a weaker ambient category -- a braided autonomous category instead of the usual compact closed category -- is sufficient to recover the topology meta rule.
• We give a finite presentation by generators and relations of unitary operators expressible over the $\{\mathrm{CNOT}, T, X\}$ gate set, also known as $\mathrm{CNOT}$-dihedral operators. To this end, we introduce a notion of normal form for $\mathrm{CNOT}$-dihedral circuits and prove that every $\mathrm{CNOT}$-dihedral operator admits a unique normal form. Moreover, we show that in the presence of certain structural rules only finitely many circuit identities are required to reduce an arbitrary $\mathrm{CNOT}$-dihedral circuit to its normal form. By appropriately restricting our relations, we obtain a finite presentation of unitary operators expressible over the $\{\mathrm{CNOT}, T, X\}$ gate set as a corollary.
• Jul 11 2017 cs.LO quant-ph arXiv:1707.02348v1
We exhibit a complete set of identities for CNOT, the symmetric monoidal category generated by the controlled-not gate, the swap gate, and the computational ancillae. We prove that CNOT is a discrete inverse category. Moreover, we prove that CNOT is equivalent to the category of partial isomorphisms of finitely-generated non-empty commutative torsors of characteristic 2. This is equivalently the category of partial isomorphisms of affine maps between finite-dimensional $\mathbb{Z}_2$ vector spaces.
• Schaefer introduced a framework for generalized satisfiability problems on the Boolean domain and characterized the computational complexity of such problems. We investigate an algebraization of Schaefer's framework in which the Fourier transform is used to represent constraints by multilinear polynomials in a unique way. The polynomial representation of constraints gives rise to a relaxation of the notion of satisfiability in which the values to variables are linear operators on some Hilbert space. For the case of constraints given by a system of linear equations over the two-element field, this relaxation has received considerable attention in the foundations of quantum mechanics, where such constructions as the Mermin-Peres magic square show that there are systems that have no solutions in the Boolean domain, but have solutions via operator assignments on some finite-dimensional Hilbert space. We obtain a complete characterization of the classes of Boolean relations for which there is a gap between satisfiability in the Boolean domain and the relaxation of satisfiability via operator assignments. To establish our main result, we adapt the notion of primitive-positive definability (pp-definability) to our setting, a notion that has been used extensively in the study of constraint satisfaction problems. Here, we show that pp-definability gives rise to gadget reductions that preserve satisfiability gaps. We also present several additional applications of this method. In particular and perhaps surprisingly, we show that the relaxed notion of pp-definability in which the quantified variables are allowed to range over operator assignments gives no additional expressive power in defining Boolean relations.
• In this paper we present a Quantomatic case study, verifying the basic properties of the Smallest Interesting Colour Code error correcting code.
• This volume contains the proceedings of the 13th International Conference on Quantum Physics and Logic (QPL 2016), which was held June 6-10, 2016 at the University of Strathclyde. QPL is a conference that brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behaviour in general.
• The ZX-Calculus is a powerful diagrammatic language devoted to represent complex quantum evolutions. But the advantages of quantum computing still exist when working with rebits, and evolutions with real coefficients. Some models explicitly use rebits, but the ZX-Calculus can not handle these evolutions as it is. Hence, we define an alternative language solely dealing with real matrices, with a new set of rules. We show that three of its non-trivial rules are not derivable from the others and we prove that the language is complete for the $\pi$/2-fragment. We define a generalisation of the Hadamard node, and exhibit two interpretations from and to the ZX-Calculus, showing the consistency between the two languages.
• This paper is a tutorial for newcomers to the field of automated verification tools, though we assume the reader to be relatively familiar with Hoare-style verification. In this paper, besides introducing the most basic features of the language and verifier Dafny, we place special emphasis on how to use Dafny as an assistant in the development of verified programs. Our main aim is to encourage the software engineering community to make the move towards using formal verification tools.
• The development and deployment of Autonomous Vehicles (AVs) on our roads is not only realistic in the near future but can also bring significant benefits. In particular, it can potentially solve several problems relating to vehicles and traffic, for instance: (i) possible reduction of traffic congestion, with the consequence of improved fuel economy and reduced driver inactivity; (ii) possible reduction in the number of accidents, assuming that an AV can minimise the human errors that often cause traffic accidents; and (iii) increased ease of parking, especially when one considers the potential for shared AVs. In order to deploy an AV there are significant steps that must be completed in terms of hardware and software. As expected, software components play a key role in the complex AV system and so, at least for safety, we should assess the correctness of these components. In this paper, we are concerned with the high-level software component(s) responsible for the decisions in an AV. We intend to model an AV capable of navigation; obstacle avoidance; obstacle selection (when a crash is unavoidable) and vehicle recovery, etc, using a rational agent. To achieve this, we have established the following stages. First, the agent plans and actions have been implemented within the Gwendolen agent programming language. Second, we have built a simulated automotive environment in the Java language. Third, we have formally specified some of the required agent properties through LTL formulae, which are then formally verified with the AJPF verification tool. Finally, within the MCAPL framework (which comprises all the tools used in previous stages) we have obtained formal verification of our AV agent in terms of its specific behaviours. For example, the agent plans responsible for selecting an obstacle with low potential damage, instead of a higher damage obstacle (when possible) can be formally verified within MCAPL. We must emphasise that the major goal (of our present approach) lies in the formal verification of agent plans, rather than evaluating real-world applications. For this reason we utilised a simple matrix representation concerning the environment used by our agent.
• Theoretical computer science discusses foundational issues about computations. It asks and answers questions such as "What is a computation?", "What is computable?", "What is efficiently computable?","What is information?", "What is random?", "What is an algorithm?", etc. We will present many of the major themes and theorems with the basic language of category theory. Surprisingly, many interesting theorems and concepts of theoretical computer science are easy consequences of functoriality and composition when you look at the right categories and functors connecting them.
• In this paper, we develop a game-theoretic account of concurrent separation logic. To every execution trace of the Code confronted to the Environment, we associate a specification game where Eve plays for the Code, and Adam for the Environment. The purpose of Eve and Adam is to decompose every intermediate machine state of the execution trace into three pieces: one piece for the Code, one piece for the Environment, and one piece for the available shared resources. We establish the soundness of concurrent separation logic by interpreting every derivation tree of the logic as a winning strategy of this specification game.
• Oct 03 2017 cs.LO arXiv:1710.00787v1
We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski's formal geometry. We used proofs as close as possible to those given by Euclid, but filling Euclid's gaps and correcting errors. Euclid Book I has 48 propositions, we proved 213 theorems. The extras were partly "Book Zero", preliminaries of a very fundamental nature, partly propositions that Euclid omitted but were used implicitly, partly advanced theorems that we found necessary to fill Euclid's gaps, and partly just variants of Euclid's propositions. We wrote these proofs in a simple fragment of first-order logic corresponding to Euclid's logic, debugged them using a custom software tool, and then checked them in the well-known and trusted proof checkers HOL Light and Coq.
• Sep 27 2017 cs.FL cs.GT cs.LO arXiv:1709.08991v1
In this paper, we study the problem of deciding the winner of reachability switching games. These games provide deterministic analogues of Markovian systems. We study zero-, one-, and two-player variants of these games. We show that the zero-player case is NL-hard, the one-player case is NP-complete, and that the two-player case is PSPACE-hard and in EXPTIME. In the one- and two-player cases, the problem of determining the winner of a switching game turns out to be much harder than the problem of determining the winner of a Markovian game. We also study the structure of winning strategies in these games, and in particular we show that both players in a two-player reachability switching game require exponential memory.
• Sep 08 2017 cs.LO cs.CR arXiv:1709.02105v1
A social network service is a platform to build social relations among people sharing similar interests and activities. The underlying structure of a social networks service is the social graph, where nodes represent users and the arcs represent the users' social links and other kind of connections. One important concern in social networks is privacy: what others are (not) allowed to know about us. The "logic of knowledge" (epistemic logic) is thus a good formalism to define, and reason about, privacy policies. In this paper we consider the problem of verifying knowledge properties over social network models (SNMs), that is social graphs enriched with knowledge bases containing the information that the users know. More concretely, our contributions are: i) We prove that the model checking problem for epistemic properties over SNMs is decidable; ii) We prove that a number of properties of knowledge that are sound w.r.t. Kripke models are also sound w.r.t. SNMs; iii) We give a satisfaction-preserving encoding of SNMs into canonical Kripke models, and we also characterise which Kripke models may be translated into SNMs; iv) We show that, for SNMs, the model checking problem is cheaper than the one based on standard Kripke models. Finally, we have developed a proof-of-concept implementation of the model-checking algorithm for SNMs.
• In this paper we introduce \em global and local announcement logic (GLAL), a dynamic epistemic logic with two distinct announcement operators -- $[\phi]^+_A$ and $[\phi]^-_A$ indexed to a subset $A$ of the set $Ag$ of all agents -- for global and local announcements respectively. The boundary case $[\phi]^+_{Ag}$ corresponds to the public announcement of $\phi$, as known from the literature. Unlike standard public announcements, which are \em model transformers, the global and local announcements are \em pointed model transformers. In particular, the update induced by the announcement may be different in different states of the model. Therefore, the resulting computations are trees of models, rather than the typical sequences. A consequence of our semantics is that modally bisimilar states may be distinguished in our logic. Then, we provide a stronger notion of bisimilarity and we show that it preserves modal equivalence in GLAL. Additionally, we show that GLAL is strictly more expressive than public announcement logic with common knowledge. We prove a wide range of validities for GLAL involving the interaction between dynamics and knowledge, and show that the satisfiability problem for GLAL is decidable. We illustrate the formal machinery by means of detailed epistemic scenarios.
• The recent increase of interest in the graph invariant called tree-depth and in its applications in algorithms and logic on graphs led to a natural question: is there an analogously useful "depth" notion also for dense graphs (say; one which is stable under graph complementation)? To this end, in a 2012 conference paper, a new notion of shrub-depth has been introduced, such that it is related to the established notion of clique-width in a similar way as tree-depth is related to tree-width. Since then shrub-depth has been successfully used in several research papers. Here we provide an in-depth review of the definition and basic properties of shrub-depth, and we focus on its logical aspects which turned out to be most useful. In particular, we use shrub-depth to give a characterization of the lower ${\omega}$ levels of the MSO1 transduction hierarchy of simple graphs.
• String diagrams provide a convenient graphical framework which may be used for equational reasoning about morphisms of monoidal categories. However, unlike term rewriting, rewriting string diagrams results in shorter equational proofs, because the string diagrammatic representation allows us to formally establish equalities modulo any rewrite steps which follow from the monoidal structure. Manipulating string diagrams by hand is a time-consuming and error-prone process, especially for large string diagrams. This can be ameliorated by using software proof assistants, such as Quantomatic. However, reasoning about concrete string diagrams may be limiting and in some scenarios it is necessary to reason about entire (infinite) families of string diagrams. When doing so, we face the same problems as for manipulating concrete string diagrams, but in addition, we risk making further mistakes if we are not precise enough about the way we represent (infinite) families of string diagrams. The primary goal of this thesis is to design a mathematical framework for equational reasoning about infinite families of string diagrams which is amenable to computer automation. We will be working with context-free families of string diagrams and we will represent them using context-free graph grammars. We will model equations between infinite families of diagrams using rewrite rules between context-free grammars. Our framework represents equational reasoning about concrete string diagrams and context-free families of string diagrams using double-pushout rewriting on graphs and context-free graph grammars respectively. We will prove that our representation is sound by showing that it respects the concrete semantics of string diagrammatic reasoning and we will show that our framework is appropriate for software implementation by proving important decidability properties.
• Apr 27 2017 cs.FL cs.LO arXiv:1704.08055v1
Automata learning has been successfully applied in the verification of hardware and software. The size of the automaton model learned is a bottleneck for scalability and hence optimizations that enable learning of compact representations are important. In this paper, we continue the development of a general framework for automata learning based on category theory and develop a class of optimizations and an accompanying correctness proof for learning algorithms. The new algorithm is parametric on a monad, which provides a rich algebraic structure to capture non-determinism and other side-effects. These side-effects are used to learn more compact automaton models and the abstract categorical approach enables us to capture several possible optimizations under the same (p)roof.
• This paper presents a symmetric monoidal and compact closed bicategory that categorifies the zx-calculus developed by Coecke and Duncan. The $1$-cells in this bicategory are certain graph morphisms that correspond to the string diagrams of the zx-calculus, while the $2$-cells are rewrite rules.
• Partially Observable Markov Decision Process (POMDP) is widely used to model probabilistic behavior for complex systems. Compared with MDPs, POMDP models a system more accurate but solving a POMDP generally takes exponential time in the size of its state space. This makes the formal verification and synthesis problems much more challenging for POMDPs, especially when multiple system components are involved. As a promising technique to reduce the verification complexity, the abstraction method tries to find an abstract system with a smaller state space but preserves enough properties for the verification purpose. While abstraction based verification has been explored extensively for MDPs, in this paper, we present the first result of POMDP abstraction and its refinement techniques. The main idea follows the counterexample-guided abstraction refinement (CEGAR) framework. Starting with a coarse guess for the POMDP abstraction, we iteratively use counterexamples from formal verification to refine the abstraction until the abstract system can be used to infer the verification result for the original POMDP. Our main contributions have two folds: 1) we propose a novel abstract system model for POMDP and a new simulation relation to capture the partial observability then prove the preservation on a fragment of Probabilistic Computation Tree Logic (PCTL); 2) to find a proper abstract system that can prove or disprove the satisfaction relation on the concrete POMDP, we develop a novel refinement algorithm. Our work leads to a sound and complete CEGAR framework for POMDP.
• We present a categorical construction for modelling both definite and indefinite causal structures within a general class of process theories that include classical probability theory and quantum theory. Unlike prior constructions within categorical quantum mechanics, the objects of this theory encode finegrained causal relationships between subsystems and give a new method for expressing and deriving consequences for a broad class of causal structures. To illustrate this point, we show that this framework admits processes with definite causal structures, namely one-way signalling processes, non-signalling processes, and quantum n-combs, as well as processes with indefinite causal structure, such as the quantum switch and the process matrices of Oreshkov, Costa, and Brukner. We furthermore give derivations of their operational behaviour using simple, diagrammatic axioms.
• Jan 13 2017 cs.PL cs.LO arXiv:1701.03320v1
This paper is a tutorial introducing the underlying technology and the use of the tool Liquid Haskell, a type-checker for the functional language Haskell that can help programmers to verify non-trivial properties of their programs with a low effort. The first sections introduce the technology of Liquid Types by explaining its principles and summarizing how its type inference algorithm manages to prove properties. The remaining sections present a selection of Haskell examples and show the kind of properties that can be proved with the system.
• Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed. Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.
• Jan 02 2017 cs.LO arXiv:1612.09514v2
In the final chain of the countable powerset functor, we show that the set at index $\omega_1$, regarded as a transition system, is not strongly extensional because it contains a "ghost" element that has no successor even though its component at index 1 is inhabited. The method, adapted from a construction of Forti and Honsell, also gives ghosts at larger ordinals in the final chain of other subfunctors of the powerset functor. This leads to a precise description of which sets in these final chains are strongly extensional.
• In this article, we will show that uncomputability is a relative property not only of oracle Turing machines, but also of subrecursive classes. We will define the concept of a Turing submachine, and a recursive relative version for the Busy Beaver function which we will call Busy Beaver Plus function. Therefore, we will prove that the computable Busy Beaver Plus function defined on any Turing submachine is not computable by any program running on this submachine. We will thereby demonstrate the existence of a "paradox" of computability a la Skolem: a function is computable when "seen from the outside" the subsystem, but uncomputable when "seen from within" the same subsystem. Finally, we will raise the possibility of defining universal submachines, and a hierarchy of negative Turing degrees.
• MEMICS provides a forum for doctoral students interested in applications of mathematical and engineering methods in computer science. Besides a rich technical programme (including invited talks, regular papers, and presentations), MEMICS also offers friendly social activities and exciting opportunities for meeting like-minded people. MEMICS submissions traditionally cover all areas of computer science (such as parallel and distributed computing, computer networks, modern hardware and its design, non-traditional computing architectures, information systems and databases, multimedia and graphics, verification and testing, computer security, as well as all related areas of theoretical computer science).
• After substantial progress over the last 15 years, the "algebraic CSP-dichotomy conjecture" reduces to the following: every local constraint satisfaction problem (CSP) associated with a finite idempotent algebra is tractable if and only if the algebra has a Taylor term operation. Despite the tremendous achievements in this area, there remain examples of small algebras with just a single binary operation whose CSP resists classification as either tractable or NP-complete using known methods. In this paper we present some new methods for approaching this problem, with particular focus on those techniques that help us attack the class of finite algebras known as "commutative idempotent binars" (CIBs). We demonstrate the utility of these methods by using them to prove that every CIB of cardinality at most 4 yields a tractable CSP.
• Nov 03 2016 cs.LO arXiv:1611.00580v2
Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automatically whether the executions of an implementation of a data structure are causally consistent. We consider two problems: (1) checking whether one single execution is causally consistent, which is relevant for developing testing and bug finding algorithms, and (2) verifying whether all the executions of an implementation are causally consistent. We show that the first problem is NP-complete. This holds even for the read-write memory abstraction, which is a building block of many modern distributed systems. Indeed, such systems often store data in key-value stores, which are instances of the read-write memory abstraction. Moreover, we prove that, surprisingly, the second problem is undecidable, and again this holds even for the read-write memory abstraction. However, we show that for the read-write memory abstraction, these negative results can be circumvented if the implementations are data independent, i.e., their behaviors do not depend on the data values that are written or read at each moment, which is a realistic assumption.
• Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to fully replace nondeterminism with probability distributions and no stochastic structure is desired/allowed. Here we propose a general solution based on a recursive, static decomposition of (finite, occurrence) nets in loci of decision, called structural branching cells (s-cells). Each s-cell exposes a set of alternatives, called transactions, that can be equipped with a general probabilistic distribution. The solution is formalised as a transformation from a given Petri net to another net whose transitions are the transactions of the s-cells and whose places are the places of the original net, with some auxiliary structure for bookkeeping. The resulting net is confusion-free, namely if a transition is enabled, then all its conflicting alternatives are also enabled. Thus sets of conflicting alternatives can be equipped with probability distributions, while nonintersecting alternatives are purely concurrent and do not introduce any nondeterminism: they are Church-Rosser and their probability distributions are independent. The validity of the construction is witnessed by a tight correspondence result with the recent approach by Abbes and Benveniste (AB) based on recursively stopped configurations in event structures. Some advantages of our approach over AB's are that: i) s-cells are defined statically and locally in a compositional way, whereas AB's branching cells are defined dynamically and globally; ii) their recursively stopped configurations correspond to possible executions, but the existing concurrency is not made explicit. Instead, our resulting nets are equipped with an original concurrency structure exhibiting a so-called complete concurrency property.
• Oct 12 2017 cs.LO arXiv:1710.03979v1
The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which allows to describe atomic components as symbolic transition systems or QLTL formulas, and composite components formed using three primitive composition operators: serial, parallel, and feedback. The semantics of the language is given in terms of monotonic property transformers, an extension to reactive systems of monotonic predicate transformers which have been used to give compositional semantics to sequential programs. RCRS allows to specify both safety and liveness properties. It also allows to model input-output systems which are both non-deterministic and non-input-receptive (i.e., which may reject some inputs at some points in time), and can thus be seen as a behavioral type system. RCRS provides a set of techniques for symbolic computer-aided reasoning, including compositional static analysis and verification. RCRS comes with an open-source implementation built on top of the Isabelle theorem prover.
• A number of high-level languages and libraries have been proposed that offer novel and simple to use abstractions for concurrent, asynchronous, and distributed programming. The execution models that realise them, however, often change over time---whether to improve performance, or to extend them to new language features---potentially affecting behavioural and safety properties of existing programs. This is exemplified by SCOOP, a message-passing approach to concurrent object-oriented programming that has seen multiple changes proposed and implemented, with demonstrable consequences for an idiomatic usage of its core abstraction. We propose a semantics comparison workbench for SCOOP with fully and semi-automatic tools for analysing and comparing the state spaces of programs with respect to different execution models or semantics. We demonstrate its use in checking the consistency of properties across semantics by applying it to a set of representative programs, and highlighting a deadlock-related discrepancy between the principal execution models of SCOOP. Furthermore, we demonstrate the extensibility of the workbench by generalising the formalisation of an execution model to support recently proposed extensions for distributed programming. Our workbench is based on a modular and parameterisable graph transformation semantics implemented in the GROOVE tool. We discuss how graph transformations are leveraged to atomically model intricate language abstractions, how the visual yet algebraic nature of the model can be used to ascertain soundness, and highlight how the approach could be applied to similar languages.
• Learning from expert demonstrations has received a lot of attention in artificial intelligence and machine learning. The goal is to infer the underlying reward function that an agent is optimizing given a set of observations of the agent's behavior over time in a variety of circumstances, the system state trajectories, and a plant model specifying the evolution of the system state for different agent's actions. The system is often modeled as a Markov decision process, that is, the next state depends only on the current state and agent's action, and the the agent's choice of action depends only on the current state. While the former is a Markovian assumption on the evolution of system state, the later assumes that the target reward function is itself Markovian. In this work, we explore learning a class of non-Markovian reward functions, known in the formal methods literature as specifications. These specifications offer better composition, transferability, and interpretability. We then show that inferring the specification can be done efficiently without unrolling the transition system. We demonstrate on a 2-d grid world example.
• The paper reports on some results concerning Aqvist's dyadic logic known as system G, which is one of the most influential logics for reasoning with dyadic obligations ("it ought to be the case that ... if it is the case that ..."). Although this logic has been known in the literature for a while, many of its properties still await in-depth consideration. In this short paper we show: that any formula in system G including nested modal operators is equivalent to some formula with no nesting; that the universal modality introduced by Aqvist in the first presentation of the system is definable in terms of the deontic modality.
• In this position paper we discuss three main shortcomings of existing approaches to counterfactual causality from the computer science perspective, and sketch lines of work to try and overcome these issues: (1) causality definitions should be driven by a set of precisely specified requirements rather than specific examples; (2) causality frameworks should support system dynamics; (3) causality analysis should have a well-understood behavior in presence of abstraction.
• Oct 11 2017 cs.LO cs.PL arXiv:1710.03391v1
Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of model checking algorithms that capture the causal relationships in a special data structure called concurrent traces. Concurrent traces identify key events in an execution history and link them through their cause-effect relationships. The model checker builds a tableau of concurrent traces, where the case splits represent different causal explanations of a hypothetical error. Causality-based model checking has been implemented in the ARCTOR tool, and applied to previously intractable multi-threaded benchmarks.
• One of the key challenges when looking for the causes of a complex event is to determine the causal status of factors that are neither individually necessary nor individually sufficient to produce that event. In order to reason about how such factors should be taken into account, we need a vocabulary to distinguish different cases. In philosophy, the concept of overdetermination and the concept of preemption serve an important purpose in this regard, although their exact meaning tends to remain elusive. In this paper, I provide theory-neutral definitions of these concepts using structural equations in the Halpern-Pearl tradition. While my definitions do not presuppose any particular causal theory, they take such a theory as a variable parameter. This enables us to specify formal constraints on theories of causality, in terms of a pre-theoretic understanding of what preemption and overdetermination actually mean. I demonstrate the usefulness of this by presenting and arguing for what I call the principle of presumption. Roughly speaking, this principle states that a possible cause can only be regarded as having been preempted if there is independent evidence to support such an inference. I conclude by showing that the principle of presumption is violated by the two main theories of causality formulated in the Halpern-Pearl tradition. The paper concludes by defining the class of empirical causal theories, characterised in terms of a fixed-point of counterfactual reasoning about difference-making. It is argued that theories of actual causality ought to be empirical.
• This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an instantiation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support for program verification. In rely/guarantee concurrency, programs are specified to guarantee certain behaviours until assumptions about the behaviour of their environment are violated. When assumptions are violated, program behaviour is unconstrained (aborting), and guarantees need no longer hold. To support these guarantees a second synchronous operator, weak conjunction, was introduced: both processes in a weak conjunction must agree to take each atomic step, unless one aborts in which case the whole aborts. In developing the laws for parallel and weak conjunction we found many properties were shared by the operators and that the proofs of many laws were essentially the same. This insight led to the idea of generalising synchronisation to an abstract operator with only the axioms that are shared by the parallel and weak conjunction operator, so that those two operators can be viewed as instantiations of the abstract synchronisation operator. The main differences between parallel and weak conjunction are how they combine individual atomic steps; that is left open in the axioms for the abstract operator.
• We study the problem of formal verification of Binarized Neural Networks (BNN), which have recently been proposed as a power-efficient alternative to more traditional learning networks. More precisely, given a trained BNN and a relation between possible inputs and outputs of this BNN, we develop verification procedures for establishing that the BNN indeed meets this specification for all possible inputs. For solving the verification problem of BNNs we build on well-known methods for hardware verification.The BNN verification problem is first encoded as a combinational miter. In a second step this miter is then transformed into a corresponding propositional satisfiability (SAT) problem. The main contributions of this paper are a number of essential optimizations for making this approach to BNN verification scalable. First, we provide a transformation on fully conntected BNNs for reducing the order of the number of bitwise operations in each layer of the BNN from quadratic to linear. Second, we are identifying redundant computations in a BNN based on \em optimal factoring techniques, and we provide transformations on BNNs for avoiding these multiple computations. We prove that the problem of optimal factoring is NP-hard, and we design efficient search procedures for generating approximate solutions of the optimal factoring problem. Third, we design a compositional verification procedure for analyzing each layer of a BNN separately, and for iteratively combining and refining local verification results. We experimentally demonstrate the scalability of our verification techniques to moderately-sized BNNs for embedded applications with thousands of neurons and inputs.
• The second international CREST workshop continued the focus of the first CREST workshop: addressing approaches to causal reasoning in engineering complex embedded and safety-critical systems. Relevant approaches to causal reasoning have been (usually independently) proposed by a variety of communities: AI, concurrency, model-based diagnosis, software engineering, security engineering, and formal methods. The goal of CREST is to bring together researchers and practitioners from these communities to exchange ideas, especially between communities, in order to advance the science of determining root cause(s) for failures of critical systems. The growing complexity of failures such as power grid blackouts, airplane crashes, security and privacy violations, and malfunctioning medical devices or automotive systems makes the goals of CREST more relevant than ever before.
• Oct 09 2017 cs.LO arXiv:1710.02198v1
This paper reports on the QBF solver QFUN that has won the non-CNF track in the recent QBF evaluation. The solver is motivated by the fact that it is easy to construct Quantified Boolean Formulas (QBFs) with short winning strategies (Skolem/Herbrand functions) but are hard to solve by nowadays solvers. This paper argues that a solver benefits from generalizing a set of individual wins into a strategy. This idea is realized on top of the competitive RAReQS algorithm by utilizing machine learning. The results of the implemented prototype are highly encouraging.
• In this article, we develop a notion of Quillen bifibration which combines the two notions of Grothendieck bifibration and of Quillen model structure. In particular, given a bifibration $p:\mathcal E\to\mathcal B$, we describe when a family of model structures on the fibers $\mathcal E_A$ and on the basis category $\mathcal B$ combines into a model structure on the total category $\mathcal E$, such that the functor $p$ preserves cofibrations, fibrations and weak equivalences. Using this Grothendieck construction for model structures, we revisit the traditional definition of Reedy model structures, and possible generalizations, and exhibit their bifibrational nature.
• Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.
• Structured prediction is ubiquitous in applications of machine learning such as knowledge extraction and natural language processing. Structure often can be formulated in terms of logical constraints. We consider the question of how to perform efficient active learning in the presence of logical constraints among variables inferred by different classifiers. We propose several methods and provide theoretical results that demonstrate the inappropriateness of employing uncertainty guided sampling, a commonly used active learning method. Furthermore, experiments on ten different datasets demonstrate that the methods significantly outperform alternatives in practice. The results are of practical significance in situations where labeled data is scarce.
• Sep 27 2017 cs.LO arXiv:1709.09013v1
This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement studied in this paper is a strategy known as change of virtual data structure. By framing metaphorisms in the class of (inductive) regular relations, sufficient conditions are given for such implementations to be calculated using relation algebra. The strategy is illustrated with examples including the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.
• This work is meant to be a step towards the formal definition of the notion of algorithm, in the sense of an equivalence class of programs working "in a similar way". But instead of defining equivalence transformations directly on programs, we look at the computation for each particular argument and give it a structure. This leads to the notion of constructed number: the result of the computation is a constructed number whose constructors (0, successor) carry a history condition (or trace) of their computation. There are equivalence relations on these conditions and on constructed numbers. Two programs are equivalent if they produce equivalent constructed numbers for each argument.
• Recent approaches to verifying programs in separation logics for concurrency have used state transition systems (STSs) to specify the atomic operations of programs. A key challenge in the setting has been to compose such STSs into larger ones, while enabling programs specified under one STS to be linked to a larger one, without reverification. This paper develops a notion of morphism between two STSs which permits such lifting. The morphisms are a constructive form of simulation between the STSs, and lead to a general and concise proof system. We illustrate the concept and its generality on several disparate examples, including staged construction of a readers/writers lock and its proof, and of proofs about quiescence when concurrent programs are executed without external interference.
• Every language recognized by the Lambek calculus with brackets is context-free. This is shown by combining an observation by Jäger with an entirely straightforward adaptation of the method Pentus used for the original Lambek calculus. The case of the variant of the calculus allowing sequents with empty antecedents is slightly more complicated, requiring a restricted use of the multiplicative unit.