 |
 |
Volume 5, Issue 2
2009
1. A Faithful Semantics for Generalised Symbolic Trajectory Evaluation
Generalised Symbolic Trajectory Evaluation (GSTE) is a high-capacity formal verification technique for hardware. GSTE uses abstraction, meaning that details of the circuit behaviour are removed from the circuit model. A semantics for GSTE can be used to predict and understand why certain circuit properties can or cannot be proven by GSTE. Several semantics have been described for GSTE. These semantics, however, are not faithful to the proving power of GSTE-algorithms, that is, the GSTE-algorithms are incomplete with respect to the semantics. The abstraction used in GSTE makes it hard to understand why a specific property can, or cannot, be proven by GSTE. The semantics mentioned above cannot help the user in doing so. The contribution of this paper is a faithful semantics for GSTE. That is, we give a simple formal theory that deems a property to be true if-and-only-if the property can be proven by a GSTE-model checker. We prove that the GSTE algorithm is sound and complete with respect to this semantics.
2. Neighbourhood Structures: Bisimilarity and Basic Model Theory
Neighbourhood structures are the standard semantic tool used to reason about non-normal modal logics. The logic of all neighbourhood models is called classical modal logic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, denoted by 2^2. We use this coalgebraic modelling to derive notions of equivalence between neighbourhood structures. 2^2-bisimilarity and behavioural equivalence are well known coalgebraic concepts, and they are distinct, since 2^2 does not preserve weak pullbacks. We introduce a third, intermediate notion whose witnessing relations we call precocongruences (based on pushouts). We give back-and-forth style characterisations for 2^2-bisimulations and precocongruences, we show that on a single coalgebra, precocongruences capture behavioural equivalence, and that between neighbourhood structures, precocongruences are a better approximation of behavioural equivalence than 2^2-bisimulations. We also introduce a notion of modal saturation for neighbourhood models, and investigate its relationship with definability and image-finiteness. We prove a Hennessy-Milner theorem for modally saturated and for image-finite neighbourhood models. Our main results are an analogue of Van Benthem's characterisation theorem and a model-theoretic proof of Craig interpolation for classical modal logic.
3. A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over some potentially infinite data domain such as integers, reals, etc. Furthermore, we define a logic, called CML (colored markings logic), for the description of CPN configurations. CML is a first-order logic over tokens allowing to reason about their locations and their colors. Both CPNs and CML are parametrized by a color logic allowing to express constraints on the colors (data) associated with tokens. We investigate the decidability of the satisfiability problem of CML and its applications in the verification of CPNs. We identify a fragment of CML for which the satisfiability problem is decidable (whenever it is the case for the underlying color logic), and which is closed under the computations of post and pre images for CPNs. These results can be used for several kinds of analysis such as invariance checking, pre-post condition reasoning, and bounded reachability analysis.
4. Footprints in Local Reasoning
Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We formalise the notion of small specifications in local reasoning and show that for well-founded resource models, a smallest specification always exists that only includes the footprints, and also present results for the non-well-founded case. Finally, we use this theory of footprints to investigate the conditions under which the footprints correspond to the smallest safe states. We present a new model of RAM in which, unlike the standard model, the footprints of every program correspond to the smallest safe states, and we also identify a general condition on the primitive commands of a programming language which guarantees this property for arbitrary models.
5. The Church Problem for Countable Ordinals
A fundamental theorem of Buchi and Landweber shows that the Church synthesis problem is computable. Buchi and Landweber reduced the Church Problem to problems about ω-games and used the determinacy of such games as one of the main tools to show its computability. We consider a natural generalization of the Church problem to countable ordinals and investigate games of arbitrary countable length. We prove that determinacy and decidability parts of the Bu}chi and Landweber theorem hold for all countable ordinals and that its full extension holds for all ordinals < \omega\^\omega.
6. The Omega Rule is $\mathbf{\Pi_{1}^{1}}$-Complete in the $\lambda\beta$-Calculus
In a functional calculus, the so called \Omega-rule states that if two terms P and Q applied to any closed term <i>N</i> return the same value (i.e. PN = QN), then they are equal (i.e. P = Q holds). As it is well known, in the \lambda\beta-calculus the \Omega-rule does not hold, even when the \eta-rule (weak extensionality) is added to the calculus. A long-standing problem of H. Barendregt (1975) concerns the determination of the logical power of the \Omega-rule when added to the \lambda\beta-calculus. In this paper we solve the problem, by showing that the resulting theory is \Pi\_{1}^{1}-complete.
7. Qualitative Logics and Equivalences for Probabilistic Systems
We investigate logics and equivalence relations that capture the qualitative behavior of Markov Decision Processes (MDPs). We present Qualitative Randomized CTL (QRCTL): formulas of this logic can express the fact that certain temporal properties hold over all paths, or with probability 0 or 1, but they do not distinguish among intermediate probability values. We present a symbolic, polynomial time model-checking algorithm for QRCTL on MDPs. The logic QRCTL induces an equivalence relation over states of an MDP that we call qualitative equivalence: informally, two states are qualitatively equivalent if the sets of formulas that hold with probability 0 or 1 at the two states are the same. We show that for finite alternating MDPs, where nondeterministic and probabilistic choices occur in different states, qualitative equivalence coincides with alternating bisimulation, and can thus be computed via efficient partition-refinement algorithms. On the other hand, in non-alternating MDPs the equivalence relations cannot be computed via partition-refinement algorithms, but rather, they require non-local computation. Finally, we consider QRCTL*, that extends QRCTL with nested temporal operators in the same manner in which CTL* extends CTL. We show that QRCTL and QRCTL* induce the same qualitative equivalence on alternating MDPs, while on non-alternating MDPs, the equivalence arising from QRCTL* can be strictly finer. We also provide a full characterization of the relation between […]
8. Ranking Functions for Size-Change Termination II
Size-Change Termination is an increasingly-popular technique for verifying program termination. These termination proofs are deduced from an abstract representation of the program in the form of "size-change graphs". We present algorithms that, for certain classes of size-change graphs, deduce a global ranking function: an expression that ranks program states, and decreases on every transition. A ranking function serves as a witness for a termination proof, and is therefore interesting for program certification. The particular form of the ranking expressions that represent SCT termination proofs sheds light on the scope of the proof method. The complexity of the expressions is also interesting, both practicaly and theoretically. While deducing ranking functions from size-change graphs has already been shown possible, the constructions in this paper are simpler and more transparent than previously known. They improve the upper bound on the size of the ranking expression from triply exponential down to singly exponential (for certain classes of instances). We claim that this result is, in some sense, optimal. To this end, we introduce a framework for lower bounds on the complexity of ranking expressions and prove exponential lower bounds.
9. Solving Simple Stochastic Games with Few Random Vertices
Simple stochastic games are two-player zero-sum stochastic games with turn-based moves, perfect information, and reachability winning conditions. We present two new algorithms computing the values of simple stochastic games. Both of them rely on the existence of optimal permutation strategies, a class of positional strategies derived from permutations of the random vertices. The "permutation-enumeration" algorithm performs an exhaustive search among these strategies, while the "permutation-improvement" algorithm is based on successive improvements, à la Hoffman-Karp. Our algorithms improve previously known algorithms in several aspects. First they run in polynomial time when the number of random vertices is fixed, so the problem of solving simple stochastic games is fixed-parameter tractable when the parameter is the number of random vertices. Furthermore, our algorithms do not require the input game to be transformed into a stopping game. Finally, the permutation-enumeration algorithm does not use linear programming, while the permutation-improvement algorithm may run in polynomial time.
10. Polynomial Size Analysis of First-Order Shapely Functions
We present a size-aware type system for first-order shapely function definitions. Here, a function definition is called shapely when the size of the result is determined exactly by a polynomial in the sizes of the arguments. Examples of shapely function definitions may be implementations of matrix multiplication and the Cartesian product of two lists. The type system is proved to be sound w.r.t. the operational semantics of the language. The type checking problem is shown to be undecidable in general. We define a natural syntactic restriction such that the type checking becomes decidable, even though size polynomials are not necessarily linear or monotonic. Furthermore, we have shown that the type-inference problem is at least semi-decidable (under this restriction). We have implemented a procedure that combines run-time testing and type-checking to automatically obtain size dependencies. It terminates on total typable function definitions.
11. Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
The intuitionistic fragment of the call-by-name version of Curien and Herbelin's \lambda\_mu\_{\~mu}-calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed lambda-calculus. Our embedding is a continuation-and-garbage-passing style translation, the inspiring idea coming from Ikeda and Nakazawa's translation of Parigot's \lambda\_mu-calculus. The embedding strictly simulates reductions while usual continuation-passing-style transformations erase permutative reduction steps. For our intuitionistic sequent calculus, we even only need "units of garbage" to be passed. We apply the same method to other calculi, namely successive extensions of the simply-typed λ-calculus leading to our intuitionistic system, and already for the simplest extension we consider (λ-calculus with generalised application), this yields the first proof of strong normalisation through a reduction-preserving embedding. The results obtained extend to second and higher-order calculi.
12. Simulating reachability using first-order logic with applications to verification of linked data structures
This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of pointer-valued structure fields. One of the main obstacles is specifying and proving the (absence) of reachability properties among dynamically allocated cells. The main technical contributions are methods for simulating reachability in a conservative way using first-order formulas--the formulas describe a superset of the set of program states that would be specified if one had a precise way to express reachability. These methods are employed for semi-automatic program verification (i.e., using programmer-supplied loop invariants) on programs such as mark-and-sweep garbage collection and destructive reversal of a singly linked list. (The mark-and-sweep example has been previously reported as being beyond the capabilities of ESC/Java.)
13. Universal Structures and the logic of Forbidden Patterns
Forbidden Patterns Problems (FPPs) are a proper generalisation of Constraint Satisfaction Problems (CSPs). However, we show that when the input is connected and belongs to a class which has low tree-depth decomposition (e.g. structure of bounded degree, proper minor closed class and more generally class of bounded expansion) any FPP becomes a CSP. This result can also be rephrased in terms of expressiveness of the logic MMSNP, introduced by Feder and Vardi in relation with CSPs. Our proof generalises that of a recent paper by Nesetril and Ossona de Mendez. Note that our result holds in the general setting of problems over arbitrary relational structures (not just for graphs).
14. Polygraphic programs and polynomial-time functions
We study the computational model of polygraphs. For that, we consider polygraphic programs, a subclass of these objects, as a formal description of first-order functional programs. We explain their semantics and prove that they form a Turing-complete computational model. Their algebraic structure is used by analysis tools, called polygraphic interpretations, for complexity analysis. In particular, we delineate a subclass of polygraphic programs that compute exactly the functions that are Turing-computable in polynomial time.
15. Explicit fairness in testing semantics
In this paper we investigate fair computations in the pi-calculus. Following Costa and Stirling's approach for CCS-like languages, we consider a method to label process actions in order to filter out unfair computations. We contrast the existing fair-testing notion with those that naturally arise by imposing weak and strong fairness. This comparison provides insight about the expressiveness of the various `fair' testing semantics and about their discriminating power.
16. Formalising the pi-calculus using nominal logic
We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely following the intuitive arguments found in manual proofs. In this way we have covered many of the standard theorems of bisimulation equivalence and congruence, both late and early, and both strong and weak in a uniform manner. We thus provide one of the most extensive formalisations of a process calculus ever done inside a theorem prover. A significant gain in our formulation is that agents are identified up to alpha-equivalence, thereby greatly reducing the arguments about bound names. This is a normal strategy for manual proofs about the pi-calculus, but that kind of hand waving has previously been difficult to incorporate smoothly in an interactive theorem prover. We show how the nominal logic formalism and its support in Isabelle accomplishes this and thus significantly reduces the tedium of conducting completely formal proofs. This improves on previous work using weak higher order abstract syntax since we do not need extra assumptions to filter out exotic terms and can keep all arguments within a familiar first-order logic.