 |
 |
Volume 8, Issue 4
2012
1. First steps in synthetic guarded domain theory: step-indexing in the topos of trees
We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S. Moreover, we give an axiomatic categorical treatment of models of synthetic guarded domain theory and prove that, for any complete Heyting algebra A with a well-founded basis, the topos of sheaves over A forms a model of synthetic guarded domain theory, generalizing the results for S.
2. Linear-use CPS translations in the Enriched Effect Calculus
The enriched effect calculus (EEC) is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. This paper explores the enriched effect calculus as a target language for continuation-passing-style (CPS) translations in which the typing of the translations enforces the linear usage of continuations. We first observe that established call-by-value and call-by name linear-use CPS translations of simply-typed lambda-calculus into intuitionistic linear logic (ILL) land in the fragment of ILL given by EEC. These two translations are uniformly generalised by a single generic translation of the enriched effect calculus into itself. As our main theorem, we prove that the generic self-translation of EEC is involutive up to isomorphism. As corollaries, we obtain full completeness results, both for the generic translation, and for the original call-by-value and call-by-name translations.
3. Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion
We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a "must" parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus.
4. On streams that are finitely red
Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically, but is intuitionistically of strictly decreasing strength. We characterize the differences in strength in a precise way by weak instances of the Law of Excluded Middle.
5. Essential Convexity and Complexity of Semi-Algebraic Constraints
Let \Gamma be a structure with a finite relational signature and a first-order definition in (R;*,+) with parameters from R, that is, a relational structure over the real numbers where all relations are semi-algebraic sets. In this article, we study the computational complexity of constraint satisfaction problem (CSP) for \Gamma: the problem to decide whether a given primitive positive sentence is true in \Gamma. We focus on those structures \Gamma that contain the relations \leq, {(x,y,z) | x+y=z} and {1}. Hence, all CSPs studied in this article are at least as expressive as the feasibility problem for linear programs. The central concept in our investigation is essential convexity: a relation S is essentially convex if for all a,b\inS, there are only finitely many points on the line segment between a and b that are not in S. If \Gamma contains a relation S that is not essentially convex and this is witnessed by rational points a,b, then we show that the CSP for \Gamma is NP-hard. Furthermore, we characterize essentially convex relations in logical terms. This different view may open up new ways for identifying tractable classes of semi-algebraic CSPs. For instance, we show that if \Gamma is a first-order expansion of (R;*,+), then the CSP for \Gamma can be solved in polynomial time if and only if all relations in \Gamma are essentially convex (unless P=NP).
6. Parameterised Multiparty Session Types
For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Gödel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.
7. On Berry's conjectures about the stable order in PCF
PCF is a sequential simply typed lambda calculus language. There is a unique order-extensional fully abstract cpo model of PCF, built up from equivalence classes of terms. In 1979, Gérard Berry defined the stable order in this model and proved that the extensional and the stable order together form a bicpo. He made the following two conjectures: 1) "Extensional and stable order form not only a bicpo, but a bidomain." We refute this conjecture by showing that the stable order is not bounded complete, already for finitary PCF of second-order types. 2) "The stable order of the model has the syntactic order as its image: If a is less than b in the stable order of the model, for finite a and b, then there are normal form terms A and B with the semantics a, resp. b, such that A is less than B in the syntactic order." We give counter-examples to this conjecture, again in finitary PCF of second-order types, and also refute an improved conjecture: There seems to be no simple syntactic characterization of the stable order. But we show that Berry's conjecture is true for unary PCF. For the preliminaries, we explain the basic fully abstract semantics of PCF in the general setting of (not-necessarily complete) partial order models (f-models.) And we restrict the syntax to "game terms", with a graphical representation.
8. Off-line test selection with test purposes for non-deterministic timed automata
This article proposes novel off-line test generation techniques from non-deterministic timed automata with inputs and outputs (TAIOs) in the formal framework of the tioco conformance theory. In this context, a fi?rst problem is the determinization of TAIOs, which is necessary to foresee next enabled actions after an observable trace, but is in general impossible because not all timed automata are determinizable. This problem is solved thanks to an approximate determinization using a game approach. The algorithm performs an io-abstraction which preserves the tioco conformance relation and thus guarantees the soundness of generated test cases. A second problem is the selection of test cases from a TAIO speci?fication. The selection here relies on a precise description of timed behaviors to be tested which is carried out by expressive test purposes modeled by a generalization of TAIOs. Finally, an algorithm is described which generates test cases in the form of TAIOs equipped with verdicts, using a symbolic co-reachability analysis guided by the test purpose. Properties of test cases are then analyzed with respect to the precision of the approximate determinization: when determinization is exact, which is the case on known determinizable classes, in addition to soundness, properties characterizing the adequacy of test cases verdicts are also guaranteed.
9. Petri Net Reachability Graphs: Decidability Status of First Order Properties
We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order and modal languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable problems from undecidable ones. Not only are we able to provide precise borders and a systematic analysis, but we also demonstrate the robustness of our proof techniques.
10. Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path checking can be efficiently parallelized. In addition to the core logic, we consider the extensions of LTL with bounded-future (BLTL) and past-time (LTL+Past) operators. Even though both extensions improve the succinctness of the logic exponentially, path checking remains efficiently parallelizable: Our algorithm for LTL, LTL+Past, and BLTL+Past is in AC^1(logDCFL) \subseteq NC.
11. Linear Dependent Types and Relative Completeness
A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of PCF programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of evaluating them with Krivine's Machine. dlPCF is designed around dependent types and linear logic and is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.
12. Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees
We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.
13. Adaptable processes
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime; this allows to express a wide range of evolvability patterns for concurrent processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that the number of consecutive erroneous states that can be traversed during a computation is bound by some given number k, the latter ensures that if the system enters into a state with errors then a state without errors will be eventually reached. We study the (un)decidability of these two problems in several variants of the calculus, which result from considering dynamic and static topologies of adaptable processes as well as different evolvability patterns. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities.
14. Environment and classical channels in categorical quantum mechanics
We present a both simple and comprehensive graphical calculus for quantum computing. In particular, we axiomatize the notion of an environment, which together with the earlier introduced axiomatic notion of classical structure enables us to define classical channels, quantum measurements and classical control. If we moreover adjoin the earlier introduced axiomatic notion of complementarity, we obtain sufficient structural power for constructive representation and correctness derivation of typical quantum informatic protocols.
15. On computable approximations of Landau's constant
We present an algorithm which computes the Landau constant up to any given precision.
16. The Structure of Differential Invariants and Differential Cut Elimination
The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather ad-hoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze trade-offs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics.
17. A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems
We address a fundamental mismatch between the combinations of dynamics that occur in cyber-physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics. We provide the logical foundations for closing this analytic gap. We develop a formal model for distributed hybrid systems. It combines quantified differential equations with quantified assignments and dynamic dimensionality-changes. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for this logic. This is the first formal verification approach for distributed hybrid systems. We prove that our calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantified differential equations. In our calculus we have proven collision freedom in distributed car control even when an unbounded number of new cars may appear dynamically on the road.
18. Probabilistic modal {\mu}-calculus with independent product
The probabilistic modal {\mu}-calculus is a fixed-point logic designed for expressing properties of probabilistic labeled transition systems (PLTS's). Two equivalent semantics have been studied for this logic, both assigning to each state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotational and the other is a game semantics, specified in terms of two-player stochastic parity games. A shortcoming of the probabilistic modal {\mu}-calculus is the lack of expressiveness required to encode other important temporal logics for PLTS's such as Probabilistic Computation Tree Logic (PCTL). To address this limitation we extend the logic with a new pair of operators: independent product and coproduct. The resulting logic, called probabilistic modal {\mu}-calculus with independent product, can encode many properties of interest and subsumes the qualitative fragment of PCTL. The main contribution of this paper is the definition of an appropriate game semantics for this extended probabilistic {\mu}-calculus. This relies on the definition of a new class of games which generalize standard two-player stochastic (parity) games by allowing a play to be split into concurrent subplays, each continuing their evolution independently. Our main technical result is the equivalence of the two semantics. The proof is carried out in ZFC set theory extended with Martin's Axiom at an uncountable […]
19. Continuous Markovian Logics - Axiomatization and Quantified Metatheory
Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-time labelled Markov processes with arbitrary (analytic) state-spaces, henceforth called continuous Markov processes (CMPs). The modalities of CML evaluate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions of a CMP. In this paper we present weak and strong complete axiomatizations for CML and prove a series of metaproperties, including the finite model property and the construction of canonical models. CML characterizes stochastic bisimilarity and it supports the definition of a quantified extension of the satisfiability relation that measures the "compatibility" between a model and a property. In this context, the metaproperties allows us to prove two robustness theorems for the logic stating that one can perturb formulas and maintain "approximate satisfaction".