We present a logic-based framework for the specification and validation of distributed protocols. Our specification language is a logic-based presentation of update rules for arbitrary graphs. Update rules are specified via conditional rewriting rules defined over a relational language. We focus our attention on unary and binary relations as a way to specify predicates over nodes and edges of a graph. For the considered language, we define assertions that can be applied to specify correctness properties for arbitrary configurations. We apply the language to model the distributed version of the Dining Philosopher Protocol. The protocol is defined for asynchronous processes distributed over a graph with arbitrary topology. We propose then validation methods based on source to source transformations and deductive reasoning. We apply the resulting method to provide a succint correctness proof of the considered case-study.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this paper, we extend existing results about simulation and intrinsic universality in a model of tile-based self-assembly. Namely, we work within the 2-Handed Assembly Model (2HAM), which is a model of self-assembly in which assemblies are formed by square tiles that are allowed to combine, using glues along their edges, individually or as pairs of arbitrarily large assemblies in a hierarchical manner, and we explore the abilities of these systems to simulate each other when the simulating systems have a higher "temperature" parameter, which is a system wide threshold dictating how many glue bonds must be formed between two assemblies to allow them to combine. It has previously been shown that systems with lower temperatures cannot simulate arbitrary systems with higher temperatures, and also that systems at some higher temperatures can simulate those at particular lower temperatures, creating an infinite set of infinite hierarchies of 2HAM systems with strictly increasing simulation power within each hierarchy. These previous results relied on two different definitions of simulation, one (strong simulation) seemingly more restrictive than the other (standard simulation), but which have previously not been proven to be distinct. Here we prove distinctions between them by first fully characterizing the set of pairs of temperatures such that the high temperature systems are intrinsically universal for the lower temperature systems (i.e. one tile set at the higher temperature can simulate any at the lower) using strong simulation. This includes the first impossibility result for simulation downward in temperature. We then show that lower temperature systems which cannot be simulated by higher temperature systems using the strong definition, can in fact be simulated using the standard definition, proving the distinction between the types of simulation.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.