 |
 |
Volume 9, Issue 4
2013
1. Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems
Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating into the formula the behavioural information taken from one process - an operation called quotienting - to obtain a new formula that can be verified on a smaller composition from which the incorporated process has been removed. Simplifications of the formula must be applied at each step, so as to maintain the formula at a tractable size. In this paper, we revisit partial model checking. First, we extend quotienting to the network of labelled transition systems model, which subsumes most parallel composition operators, including m-among-n synchronisation and parallel composition using synchronisation interfaces, available in the ELOTOS standard. Second, we reformulate quotienting in terms of a simple synchronous product between a graph representation of the formula (called formula graph) and a process, thus enabling quotienting to be implemented efficiently and easily, by reusing existing tools dedicated to graph compositions. Third, we propose simplifications of the formula as a combination of bisimulations and reductions using Boolean equation systems applied directly to the formula graph, thus enabling formula simplifications also to be implemented efficiently. Finally, we describe an implementation in the CADP (Construction and Analysis of Distributed Processes) toolbox and present some […]
2. Lower Bounds for Existential Pebble Games and k-Consistency Tests
The existential k-pebble game characterizes the expressive power of the existential-positive k-variable fragment of first-order logic on finite structures. The winner of the existential k-pebble game on two given finite structures can be determined in time O(n2k) by dynamic programming on the graph of game configurations. We show that there is no O(n(k-3)/12)-time algorithm that decides which player can win the existential k-pebble game on two given structures. This lower bound is unconditional and does not rely on any complexity-theoretic assumptions. Establishing strong k-consistency is a well-known heuristic for solving the constraint satisfaction problem (CSP). By the game characterization of Kolaitis and Vardi our result implies that there is no O(n(k-3)/12)-time algorithm that decides if strong k-consistency can be established for a given CSP-instance.
3. Non-idempotent intersection types and strong normalisation
We present a typing system with non-idempotent intersection types, typing a term syntax covering three different calculi: the pure {\lambda}-calculus, the calculus with explicit substitutions {\lambda}S, and the calculus with explicit substitutions, contractions and weakenings {\lambda}lxr. In each of the three calculi, a term is typable if and only if it is strongly normalising, as it is the case in (many) systems with idempotent intersections. Non-idempotency brings extra information into typing trees, such as simple bounds on the longest reduction sequence reducing a term to its normal form. Strong normalisation follows, without requiring reducibility techniques. Using this, we revisit models of the {\lambda}-calculus based on filters of intersection types, and extend them to {\lambda}S and {\lambda}lxr. Non-idempotency simplifies a methodology, based on such filter models, that produces modular proofs of strong normalisation for well-known typing systems (e.g. System F). We also present a filter model by means of orthogonality techniques, i.e. as an instance of an abstract notion of orthogonality model formalised in this paper and inspired by classical realisability. Compared to other instances based on terms (one of which rephrases a now standard proof of strong normalisation for the {\lambda}-calculus), the instance based on filters is shown to be better at proving strong normalisation results for {\lambda}S and {\lambda}lxr. Finally, the bounds on the longest reduction […]
4. Step-Indexed Relational Reasoning for Countable Nondeterminism
Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for programming languages with countable nondeterminism is challenging. We present a step-indexed logical relations model of a higher-order functional programming language with countable nondeterminism and demonstrate how it can be used to reason about contextually defined may- and must-equivalence. In earlier step-indexed models, the indices have been drawn from {\omega}. Here the step-indexed relations for must-equivalence are indexed over an ordinal greater than {\omega}.
5. Satisfiability Games for Branching-Time Logics
The satisfiability problem for branching-time temporal logics like CTL*, CTL and CTL+ has important applications in program specification and verification. Their computational complexities are known: CTL* and CTL+ are complete for doubly exponential time, CTL is complete for single exponential time. Some decision procedures for these logics are known; they use tree automata, tableaux or axiom systems. In this paper we present a uniform game-theoretic framework for the satisfiability problem of these branching-time temporal logics. We define satisfiability games for the full branching-time temporal logic CTL* using a high-level definition of winning condition that captures the essence of well-foundedness of least fixpoint unfoldings. These winning conditions form formal languages of \omega-words. We analyse which kinds of deterministic {\omega}-automata are needed in which case in order to recognise these languages. We then obtain a reduction to the problem of solving parity or Büchi games. The worst-case complexity of the obtained algorithms matches the known lower bounds for these logics. This approach provides a uniform, yet complexity-theoretically optimal treatment of satisfiability for branching-time temporal logics. It separates the use of temporal logic machinery from the use of automata thus preserving a syntactical relationship between the input formula and the object that represents satisfiability, i.e. a winning strategy in a parity or Büchi game. The games […]
6. Incarnation in Ludics and maximal cliques of paths
Ludics is a reconstruction of logic with interaction as a primitive notion, in the sense that the primary logical concepts are no more formulas and proofs but cut-elimination interpreted as an interaction between objects called designs. When the interaction between two designs goes well, such two designs are said to be orthogonal. A behaviour is a set of designs closed under bi-orthogonality. Logical formulas are then denoted by behaviours. Finally proofs are interpreted as designs satisfying particular properties. In that way, designs are more general than proofs and we may notice in particular that they are not typed objects. Incarnation is introduced by Girard in Ludics as a characterization of "useful" designs in a behaviour. The incarnation of a design is defined as its subdesign that is the smallest one in the behaviour ordered by inclusion. It is useful in particular because being "incarnated" is one of the conditions for a design to denote a proof of a formula. The computation of incarnation is important also as it gives a minimal denotation for a formula, and more generally for a behaviour. We give here a constructive way to capture the incarnation of the behaviour of a set of designs, without computing the behaviour itself. The method we follow uses an alternative definition of designs: rather than defining them as sets of chronicles, we consider them as sets of paths, a concept very close to that of play in game semantics that allows an easier […]
7. Implicit Resolution
Let \Omega be a set of unsatisfiable clauses, an implicit resolution refutation of \Omega is a circuit \beta with a resolution proof {\alpha} of the statement "\beta describes a correct tree-like resolution refutation of \Omega". We show that such system is p-equivalent to Extended Frege. More generally, let {\tau} be a tautology, a [P, Q]-proof of {\tau} is a pair (\alpha,\beta) s.t. \alpha is a P-proof of the statement "\beta is a circuit describing a correct Q-proof of \tau". We prove that [EF,P] \leq p [R,P] for arbitrary Cook-Reckhow proof system P.
8. Relation lifting, with an application to the many-valued cover modality
We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.
9. Polynomial Path Orders
This paper is concerned with the complexity analysis of constructor term rewrite systems and its ramification in implicit computational complexity. We introduce a path order with multiset status, the polynomial path order POP*, that is applicable in two related, but distinct contexts. On the one hand POP* induces polynomial innermost runtime complexity and hence may serve as a syntactic, and fully automatable, method to analyse the innermost runtime complexity of term rewrite systems. On the other hand POP* provides an order-theoretic characterisation of the polytime computable functions: the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP*.
10. Priced Timed Petri Nets
We consider priced timed Petri nets, i.e., unbounded Petri nets where each token carries a real-valued clock. Transition arcs are labeled with time intervals, which specify constraints on the ages of tokens. Furthermore, our cost model assigns token storage costs per time unit to places, and firing costs to transitions. This general model strictly subsumes both priced timed automata and unbounded priced Petri nets. We study the cost of computations that reach a given control-state. In general, a computation with minimal cost may not exist, due to strict inequalities in the time constraints. However, we show that the infimum of the costs to reach a given control-state is computable in the case where all place and transition costs are non-negative. On the other hand, if negative costs are allowed, then the question whether a given control-state is reachable with zero overall cost becomes undecidable. In fact, this negative result holds even in the simpler case of discrete time (i.e., integer-valued clocks).
11. All Linear-Time Congruences for Familiar Operators
The detailed behaviour of a system is often represented as a labelled transition system (LTS) and the abstract behaviour as a stuttering-insensitive semantic congruence. Numerous congruences have been presented in the literature. On the other hand, there have not been many results proving the absence of more congruences. This publication fully analyses the linear-time (in a well-defined sense) region with respect to action prefix, hiding, relational renaming, and parallel composition. It contains 40 congruences. They are built from the alphabet, two kinds of traces, two kinds of divergence traces, five kinds of failures, and four kinds of infinite traces. In the case of finite LTSs, infinite traces lose their role and the number of congruences drops to 20. The publication concentrates on the hardest and most novel part of the result, that is, proving the absence of more congruences.
12. Definability of linear equation systems over groups and rings
Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Moreover, we prove closure properties for classes of queries that reduce to solvability over rings, which provides normal forms for logics extended with solvability operators. We conclude by studying the extent to which fixed-point logic with counting can express problems in linear algebra over finite commutative rings, generalising known results on the logical definability of linear-algebraic problems over finite fields.
13. Avoiding Shared Clocks in Networks of Timed Automata
Networks of timed automata (NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks, i.e. transitions of one automaton may be guarded by conditions on the value of clocks reset by another automaton. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given an NTA A1 || A2 where A2 reads some clocks reset by A1, does there exist an NTA A'1 || A'2 without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only, in particular by copying the value of their neighbor's clocks. We discuss a formalization of the problem and define an appropriate behavioural equivalence. Then we give a criterion using the notion of contextual timed transition system, which represents the behavior of A2 when in parallel with A1. Finally, we effectively build A'1 || A'2 when it exists.
14. Products of effective topological spaces and a uniformly computable Tychonoff Theorem
This article is a fundamental study in computable analysis. In the framework of Type-2 effectivity, TTE, we investigate computability aspects on finite and infinite products of effective topological spaces. For obtaining uniform results we introduce natural multi-representations of the class of all effective topological spaces, of their points, of their subsets and of their compact subsets. We show that the binary, finite and countable product operations on effective topological spaces are computable. For spaces with non-empty base sets the factors can be retrieved from the products. We study computability of the product operations on points, on arbitrary subsets and on compact subsets. For the case of compact sets the results are uniformly computable versions of Tychonoff's Theorem (stating that every Cartesian product of compact spaces is compact) for both, the cover multi-representation and the "minimal cover" multi-representation.
15. Approximation systems for functions in topological and in metric spaces
A notable feature of the TTE approach to computability is the representation of the argument values and the corresponding function values by means of infinitistic names. Two ways to eliminate the using of such names in certain cases are indicated in the paper. The first one is intended for the case of topological spaces with selected indexed denumerable bases. Suppose a partial function is given from one such space into another one whose selected base has a recursively enumerable index set, and suppose that the intersection of base open sets in the first space is computable in the sense of Weihrauch-Grubba. Then the ordinary TTE computability of the function is characterized by the existence of an appropriate recursively enumerable relation between indices of base sets containing the argument value and indices of base sets containing the corresponding function value.This result can be regarded as an improvement of a result of Korovina and Kudinov. The second way is applicable to metric spaces with selected indexed denumerable dense subsets. If a partial function is given from one such space into another one, then, under a semi-computability assumption concerning these spaces, the ordinary TTE computability of the function is characterized by the existence of an appropriate recursively enumerable set of quadruples. Any of them consists of an index of element from the selected dense subset in the first space, a natural number encoding a rational bound for the distance between […]
16. Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems
Coalgebras in a Kleisli category yield a generic definition of trace semantics for various types of labelled transition systems. In this paper we apply this generic theory to generative probabilistic transition systems, short PTS, with arbitrary (possibly uncountable) state spaces. We consider the sub-probability monad and the probability monad (Giry monad) on the category of measurable spaces and measurable functions. Our main contribution is that the existence of a final coalgebra in the Kleisli category of these monads is closely connected to the measure-theoretic extension theorem for sigma-finite pre-measures. In fact, we obtain a practical definition of the trace measure for both finite and infinite traces of PTS that subsumes a well-known result for discrete probabilistic transition systems. Finally we consider two example systems with uncountable state spaces and apply our theory to calculate their trace measures.
17. Epistemic Updates on Algebras
We develop the mathematical theory of epistemic updates with the tools of duality theory. We focus on the Logic of Epistemic Actions and Knowledge (EAK), introduced by Baltag-Moss- Solecki, without the common knowledge operator. We dually characterize the product update construction of EAK as a certain construction transforming the complex algebras associated with the given model into the complex algebra associated with the updated model. This dual characterization naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). As an application of this dual characterization, we axiomatize the intuitionistic analogue of the logic of epistemic knowledge and actions, which we refer to as IEAK, prove soundness and completeness of IEAK w.r.t. both algebraic and relational models, and illustrate how IEAK encodes the reasoning of agents in a concrete epistemic scenario.
18. Expansions of MSO by cardinality relations
We study expansions of the Weak Monadic Second Order theory of (N,<) by cardinality relations, which are predicates R(X1,...,Xn) whose truth value depends only on the cardinality of the sets X1, ...,Xn. We first provide a (definable) criterion for definability of a cardinality relation in (N,<), and use it to prove that for every cardinality relation R which is not definable in (N,<), there exists a unary cardinality relation which is definable in (N,<,R) and not in (N,<). These results resemble Muchnik and Michaux-Villemaire theorems for Presburger Arithmetic. We prove then that + and x are definable in (N,<,R) for every cardinality relation R which is not definable in (N,<). This implies undecidability of the WMSO theory of (N,<,R). We also consider the related satisfiability problem for the class of finite orderings, namely the question whether an MSO sentence in the language {<,R} admits a finite model M where < is interpreted as a linear ordering, and R as the restriction of some (fixed) cardinality relation to the domain of M. We prove that this problem is undecidable for every cardinality relation R which is not definable in (N,<).
19. Compact manifolds with computable boundaries
We investigate conditions under which a co-computably enumerable closed set in a computable metric space is computable and prove that in each locally computable computable metric space each co-computably enumerable compact manifold with computable boundary is computable. In fact, we examine the notion of a semi-computable compact set and we prove a more general result: in any computable metric space each semi-computable compact manifold with computable boundary is computable. In particular, each semi-computable compact (boundaryless) manifold is computable.
20. Nominal Coalgebraic Data Types with Applications to Lambda Calculus
We investigate final coalgebras in nominal sets. This allows us to define types of infinite data with binding for which all constructions automatically respect alpha equivalence. We give applications to the infinitary lambda calculus.
21. Ordered Models of the Lambda Calculus
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not simultaneously satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of lambda calculus, by studying the connection between the notion of absolute unorderability in a specific point and a weaker notion of subtractivity (namely n-subtractivity) for partially ordered algebras. Finally we study the relation between n-subtractivity and relativized separation conditions in topological algebras, obtaining an incompleteness theorem for a general topological semantics of lambda calculus.
22. Modeling and Verification of Infinite Systems with Resources
We consider formal verification of recursive programs with resource consumption. We introduce prefix replacement systems with non-negative integer counters which can be incremented and reset to zero as a formal model for such programs. In these systems, we investigate bounds on the resource consumption for reachability questions. Motivated by this question, we introduce relational structures with resources and a quantitative first-order logic over these structures. We define resource automatic structures as a subclass of these structures and provide an effective method to compute the semantics of the logic on this subclass. Subsequently, we use this framework to solve the bounded reachability problem for resource prefix replacement systems. We achieve this result by extending the well-known saturation method to annotated prefix replacement systems. Finally, we provide a connection to the study of the logic cost-WMSO.
23. Handling Algebraic Effects
Algebraic effects are computational effects that can be represented by an equational theory whose operations produce the effects at hand. The free model of this theory induces the expected computational monad for the corresponding effect. Algebraic effects include exceptions, state, nondeterminism, interactive input/output, and time, and their combinations. Exception handling, however, has so far received no algebraic treatment. We present such a treatment, in which each handler yields a model of the theory for exceptions, and each handling construct yields the homomorphism induced by the universal property of the free model. We further generalise exception handlers to arbitrary algebraic effects. The resulting programming construct includes many previously unrelated examples from both theory and practice, including relabelling and restriction in Milner's CCS, timeout, rollback, and stream redirection.
24. Herbrand-Confluence
We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly normalizing. In this work we take a coarser (and mathematically more realistic) look at cut-free proofs. We analyze which witnesses they choose for which quantifiers, or in other words: we only consider the Herbrand-disjunction of a cut-free proof. Our main theorem is a confluence result for a natural class of proofs: all (possibly infinitely many) normal forms of the non-erasing reduction lead to the same Herbrand-disjunction.
25. Strong Turing Degrees for Additive BSS RAM's
For the additive real BSS machines using only constants 0 and 1 and order tests we consider the corresponding Turing reducibility and characterize some semi-decidable decision problems over the reals. In order to refine, step-by-step, a linear hierarchy of Turing degrees with respect to this model, we define several halting problems for classes of additive machines with different abilities and construct further suitable decision problems. In the construction we use methods of the classical recursion theory as well as techniques for proving bounds resulting from algebraic properties. In this way we extend a known hierarchy of problems below the halting problem for the additive machines using only equality tests and we present a further subhierarchy of semi-decidable problems between the halting problems for the additive machines using only equality tests and using order tests, respectively.
26. Undecidable First-Order Theories of Affine Geometries
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation \beta, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,\beta) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of the class of expansions of (R^2,\beta) with just one unary predicate is not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,\beta), and show that for each structure (T,\beta) in C, the FO-theory of the class of expansions of (T,\beta) with a single unary predicate is undecidable. We then consider classes of expansions of structures (T,\beta) with a restricted unary predicate, for example a finite predicate, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivities of universal MSO and weak universal MSO over expansions of (R^n,\beta). While the logics are incomparable in general, over expansions of (R^n,\beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO.