total 9267took 0.13s

Uniform rationality of Poincaré series of p-adic equivalence relations and Igusa's conjecture on exponential sumsMar 15 2019This thesis contains some new results on the uniform rationality of Poincar\'e series of p-adic equivalence relations and Igusa's conjecture on exponential sums

Mutual CoinductionMar 14 2019In this paper we present mutual coinduction as a dual of mutual induction and as a generalization of standard coinduction. In particular, we present a formal definition of mutual induction and mutual coinduction, and in the process we present, and prove, ... More

A two-dimensional metric temporal logicMar 14 2019We introduce a two-dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness ... More

A Functional (Monadic) Second-Order Theory of Infinite TreesMar 14 2019This paper presents a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. MSO on infinite trees is a rich system, and its decidability ("Rabin's Tree Theorem") is one of the most powerful known results concerning the decidability ... More

Completeness of the ZX-CalculusMar 13 2019The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which ... More

Effective local compactness and the hyperspace of located setsMar 13 2019We revisit the definition of effective local compactness, and propose an approach that works for arbitrary countably-based spaces extending the previous work on computable metric spaces. We use this to show that effective local compactness suffices to ... More

SymPas: Symbolic Program SlicingMar 13 2019Program slicing is a technique for simplifying programs by focusing on selected aspects of their behaviour. Current mainstream static slicing methods operate on the PDG (program dependence graph) or SDG (system dependence graph), but these friendly graph ... More

Blackbox End-to-End Verification of Ground Robot Safety and LivenessMar 12 2019We formally prove end-to-end correctness of a ground robot implemented in a simulator. We use an untrusted controller supervised by a verified sandbox. Contributions include: (i) A model of the robot in differential dynamic logic, which specifies assumptions ... More

On first-order expressibility of satisfiability in submodelsMar 12 2019Let $\kappa,\lambda$ be regular cardinals, $\lambda\le\kappa$, let $\varphi$ be a sentence of the language $L_{\kappa,\lambda}$ in a given signature, and let $\vartheta(\varphi)$ express the fact that $\varphi$ holds in a submodel, i.e., any model $\mathfrak ... More

Probabilistic Temporal Logic over Finite Traces (Technical Report)Mar 12 2019Temporal logics over finite traces have recently gained attention due to their use in real-world applications, in particular in business process modelling and planning. In real life, processes contain some degree of uncertainty that is impossible to handle ... More

Model Checking ATL* on vCGSMar 11 2019We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model checking ATL* on iCGS.

DCSYNTH: A Tool for Guided Reactive Synthesis with Soft RequirementsMar 10 2019This paper proposes a technique for the synthesis of high quality controllers from logical specification in an interval temporal logic Quantified Discrete Duration Calculus (QDDC). The specification consists of hard and soft requirements. We compute the ... More

Timed Systems through the Lens of LogicMar 09 2019In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can ... More

Trace Equivalence and Epistemic Logic to Express Security PropertiesMar 09 2019In process algebras, security properties are expressed as equivalences between processes, but which equivalence is suitable is not clear. This means that there is a gap between an intuitive security notion and the formulation. Appropriate formalization ... More

Polar Coding with Chemical Reaction NetworksMar 09 2019In this paper, we propose a new polar coding scheme with molecular programming, which is capable of highly parallel implementation at a nano-scale without a need of electrical power sources. We designed chemical reaction networks (CRN) to employ either ... More

