computational RFID (CRFID) devices are emerging platforms that can enable perennial computation and sensing by eliminating the need for batteries. Although much research has been devoted to improving upstream (CRFID t...
ISBN:
(纸本)9781467399531
computational RFID (CRFID) devices are emerging platforms that can enable perennial computation and sensing by eliminating the need for batteries. Although much research has been devoted to improving upstream (CRFID to RFID reader) communication rates, the opposite direction has so far been neglected, presumably due to the difficulty of guaranteeing fast and error-free transfer amidst frequent power interruptions of CRFID. With growing interest in the market where CRFIDs are forever-embedded in many structures, it is necessary for this void to be filled. therefore, we propose Wisent-a robust downstream communication protocol for CRFIDs that operates on top of the legacy UHF RFID communication protocol: EPC C1G2. the novelty of Wisent is its ability to adaptively change the frame length sent by the reader, based on the lengththrottling mechanism, to minimize the transfer times at varying channel conditions. We present an implementation of Wisent for the WISP 5 and an off-the-shelf RFID reader. Our experiments show that Wisent allows transfer up to 16 times faster than a baseline, non-adaptive shortest frame case, i.e. single word length, at sub-meter distance. As a case study, we show how Wisent enables wireless CRFID reprogramming, demonstrating the world's first wirelessly reprogrammable (software defined) CRFID.
Differential dataflow is a recent approach to incremental computationthat relies on a partially ordered set of differences. In the present paper, we aim to develop its foundations. We define a small programming langu...
详细信息
ISBN:
(纸本)9783662466780;9783662466773
Differential dataflow is a recent approach to incremental computationthat relies on a partially ordered set of differences. In the present paper, we aim to develop its foundations. We define a small programming language whose types are abelian groups equipped with linear inverses, and provide both a standard and a differential denotational semantics. the two semantics coincide in that the differential semantics is the differential of the standard one. Mobius inversion, a well-known idea from combinatorics, permits a systematic treatment of various operators and constructs.
the sensitivity conjecture of Nisan and Szegedy [CC'94] asks whether for any Boolean function f, the maximum sensitivity s(f), is polynomially related to its block sensitivity bs(f), and hence to other major compl...
详细信息
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order pro...
详细信息
ISBN:
(纸本)9783662466780;9783662466773
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order programming language with impredicative polymorphism and recursive types. We show that the resulting logical relation is sound and complete with respect to the contextual preorder and, moreover, that it is convenient for reasoning about concrete program equivalences. Finally, we extend the language with dynamically allocated first-order references and show how to extend the logical relation to this language. We show that the resulting relation remains useful for reasoning about examples involving both state and probabilistic choice.
Mean-payoff games play a central role in quantitative synthesis and verification. In a single-dimensional game a weight is assigned to every transition and the objective of the protagonist is to assure a non-negative ...
详细信息
ISBN:
(纸本)9783662466780;9783662466773
Mean-payoff games play a central role in quantitative synthesis and verification. In a single-dimensional game a weight is assigned to every transition and the objective of the protagonist is to assure a non-negative limit-average weight. In the multidimensional setting, a weight vector is assigned to every transition and the objective of the protagonist is to satisfy a boolean condition over the limit-average weight of each dimension, e.g., LimAvg(xi) < 0 V LimAvg(x2) >= 0 A LimAvg(x3) >= 0. We recently proved that when one of the players is restricted to finite-memory strategies then the decidability of determining the winner is inter-reducible with Hilbert's Tenth problem over rationals (a fundamental long-standing open problem). In this work we consider arbitrary (infinite-memory) strategies for both players and show that the problem is undecidable.
the call-by-value language RML may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct in the sense of Reynolds. We consider the fragment of...
详细信息
ISBN:
(纸本)9783662466780;9783662466773
the call-by-value language RML may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct in the sense of Reynolds. We consider the fragment of (finitary) RML terms of order at most 1 with free variables of order at most 2, and identify two subfragments of this for which we show observational equivalence to be Sit decidable. the first subfragment, RMLr P211 consists of those terms in which the P-pointers in the game semantic representation are determined by the underlying sequence of moves. the second subfragment consists of terms in which the 0-pointers of moves corresponding to free variables in the game semantic representation are determined by the underlying moves. these results are shown using a reduction to a form of automata over data words in which the data values have a tree-structure, reflecting the tree-structure of the threads in the game semantic plays. In addition we show that observational equivalence is undecidable at every third- or higher-order type, every second-order type which takes at least two firstorder arguments, and every second-order type (of arity greater than one) that has a first-order argument which is not the final argument.
We compare three notions of knowledge in concurrent system: memoryless knowledge, knowledge of perfect recall, and causal knowledge. Memoryless knowledge is based only on the current state of a process, knowledge of p...
详细信息
We consider two-player reachability games with additional resource counters on arenas that are induced by the configuration graphs of pushdown systems. For a play, we define the resource cost to be the highest occurri...
详细信息
ISBN:
(纸本)9783642548307;9783642548291
We consider two-player reachability games with additional resource counters on arenas that are induced by the configuration graphs of pushdown systems. For a play, we define the resource cost to be the highest occurring counter value. In this way, we quantify resources and memory that player 0 needs to win. We introduce the bounded winning problem: Is there a uniform bound k such that player 0 can win the game from a set of initial configurations withthis bound k? We provide an effective, saturation-based method to solve this problem for regular sets of initial and goal configurations.
We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and exis...
详细信息
ISBN:
(纸本)9783642548307;9783642548291
We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and ExPTIME-hard in a fragment recently shown to be decidable by Iosif et al. Moreover, entailment in the base language is Pi(P)(2)-complete, the upper bound even holds in the presence of list predicates. We additionally show that entailment in essentially any fragment of Separation Logic allowing for general inductive predicates is intractable even when strong syntactic restrictions are imposed.
In this paper, we consider multi-dimensional maximal costbounded reachability probability over continuous-time Markov decision processes (CTMDPs). Our major contributions are as follows. Firstly, we derive an integral...
详细信息
ISBN:
(纸本)9783642548307;9783642548291
In this paper, we consider multi-dimensional maximal costbounded reachability probability over continuous-time Markov decision processes (CTMDPs). Our major contributions are as follows. Firstly, we derive an integral characterization which states that the maximal cost-bounded reachability probability function is the least fixed-point of a system of integral equations. Secondly, we prove that the maximal cost-bounded reachability probability can be attained by a measurable deterministic cost-positional scheduler. thirdly, we provide a numerical approximation algorithm for maximal cost-bounded reachability probability. We present these results under the setting of both early and late schedulers. Besides, we correct a fundamental proof error in the PhD thesis by Martin Neuhaufier on maximal time-bounded reachability probability by completely new proofs for the more general case of multi-dimensional maximal cost-bounded reachability probability.
暂无评论