Search

We analyse the complexity of the satisfiability problem (SAT) for transformer encoders (TE), naturally occurring in formal verification or interpretation tasks. We find that SAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where SAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE -- those restricted by fixed -- width arithmetic-lead to the decidability of SAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where SAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning.

Verifying properties and interpreting the behaviour of deep neural networks (DNN) is an important task given their ubiquitous use in applications, including safety-critical ones, and their black-box nature. We propose an automata-theoric approach to tackling problems arising in DNN analysis. We show that the input-output behaviour of a DNN can be captured precisely by a (special) weak B\"uchi automaton and we show how these can be used to address common verification and interpretation tasks of DNN like adversarial robustness or minimum sufficient reasons.

Otto's Theorem characterises the bisimulation-invariant PTIME queries over graphs as exactly those that can be formulated in the polyadic mu-calculus, hinging on the Immerman-Vardi Theorem which characterises PTIME (over ordered structures) by First-Order Logic with least fixpoints. This connection has been extended to characterise bisimulation-invariant EXPTIME by an extension of the polyadic mu-calculus with functions on predicates, making use of Immerman's characterisation of EXPTIME by Second-Order Logic with least fixpoints. In this paper we show that the bisimulation-invariant versions of all classes in the exponential time hierarchy have logical counterparts which arise as extensions of the polyadic mu-calculus by higher-order functions. This makes use of the characterisation of k-EXPTIME by Higher-Order Logic (of order k+1) with least fixpoints, due to Freire and Martins., Comment: In Proceedings GandALF 2022, arXiv:2209.09333

Output reachability and adversarial robustness are among the most relevant safety properties of neural networks. We show that in the context of Message Passing Neural Networks (MPNN), a common Graph Neural Network (GNN) model, formal verification is impossible. In particular, we show that output reachability of graph-classifier MPNN, working over graphs of unbounded size, non-trivial degree and sufficiently expressive node labels, cannot be verified formally: there is no algorithm that answers correctly (with yes or no), given an MPNN, whether there exists some valid input to the MPNN such that the corresponding output satisfies a given specification. However, we also show that output reachability and adversarial robustness of node-classifier MPNN can be verified formally when a limit on the degree of input graphs is given a priori. We discuss the implications of these results, for the purpose of obtaining a complete picture of the principle possibility to formally verify GNN, depending on the expressiveness of the involved GNN models and input-output specifications.

We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and specifications over the input/output dimension given by conjunctions of linear inequalities. We recapitulate the proof and repair some flaws in the original upper and lower bound proofs. Motivated by the general result, we show that NP-hardness already holds for restricted classes of simple specifications and neural networks. Allowing for a single hidden layer and an output dimension of one as well as neural networks with just one negative, zero and one positive weight or bias is sufficient to ensure NP-hardness. Additionally, we give a thorough discussion and outlook of possible extensions for this direction of research on neural network verification., Comment: arXiv admin note: substantial text overlap with arXiv:2108.13179

We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and conjunctive input/output specifications. We repair some flaws in the original upper and lower bound proofs. We then show that NP-hardness already holds for restricted classes of simple specifications and neural networks with just one layer, as well as neural networks with minimal requirements on the occurring parameters.

We investigate the expressive power of the two main kinds of program logics for complex, non-regular program properties found in the literature: those extending propositional dynamic logic (PDL), and those extending the modal mu-calculus. This is inspired by the recent discovery of a decidable program logic called Visibly Pushdown Fixpoint Logic with Chop which extends both the modal mu-calculus and PDL over visibly pushdown languages, which, so far, constituted the ends of two pillars of decidable program logics. Here we show that this logic is not only more expressive than either of its two fragments, but in fact even more expressive than their union. Hence, the decidability border amongst program logics has been properly pushed up. We complete the picture by providing results separating all the PDL-based and modal fixpoint logics with regular, visibly pushdown and arbitrary context-free constructions., Comment: In Proceedings EXPRESS/SOS 2021, arXiv:2108.09624

