Compact categories have lately seen renewed interest via applications to quantum physics. Being essentially finite-dimensional, they cannot accomodate (co)limit-based constructions. For example, they cannot capture protocols such as quantum key distribution, that rely on the law of large numbers. To overcome this limitation, we introduce the notion of a compactly accessible category, relying on the extra structure of a factorisation system. This notion allows for infinite dimension while retaining key properties of compact categories: the main technical result is that the choice-of-duals functor on the compact part extends canonically to the whole compactly accessible category. As an example, we model a quantum key distribution protocol and prove its correctness categorically.
VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It has been used as a vehicle for exploration and validation of novel program verification techniques and for industrial case studies; it has served well at a number of program verification competitions; and it has been used for teaching by multiple teachers independent of the authors. However, until now, while VeriFasts operation has been described informally in a number of publications, and specific verification techniques have been formalized, a clear and precise exposition of how VeriFast works has not yet appeared. In this article we present for the first time a formal definition and soundness proof of a core subset of the VeriFast program verification approach. The exposition aims to be both accessible and rigorous: the text is based on lecture notes for a graduate course on program verification, and it is backed by an executable machine-readable definition and machine-checked soundness proof in Coq.
We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form ${varphi}$ prog ${psi}$, where the assertions $varphi$ and $psi$ are predicates defined by a set Spec of possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also called constrained Horn clauses). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that ${varphi}$ prog ${psi}$ is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here called LA-solving methods, which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of those LA-solving methods. These specifications require the proof of satisfiability of a set PC of constrained Horn clauses that contain nonlinear clauses (that is, clauses with more than one atom in their premise). Then, we present a transformation, called linearization, that converts PC into a set of linear clauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid by LA-solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method.
Priced timed games are optimal-cost reachability games played between two players---the controller and the environment---by moving a token along the edges of infinite graphs of configurations of priced timed automata. The goal of the controller is to reach a given set of target locations as cheaply as possible, while the goal of the environment is the opposite. Priced timed games are known to be undecidable for timed automata with $3$ or more clocks, while they are known to be decidable for automata with $1$ clock. In an attempt to recover decidability for priced timed games Bouyer, Markey, and Sankur studied robust priced timed games where the environment has the power to slightly perturb delays proposed by the controller. Unfortunately, however, they showed that the natural problem of deciding the existence of optimal limit-strategy---optimal strategy of the controller where the perturbations tend to vanish in the limit---is undecidable with $10$ or more clocks. In this paper we revisit this problem and improve our understanding of the decidability of these games. We show that the limit-strategy problem is already undecidable for a subclass of robust priced timed games with $5$ or more clocks. On a positive side, we show the decidability of the existence of almost optimal strategies for the same subclass of one-clock robust priced timed games by adapting a classical construction by Bouyer at al. for one-clock priced timed games.
We put forward a model of action-based randomization mechanisms to analyse quantitative information flow (QIF) under generic leakage functions, and under possibly adaptive adversaries. This model subsumes many of the QIF models proposed so far. Our main contributions include the following: (1) we identify mild general conditions on the leakage function under which it is possible to derive general and significant results on adaptive QIF; (2) we contrast the efficiency of adaptive and non-adaptive strategies, showing that the latter are as efficient as the former in terms of length up to an expansion factor bounded by the number of available actions; (3) we show that the maximum information leakage over strategies, given a finite time horizon, can be expressed in terms of a Bellman equation. This can be used to compute an optimal finite strategy recursively, by resorting to standard methods like backward induction.
In this paper, we have described a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted by bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we have used a notion of power series between Mackey-complete spaces, generalizing the notion of entire functions in C. Finally, we have obtained a quantitative model of Intuitionist Differential Linear Logic, where the syntactic differentiation correspond to the usual one and where the interpretations of proofs satisfy a Taylor expansion decomposition.
$mathbb{Q}_0$ - the involutive meadow of the rational numbers - is the field of the rational numbers where the multiplicative inverse operation is made total by imposing $0^{-1}=0$. In this note, we prove that $mathbb{Q}_0$ cannot be specified by the usual axioms for meadows augmented by a finite set of axioms of the form $(1+ cdots +1+x^2)cdot (1+ cdots +1 +x^2)^{-1}=1$.
The current work introduces the notion of pdominant sets and studies their recursion-theoretic properties. Here a set A is called pdominant iff there is a partial A-recursive function {psi} such that for every partial recursive function {phi} and almost every x in the domain of {phi} there is a y in the domain of {psi} with y<= x and {psi}(y) > {phi}(x). While there is a full {pi}01-class of nonrecursive sets where no set is pdominant, there is no {pi}01-class containing only pdominant sets. No weakly 2-generic set is pdominant while there are pdominant 1-generic sets below K. The halves of Chaitins {Omega} are pdominant. No set which is low for Martin-Lof random is pdominant. There is a low r.e. set which is pdominant and a high r.e. set which is not pdominant.
We propose automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give a probabilistic temporal logic that can express a range of quantitative properties of these models, relating to the probability of an events occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. Our approach is based on an integer discretisation of the models dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies, from the domains of computer security and task scheduling.
Automated verification of living organism models allows us to gain previously unknown knowledge about underlying biological processes. In this paper, we show the benefits to use parametric time Petri nets in order to analyze precisely the dynamic behavior of biological oscillatory systems. In particular, we focus on the resilience properties of such systems. This notion is crucial to understand the behavior of biological systems (e.g. the mammalian circadian rhythm) that are reactive and adaptive enough to endorse major changes in their environment (e.g. jet-lags, day-night alternating work-time). We formalize these properties through parametric TCTL and demonstrate how changes of the environmental conditions can be tackled to guarantee the resilience of living organisms. In particular, we are able to discuss the influence of various perturbations, e.g. artificial jet-lag or components knock-out, with regard to quantitative delays. This analysis is crucial when it comes to model elicitation for dynamic biological systems. We demonstrate the applicability of this technique using a simplified model of circadian clock.
