We present an explicitly typed lambda calculus "a la Church" based on the union and intersection types discipline;this system is the counterpart of the standard type assignment calculus "a la Curry.&quo...
详细信息
ISBN:
(纸本)9783642175107
We present an explicitly typed lambda calculus "a la Church" based on the union and intersection types discipline;this system is the counterpart of the standard type assignment calculus "a la Curry." Our typed calculus enjoys the Subject Reduction and Church-Rosser properties, and typed terms are strongly normalizing when the universal type is omitted. Moreover both type checking and type reconstruction are decidable. In contrast to other typed calculi, a system with union types will fail to be "coherent" in the sense of Tannen, Coquand, Gunter, and Scedrov: different proofs of the same typing judgment will not necessarily have the same meaning. In response, we introduce a decidable notion of equality on type-assignment derivations inspired by the equational theory of bicartesian-closed categories.
By Courcelle's theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. this result was extended to counting pr...
详细信息
ISBN:
(纸本)9783642175107
By Courcelle's theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. this result was extended to counting problems by Arnborg et al. and to enumeration problems by Flum et al. Despite the undisputed importance of these results for proving fixed-parameter tractability, they do not directly yield implementable algorithms. Recently, Gottlob et al. presented a new approach using monadic datalog to close the gap between theoretical tractability and practical computability for MSO-definable decision problems. In the current work we show how counting and enumeration problems can be tackled by an appropriate extension of the datalog approach.
In the celebrated Godel Prize winning papers, Herlihy, Shavit, Saks and Zaharoglou gave topological characterization of waitfree computation. In this paper, we characterize waitfree communication logically. First, we ...
详细信息
ISBN:
(纸本)9783642175107
In the celebrated Godel Prize winning papers, Herlihy, Shavit, Saks and Zaharoglou gave topological characterization of waitfree computation. In this paper, we characterize waitfree communication logically. First, we give an intuitionistic epistemic logic K boolean OR for asynchronous communication. the semantics for the logic K boolean OR is an abstraction of Herlihy and Shavit's topological model. In the same way Kripke model for intuitionistic logic informally describes an agent increasing its knowledge over time, the semantics of K boolean OR describes multiple agents passing proofs around and developing their knowledge together. On top of the logic K boolean OR, we give an axiom type that characterizes sequential consistency on shared memory. the advantage of intuitionistic logic over classical logicthen becomes apparent as the axioms for sequential consistency are meaning less for classical logic because they are classical tautologies. the axioms are similar to the axiom type for prelinearity (phi superset of psi) boolean OR (psi superset of phi). this similarity reflects the analogy between sequential consistency for shared memory scheduling and linearity for Kripke frames: both require total order on schedules or models. Finally, under sequential consistency, we give soundness and completeness between a set of logical formulas called waitfree assertions and a set of models called waitfree schedule models.
Constraints shield solutions from a problem solver. However, in the hands of trained constraint problem solvers, the same constraints that create the problems in the first place can also guide problem solvers to solut...
详细信息
Feature modeling has been found very effective for modeling and managing variability in Software Product Lines. the nature of feature models invites, sometimes even requires, the use of global constraints. this paper ...
详细信息
ISBN:
(纸本)9783642153952
Feature modeling has been found very effective for modeling and managing variability in Software Product Lines. the nature of feature models invites, sometimes even requires, the use of global constraints. this paper lays the groundwork for the inclusion of global constraints in automated reasoning on feature models. We present a mapping from extended feature models to constraint logicprogramming over finite domains, and show that this mapping enables using global constraints on feature attributes, as well as features, for a variety of analysis operations on feature models. We also present performance test results and discuss the benefits of using global constraints.
the proceedings contain 49 papers. the topics discussed include: constraint-directed search in computational finance and economics;constraints, graphs, algebra, logic, and complexity;testing expressibility is hard;app...
ISBN:
(纸本)364215395X
the proceedings contain 49 papers. the topics discussed include: constraint-directed search in computational finance and economics;constraints, graphs, algebra, logic, and complexity;testing expressibility is hard;applying constraint programming to identification and assignment of service professionals;computing the density of states of Boolean formulas;towards parallel non serial dynamic programming for solving hard weighted CSP;making adaptive an interval constraint propagation algorithm exploiting monotonicity;checking-up on branch-and-check;spatial, temporal, and hybrid decompositions for large-scale vehicle routing with time windows;propagating the bin packing constraint using linear programming;sweeping with continuous domains;a new hybrid tractable class of soft constraint problems;a propagator for maximum weight string alignment with arbitrary pairwise dependencies;and generating special-purpose stateless propagators for arbitrary constraints.
In this paper we introduce an extension of propositional logicthat allows clauses to be weighted with values from a generic semiring. the main interest of this extension is that different instantiations of the semiri...
详细信息
ISBN:
(纸本)9783642175107
In this paper we introduce an extension of propositional logicthat allows clauses to be weighted with values from a generic semiring. the main interest of this extension is that different instantiations of the semiring model different interesting computational problems such as finding a model, counting the number of models, finding the best model with respect to an objective function, finding the best model with respect to several independent objective functions, or finding the set of pareto-optimal models with respect to several objective functions. then we show that this framework unifies several solving techniques and, even more importantly, rephrases them from an algorithmic language to a logical language. As a result, several solving techniques can be trivially and elegantly transferred from one computational problem to another. As an example, we extend the basic DPLL algorithm to our framework producing an algorithm that we call SDPLL. then we enhance the basic SDPLL in order to incorporate the three features that are common in all modern SAT solvers: backjumping, learning and restarts. As a result, we obtain an extremely simple algorithm that captures, unifies and extends in a well-defined logical language several techniques that are valid for arbitrary semirings.
interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal mu-calculus, whic...
详细信息
ISBN:
(纸本)9783642175107
interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal mu-calculus, which is the basis for abstract model checking. the abstract semantic function is constructed directly from the standard concrete semantics together with a Galois connection between the concrete state-space and an abstract domain. there is no need for mixed or modal transition systems to abstract arbitrary temporal properties, as in previous work in the area of abstract model checking. Using the modal mu-calculus to implement CTL, the abstract semantics gives an over-approximation of the set of states in which an arbitrary CTL formula holds. then we show that this leads directly to an effective implementation of an abstract model checking algorithm for CTL using abstract domains based on linear constraints. the implementation of the abstract semantic function makes use of an SMT solver. We describe an implemented system for proving properties of linear hybrid automata and give some experimental results.
Graded modalities enrich the universal and existential quantifiers withthe capability to express the concept of at least k or all but k, for a non-negative integer k. Recently, temporal logics such as mu-calculus and...
详细信息
ISBN:
(纸本)9783642175107
Graded modalities enrich the universal and existential quantifiers withthe capability to express the concept of at least k or all but k, for a non-negative integer k. Recently, temporal logics such as mu-calculus and Computational Tree logic, CTL, augmented with graded modalities have received attention from the scientific community, both from a theoretical side and from an applicative perspective. Both mu-calculus and CTL naturally apply as specification languages for closed systems: in this paper, we add graded modalities to the Alternating-time Temporal logic (ATL) introduced by Alur et al., to study how these modalities may affect specification languages for open systems. We present, and compare with each other, three different semantics. We first consider a natural interpretation which seems suitable to off-line synthesis applications and then we restrict it to the case where players can only employ memoryless strategies. Finally, we strengthen the logic by means of a different interpretation which may find application in the verification of fault-tolerant controllers. For all the interpretations, we efficiently solve the model-checking problem both in the concurrent and turn-based settings, proving its PTIME-completeness. To this aim we also exploit also a characterization of the maximum grading value of a given formula.
the theory BV of bit-vectors, i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, is becoming very popular in formal verification. Standard solvers for this theory are based on a bit-...
详细信息
ISBN:
(纸本)9783642120015
the theory BV of bit-vectors, i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, is becoming very popular in formal verification. Standard solvers for this theory are based on a bit-level encoding into propositional logic and SAT-based resolution techniques. In this paper, we investigate an alternative approach based on a word-level encoding into bounded arithmetic and Constraint logicprogramming (CLP) resolution techniques. We define an original CLP framework (domains and propagators) dedicated to bit-vector constraints. this framework is implemented in a prototype and thorough experimental studies have been conducted. the new approach is shown to perform much better than standard CLP-based approaches, and to considerably reduce the gap withthe best SAT-based BV solvers.
暂无评论