Local fixpoint iteration describes a technique that restricts fixpoint iteration in function spaces to needed arguments only. It has been studied well for first-order functions in abstract interpretation and also in model checking. Here we consider the problem for least and greatest fixpoints of arbitrary type order. We define an abstract algebra of simply typed higher-order functions with fixpoints that can express fixpoint evaluation problems as they occur routinely in various applications, including program verification. We present an algorithm that realises local fixpoint iteration for such higher-order fixpoints, prove its correctness and study its optimisation potential in the context of several applications., Comment: In Proceedings GandALF 2020, arXiv:2009.09360

The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent calculus are finite trees obtained by successively applying proof rules to formulas, thus simplifying them step-by-step. Students often struggle with the mathematical formalities and the level of abstraction that topics like formal logic and formal proofs involve. The difficulties can be categorised as syntactic or semantic. On the syntactic level, students need to understand what a correctly formed proof is, how rules can be applied (on paper for instance) without leaving the mathematical framework of the sequent calculus, and so on. Beyond this, on the semantic level, students need to acquire strategies that let them find the right proof. The Sequent Calculus Trainer is a tool that is designed to aid students in learning the techniques of proving given statements formally. In this paper we describe the didactical motivation behind the tool and the techniques used to address issues on the syntactic as well as on the semantic level., Comment: In Proceedings ThEdu'17, arXiv:1803.00722

We study the following natural variation on the classical universality problem: given a language $L(M)$ represented by $M$ (e.g., a DFA/RE/NFA/PDA), does there exist an integer $\ell \geq 0$ such that $\Sigma^\ell \subseteq L(M)$? In the case of an NFA, we show that this problem is NEXPTIME-complete, and the smallest such $\ell$ can be doubly exponential in the number of states. This particular case was formulated as an open problem in 2009, and our solution uses a novel and involved construction. In the case of a PDA, we show that it is recursively unsolvable, while the smallest such $\ell$ is not bounded by any computable function of the number of states. In the case of a DFA, we show that the problem is NP-complete, and $e^{\sqrt{n \log n} (1+o(1))}$ is an asymptotically tight upper bound for the smallest such $\ell$, where $n$ is the number of states. Finally, we prove that in all these cases, the problem becomes computationally easier when the length $\ell$ is also given in binary in the input: it is polynomially solvable for a DFA, PSPACE-complete for an NFA, and co-NEXPTIME-complete for a PDA., Comment: This is the full version of the conference paper https://doi.org/10.4230/LIPIcs.STACS.2020.16

We consider simulation games played between Spoiler and Duplicator on two B\"uchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win the game (with unbounded buffers)., Comment: In Proceedings GandALF 2016, arXiv:1609.03648

We study the axiomatisability of the iteration-free fragment of Propositional Dynamic Logic with Intersection and Tests. The combination of program composition, intersection and tests makes its proof-theory rather difficult. We develop a normal form for formulae which minimises the interaction between these operators, as well as a refined canonical model construction. From these we derive an axiom system and a proof of its strong completeness., Comment: In Proceedings GandALF 2016, arXiv:1609.03648

We consider simulation games played between Spoiler and Duplicator on two Buchi automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers before she executes them on her structure. Previous work on such games using a single buffer has shown that they are useful to approximate language inclusion problems. We study the decidability and complexity and show that games with two buffers can be used to approximate corresponding problems on finite transducers, i.e. the inclusion problem for rational relations over infinite words., Comment: In Proceedings Cassting'16/SynCoP'16, arXiv:1608.00177

The polyadic mu-calculus is a modal fixpoint logic whose formulas define relations of nodes rather than just sets in labelled transition systems. It can express exactly the polynomial-time computable and bisimulation-invariant queries on finite graphs. In this paper we show a hierarchy result with respect to expressive power inside the polyadic mu-calculus: for every level of fixpoint alternation, greater arity of relations gives rise to higher expressive power. The proof uses a diagonalisation argument., Comment: In Proceedings FICS 2015, arXiv:1509.02826

Protein-DNA interactions are crucial for all biological processes. One of the most important fundamental aspects of these interactions is the process of protein searching and recognizing specific binding sites on DNA. A large number of experimental and theoretical investigations have been devoted to uncovering the molecular description of these phenomena, but many aspects of the mechanisms of protein search for the targets on DNA remain not well understood. One of the most intriguing problems is the role of multiple targets in protein search dynamics. Using a recently developed theoretical framework we analyze this question in detail. Our method is based on a discrete-state stochastic approach that takes into account most relevant physical-chemical processes and leads to fully analytical description of all dynamic properties. Specifically, systems with two and three targets have been explicitly investigated. It is found that multiple targets in most cases accelerate the search in comparison with a single target situation. However, the acceleration is not always proportional to the number of targets. Surprisingly, there are even situations when it takes longer to find one of the multiple targets in comparison with the single target. It depends on the spatial position of the targets, distances between them, average scanning lengths of protein molecules on DNA, and the total DNA lengths. Physical-chemical explanations of observed results are presented. Our predictions are compared with experimental observations as well as with results from a continuum theory for the protein search. Extensive Monte Carlo computer simulations fully support our theoretical calculations.

We present the Sequent Calculus Trainer, a tool that supports students in learning how to correctly construct proofs in the sequent calculus for first-order logic with equality. It is a proof assistant fostering the understanding of all the syntactic principles that need to be obeyed in constructing correct proofs. It does not provide any help in finding good proof strategies. Instead it aims at understanding the sequent calculus on a lower syntactic level that needs to be mastered before one can consider proof strategies. Its main feature is a proper feedback system embedded in a graphical user interface. We also report on some empirical findings that indicate how the Sequent Calculus Trainer can improve the students' success in learning sequent calculus for full first-order logic., Comment: Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, Jo\~ao Marcos, Mar\'ia Manzano, Sophie Pinchinat, Fran\c{c}ois Schwarzentruber

We report condensation of hexagonal whispering gallery modes (WGM) at room temperature in ZnO microwires that embody nearly perfect polygonal whispering gallery microresonators. The condensate regime is achieved in the UV spectral range only at energies below the first longitudinal optical (LO) phonon replica of the free ZnO A-exciton transition and at non-zero wave vectors. We demonstrate that the multimodality of the WGM system and the high population of free excitons and phonons with various momenta strongly enhance the probability of an interaction of quasiparticles of the cavity exciton-photon system with LO phonons. We further examine the far-field mode pattern of lasing WGM and demonstrate their spatial coherence.

It is known that the model checking problem for the modal mu-calculus reduces to the problem of solving a parity game and vice-versa. The latter is realised by the Walukiewicz formulas which are satisfied by a node in a parity game iff player 0 wins the game from this node. Thus, they define her winning region, and any model checking algorithm for the modal mu-calculus, suitably specialised to the Walukiewicz formulas, yields an algorithm for solving parity games. In this paper we study the effect of employing the most straight-forward mu-calculus model checking algorithm: fixpoint iteration. This is also one of the few algorithms, if not the only one, that were not originally devised for parity game solving already. While an empirical study quickly shows that this does not yield an algorithm that works well in practice, it is interesting from a theoretical point for two reasons: first, it is exponential on virtually all families of games that were designed as lower bounds for very particular algorithms suggesting that fixpoint iteration is connected to all those. Second, fixpoint iteration does not compute positional winning strategies. Note that the Walukiewicz formulas only define winning regions; some additional work is needed in order to make this algorithm compute winning strategies. We show that these are particular exponential-space strategies which we call eventually-positional, and we show how positional ones can be extracted from them., Comment: In Proceedings GandALF 2014, arXiv:1408.5560

Simulation relations are an important tool in automata theory because they provide efficiently computable approximations to language inclusion. In recent years, extensions of ordinary simulations have been studied, for instance multi-pebble and multi-letter simulations which yield better approximations and are still polynomial-time computable. In this paper we study the limitations of approximating language inclusion in this way: we introduce a natural extension of multi-letter simulations called buffered simulations. They are based on a simulation game in which the two players share a FIFO buffer of unbounded size. We consider two variants of these buffered games called continuous and look-ahead simulation which differ in how elements can be removed from the FIFO buffer. We show that look-ahead simulation, the simpler one, is already PSPACE-hard, i.e. computationally as hard as language inclusion itself. Continuous simulation is even EXPTIME-hard. We also provide matching upper bounds for solving these games with infinite state spaces., Comment: In Proceedings AFL 2014, arXiv:1405.5272