Definable Topological Dynamics of $SL_2(\mathbb{C}((t))$Mar 08 2019We initiate a study of definable topological dynamics for groups definable in metastable theories. Specifically, we consider the special linear group $G = SL_2$ with entries from $M = \mathbb{C}((t))$; the field of formal Laurent series with complex coefficients. ... More

Strongly Minimal Steiner Systems I: ExistenceMar 08 2019A linear space is a system of points and lines such that any two distinct points determine a unique line; a Steiner $k$-system (for $k \geq 2$) is a linear space such that each line has size exactly $k$. Clearly, as a two-sorted structure, no linear space ... More

Descriptive Complexity of Deterministic Polylogarithmic TimeMar 08 2019We propose a logical characterization of problems solvable in deterministic polylogarithmic time (PolylogTime). We introduce a novel, two-sorted logic that separates the elements of the input domain from the bit positions needed to address these elements. ... More

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for EMar 07 2019We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation where fast linear classifier is trained and used together with manually engineered ... More

An algorithmic approach to the existence of ideal objects in commutative algebraMar 07 2019The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive ... More

Only Connect, SecurelyMar 07 2019The lattice model proposed by Denning in her seminal work provided secure information flow analyses with an intuitive and uniform mathematical foundation. Different organisations, however, may employ quite different security lattices. In this paper, we ... More

Incremental Computation of Concept DiagramsMar 06 2019Suppose a formal context K=(G,M,I) is given, whose concept lattice B(K) with an attribute-additive concept diagram is already known, and an attribute column C=(G,{n},J) shall be inserted to or removed from it. This paper introduces and proves an incremental ... More

GRUNGE: A Grand Unified ATP ChallengeMar 06 2019This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order ... More

On the Succinctness of Atoms of DependencyMar 06 2019Propositional team logic is the propositional analog to first-order team logic. Non-classical atoms of dependence, independence, inclusion, exclusion and anonymity can be expressed in it, but for all atoms except dependence only exponential translation ... More

Pinaka: Symbolic Execution meets Incremental Solving (Competition Contribution)Mar 06 2019Many modern-day solvers offer functionality for incremental SAT solving, which preserves the state of the solver across invocations. This is beneficial when multiple, closely related SAT queries need to be fed to the solver. Pinaka is a symbolic execution ... More

PDP: A General Neural Framework for Learning Constraint Satisfaction SolversMar 05 2019There have been recent efforts for incorporating Graph Neural Network models for learning full-stack solvers for constraint satisfaction problems (CSP) and particularly Boolean satisfiability (SAT). Despite the unique representational power of these neural ... More

Sequential Relational DecompositionMar 04 2019The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural ... More

Bicategories in Univalent FoundationsMar 04 2019We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of those, we develop the notion of ... More

Differentiable Causal Computations via Delayed TraceMar 04 2019We investigate causal computations taking sequences of inputs to sequences of outputs where the $n$th output depends on the first $n$ inputs only. We model these in category theory via a construction taking a Cartesian category $C$ to another category ... More

Modular specification of monads through higher-order presentationsMar 03 2019In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they ... More

Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe RegionsMar 02 2019The next generation of aircraft collision avoidance systems frame the problem as a Markov decision process and use dynamic programming to optimize the alerting logic. The resulting system uses a large lookup table to determine advisories given to pilots, ... More

Model completeness and relative decidabilityMar 02 2019We study the implications of model completeness of a theory for the effectiveness of presentations of models of that theory. It is immediate that for a computable model $\mathcal A$ of a computably enumerable, model complete theory, the entire elementary ... More

2LS: Heap Analysis and Memory Safety (Competition Contribution)Mar 02 20192LS is a framework for analysis of sequential C programs that can verify and refute program assertions and termination. The 2LS framework is built upon the CPROVER infrastructure and implements template-based synthesis techniques, e.g. to find invariants ... More

Computability Aspects of Differential Games in Euclidian SpacesMar 02 2019We study computability-theoretic aspects of differential games. Our focus is on pursuit and evasion games played in Euclidean spaces in the tradition of Rado's "Lion versus Man" game. In some ways, these games can be viewed as continuous versions of reachability ... More

On universal modules with pure embeddingsMar 01 2019Mar 12 2019We show that certain classes of modules have universal models with respect to pure embeddings. $Theorem.$ Let $R$ be a ring, $T$ a first-order theory with an infinite model extending the theory of $R$-modules and $K^T=(Mod(T), \leq_{pp})$ (where $\leq_{pp}$ ... More

On universal modules with pure embeddingsMar 01 2019We show that certain classes of modules have universal models with respect to pure embeddings. $Theorem.$ Let $R$ be a ring, $T$ a first-order theory with an infinite model extending the theory of $R$-modules and $K^T=(Mod(T), \leq_{pp})$ (where $\leq_{pp}$ ... More

Strict Superstablity and Decidability of Certain Generic GraphsMar 01 2019We show that the Hrushovski-\fraisse limit of certain classes of trees lead to strictly superstable theories of various U-ranks. In fact, for each $ \alpha\in\omega+1\backslash\{0\} $ we introduce a strictly superstable theory of U-rank $ \alpha. $ Furthermore, ... More

A Trichotomy for Regular Trail QueriesMar 01 2019Regular path queries (RPQs) are an essential component of graph query languages. Such queries consider a regular expression r and a directed edge-labeled graph G and search for paths in G for which the sequence of labels is in the language of r. In order ... More

Relational Differential Dynamic LogicMar 01 2019In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations ... More

Sequentiality of String-to-Context TransducersFeb 28 2019Transducers extend finite state automata with outputs, and describe transformations from strings to strings. Sequential transducers, which have a deterministic behaviour regarding their input, are of particular interest. However, unlike finite-state automata, ... More

Semantics of higher-order probabilistic programs with conditioningFeb 28 2019We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the ... More

Infinite Types, Infinite Data, Infinite InteractionFeb 28 2019We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers ... More

From Cubes to Twisted Cubes via Graph Morphisms in Type TheoryFeb 27 2019Cube categories are used to encode higher-dimensional structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of such higher categories. Bezem, Coquand, ... More

From Cubes to Twisted Cubes via Graph Morphisms in Type TheoryFeb 27 2019Mar 03 2019Cube categories are used to encode higher-dimensional structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of such higher categories. Bezem, Coquand, ... More

A Tenth Hilbert Problem-like Result: The Decidability of MLS with Unordered Cartesian ProductFeb 27 2019Using the technique of formative processes, I solve the decidability problem of MLS with unordered cartesian product in the positive. Moreover I give a pure combinatorial description of the satisfiable MLS with unordered cartesian product-formulas for ... More

Algebraic Invariants for Linear Hybrid AutomataFeb 27 2019We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given unguarded linear hybrid automaton (i.e., a hybrid automaton having only unguarded transitions, all of whose assignments are given ... More

HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo TheoriesFeb 27 2019We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC) - a system of higher-order logic modulo theories - and prove its soundness and refutational completeness w.r.t. the standard semantics. As corollaries, we obtain ... More

Induction, Coinduction, and Fixed Points in PL Type TheoryFeb 26 2019Recently we presented a concise survey of the formulation of the induction and coinduction principles, and some concepts related to them, in programming languages type theory and four other mathematical disciplines. The presentation in type theory involved ... More

Induction, Coinduction, and Fixed Points: Intuitions and TutorialFeb 26 2019Recently we presented a concise survey of the formulation of the induction and coinduction principles, and some concepts related to them, in five different fields mathematical fields, hence shedding some light on the precise relation between these fields. ... More

SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --Feb 26 2019We present the derivation reduction problem for SLD-resolution, the undecidable problem of finding a finite subset of a set of clauses from which the whole set can be derived using SLD-resolution. We study the reducibility of various fragments of second-order ... More

Correct and Efficient Antichain Algorithms for Refinement CheckingFeb 26 2019Refinement checking plays an important role in system verification. This means that the correctness of the system is established by showing a refinement relation between two models; one for the implementation and one for the specification. In "More Anti-chain ... More

Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster VerificationFeb 26 2019Deep neural networks (DNNs) have been shown lack of robustness for the vulnerability of their classification to small perturbations on the inputs. This has led to safety concerns of applying DNNs to safety-critical domains. Several verification approaches ... More

Adding the Power-Set to Description LogicsFeb 26 2019We explore the relationships between Description Logics and Set Theory. The study is carried on using, on the set-theoretic side, a very rudimentary axiomatic set theory Omega, consisting of only four axioms characterizing binary union, set difference, ... More

A New Linear Time Correctness Condition for Multiplicative Linear LogicFeb 26 2019In this paper, we give a new linear time correctness condition for proof nets of Multiplicative Linear Logic without units. Our approach is based on a rewriting system over trees. We have only three rewrite rules. Compared to previous linear time correctness ... More

A New Linear Time Correctness Condition for Multiplicative Linear LogicFeb 26 2019Mar 04 2019In this paper, we give a new linear time correctness condition for proof nets of Multiplicative Linear Logic without units. Our approach is based on a rewriting system over trees. We have only three rewrite rules. Compared with previous linear time correctness ... More

Dependent choice as a termination principleFeb 25 2019We introduce a new formulation of the axiom of dependent choice that can be viewed as an abstract termination principle, which generalises the recursive path orderings used to establish termination of rewrite systems. We consider several variants of our ... More

Homogenousness and SpecificityFeb 25 2019We interpret homogenousness as a second order property and base it on the same principle as nonmonotonic logic: there might be a small set of exceptions.

Algebraic Type Theory and Universe HierarchiesFeb 23 2019It is commonly believed that algebraic notions of type theory support only universes \`a la Tarski, and that universes \`a la Russell must be removed by elaboration. We clarify the state of affairs, recalling the details of Cartmell's discipline of _generalized ... More

The Additive Ordered Structure of Natural Numbers with a Beatty SequenceFeb 23 2019We have provided a pure model-theoretic proof for the decidability of the additive structure of the natural numbers together with a function {f} sending {x} to {[\phi x]} with {\phi} the golden ratio.

Fully Automatic, Verified Classification of all Frankl-Complete (FC(6)) Set FamiliesFeb 23 2019The Frankl's conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. A family Fc is called Frankl-complete (or FC-family) if in every union-closed ... More

Automating the Diagram Method to Prove Correctness of Program TransformationsFeb 22 2019We report on the automation of a technique to prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. A program transformation is correct ... More

Reducing Total Correctness to Partial Correctness by a Transformation of the Language SemanticsFeb 22 2019We give a language-parametric solution to the problem of total correctness, by automatically reducing it to the problem of partial correctness, under the assumption that an expression whose value decreases with each program step in a well-founded order ... More

Fast Computations on Ordered Nominal SetsFeb 22 2019We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. In contrast to previous approaches, we work directly at the level of orbits, ... More

On Nominal Syntax and Permutation Fixed PointsFeb 22 2019We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion ... More

On the growth rate of chromatic numbers of finite subgraphsFeb 21 2019Feb 25 2019We prove that, for every function $f:\mathbb{N} \rightarrow \mathbb{N}$, there is a graph $G$ with uncountable chromatic number such that, for every $k \in \mathbb{N}$ with $k \geq 3$, every subgraph of $G$ with fewer than $f(k)$ vertices has chromatic ... More

On the growth rate of chromatic numbers of finite subgraphsFeb 21 2019We prove that, for every function $f:\mathbb{N} \rightarrow \mathbb{N}$, there is a graph $G$ with uncountable chromatic number such that, for every $k \in \mathbb{N}$ with $k \geq 3$, every subgraph of $G$ with fewer than $f(k)$ vertices has chromatic ... More

Aperiodic Weighted Automata and Weighted First-Order LogicFeb 21 2019By fundamental results of Sch\"utzenberger, McNaughton and Papert from the 1970s, the classes of first-order definable and aperiodic languages coincide. Here, we extend this equivalence to a quantitative setting. For this, weighted automata form a general ... More

On the qubit routing problemFeb 21 2019We introduce a new architecture-agnostic methodology for mapping abstract quantum circuits to realistic quantum computing devices with restricted qubit connectivity, as implemented by Cambridge Quantum Computing's tket compiler. We present empirical results ... More

Schematic Refutations of Formula SchemataFeb 21 2019Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new ... More

A complete axiomatisation of reversible Kleene latticesFeb 21 2019We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set ... More

Limit Learning Equivalence StructuresFeb 21 2019While most research in Gold-style learning focuses on learning formal languages, we consider the identification of computable structures, specifically equivalence structures. In our core model the learner gets more and more information about which pairs ... More

Characterizing Strongly First Order Dependencies: The Non-Jumping Relativizable CaseFeb 20 2019Team Semantics generalizes Tarski's Semantics for First Order Logic by allowing formulas to be satisfied or not satisfied by sets of assignments rather than by single assignments. Because of this, in Team Semantics it is possible to extend the language ... More

Founded World Views with Autoepistemic Equilibrium LogicFeb 20 2019Defined by Gelfond in 1991 (G91), epistemic specifications (or programs) are an extension of logic programming under stable models semantics that introducessubjective literals. A subjective literal al-lows checking whether some regular literal is true ... More

An Adequate While-Language for Hybrid ComputationFeb 20 2019Hybrid computation combines discrete and continuous dynamics in the form of an entangled mixture inherently present both in various natural phenomena, and in applications ranging from control theory to microbiology. The emergent behaviours bear signs ... More

The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and SpaceFeb 20 2019We study the weak call-by-value $\lambda$-calculus as a model for computational complexity theory and establish the natural measures for time and space -- the number of beta-reductions and the size of the largest term in a computation -- as reasonable ... More

Continuous Ordinary Differential Equations and Infinite Time Turing MachinesFeb 19 2019We consider Continuous Ordinary Differential Equations (CODE) y'=f(y), where f is a continuous function. They are known to always have solutions for a given initial condition y(0)=y0, these solutions being possibly non unique. We restrict to our attention ... More

Uniform Substitution in One Fell SwoopFeb 19 2019Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks does this paper introduce a uniform substitution ... More

Uniform Substitution in One Fell SwoopFeb 19 2019Feb 27 2019Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks does this paper introduce a uniform substitution ... More

The dual of compact partially ordered spaces is a varietyFeb 19 2019In a recent paper (2018), D. Hofmann, R. Neves and P. Nora proved that the dual of the category of compact partially ordered spaces and monotone continuous maps is a quasi-variety - not finitary, but bounded by $\aleph_1$. An open question was: is it ... More

The dual of compact partially ordered spaces is a varietyFeb 19 2019Feb 22 2019In a recent paper (2018), D. Hofmann, R. Neves and P. Nora proved that the dual of the category of compact partially ordered spaces and monotone continuous maps is a quasi-variety - not finitary, but bounded by $\aleph_1$. An open question was: is it ... More

Elementary-base cirquent calculus II: Choice quantifiersFeb 19 2019Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article "Elementary-base cirquent calculus I: Parallel and choice connectives" built the sound and complete axiomatization CL16 ... More

Set-theoretic aspects of accessible categoriesFeb 18 2019Mar 01 2019An accessible category is, roughly, a category with all sufficiently directed colimits, in which every object can be resolved as a directed system of "small" subobjects. Such categories admit a purely category-theoretic replacement for cardinality: the ... More

Set-theoretic aspects of accessible categoriesFeb 18 2019An accessible category is, roughly, a category with all sufficiently directed colimits, in which every object can be resolved as a directed system of "small" subobjects. Such categories admit a purely category-theoretic replacement for cardinality: the ... More

Approximations of Isomorphism and Logics with Linear-Algebraic OperatorsFeb 18 2019Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parametrised by a number k and a set Q of primes. The intuition is that two graphs G and H which are equivalent with respect ... More

Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logicsFeb 18 2019This paper is an appendix to the paper "Cut-free Calculi and Relational Semantics for Temporal STIT logics" by Berkel and Lyon, 2019. It provides the completeness proof for the basic STIT logic Ldm (relative to irreflexive, temporal Kripke STIT frames) ... More

Coverability in 1-VASS with Disequality TestsFeb 18 2019We show that the control-state reachability problem for one-dimensional vector addition systems with disequality tests is solvable in polynomial time. For the test-free case we moreover show that control-state reachability is in NC, i.e., solvable in ... More

Homotopy canonicity for cubical type theoryFeb 18 2019Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally ... More

Iterated Belief Base Revision: A Dynamic Epistemic Logic ApproachFeb 17 2019AGM's belief revision is one of the main paradigms in the study of belief change operations. In this context, belief bases (prioritised bases) have been largely used to specify the agent's belief state - whether representing the agent's `explicit beliefs' ... More

Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-CalculusFeb 16 2019We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on neutral terms ... More

Types by Need (Extended Version)Feb 15 2019A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the ... More

A static higher-order dependency pair frameworkFeb 15 2019We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, ... More

Immediately algebraically closed fieldsFeb 15 2019We consider two overlapping classes of fields, IAC and VAC, which are defined using valuation theory but which do not involve a distinguished valuation. Rather, each class is defined by a condition that quantifies over all possible valuations on the field. ... More

Coalgebra Learning via DualityFeb 15 2019Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. In this paper, we generalise learning to the theory of coalgebras. The approach relies on the use of logical formulas as tests, based on ... More

Shepherding Hordes of Markov ChainsFeb 15 2019This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, planning under partial observability, and sketching of probabilistic programs. ... More

Descriptive complexity for minimal time of cellular automataFeb 15 2019Descriptive complexity may be useful to design programs in a natural declarative way. This is important for parallel computation models such as cellular automata, because designing parallel programs is considered difficult. Our paper establishes logical ... More

Environmentally-friendly GR(1) SynthesisFeb 14 2019Many problems in reactive synthesis are stated using two formulas ---an environment assumption and a system guarantee--- and ask for an implementation that satisfies the guarantee in environments that satisfy their assumption. Reactive synthesis tools ... More

Which is the least complex explanation? Abduction and complexityFeb 14 2019It may happen that for a certain abductive problem there are several possible explanations, not all of them mutually compatible. What explanation is selected and which criteria are used to select it? This is the well-known problem of the selection of ... More

Change Actions: Models of Generalised DifferentiationFeb 14 2019Cai et al. have recently proposed change structures as a semantic framework for incremental computation. We generalise change structures to arbitrary cartesian categories and propose the notion of change action model as a categorical model for (higher-order) ... More

Overt choiceFeb 14 2019We introduce and study the notion of overt choice for countably-based spaces and for CoPolish spaces. Overt choice is the task of producing a point in a closed set specified by what open sets intersect it. We show that the question of whether overt choice ... More

HyPLC: Hybrid Programmable Logic Controller Program Translation for VerificationFeb 14 2019Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such ... More