Transition systems defined from recursive functions N-P --> N-P are introduced and named WSNs. or well-structured nets. Such nets sit conveniently between Petri net extensions and general transition systems. In the...
详细信息
Transition systems defined from recursive functions N-P --> N-P are introduced and named WSNs. or well-structured nets. Such nets sit conveniently between Petri net extensions and general transition systems. In the first part of this paper, we study decidability properties of WSN classes obtained by imposing natural restrictions on their defining functions, with respect to termination, coverability. and four variants of the boundedness problem. We are able to precisely answer almost all the questions which arise. thus gaining much insight into old and new generalized Petri net decidability results. In the second part. we specialize our analysis to WSNs defined from affine functions, which elegantly encompass most Petri net extensions studied in the literature. Again, we study decidability properties of natural classes of affine WSN with respect to the above six computational problems. In particular, we develop an algorithm computing limits of iterated nonnegative affine functions, in order to decide the path-place variant of the boundedness problem for non-negative affine WSN. (C) 2004 Published by Elsevier Inc.
We present here an implementation relation intended to formalise the notion that a system built of communicating processes is an acceptable implementation of another base, or target, system in the event that the two s...
详细信息
We present here an implementation relation intended to formalise the notion that a system built of communicating processes is an acceptable implementation of another base, or target, system in the event that the two systems have different interfaces. Such a treatment has clear applicability in the software development process, where (the interface of) an implementation component may be expressed at a different level of abstraction to (the interface of) the relevant specification component. Technically, processes are formalised using Hoare's CSP language, with its standard failures-divergences model. The implementation relation is formulated in terms of failures and divergences of the implementation and target processes. Interface difference is modelled by endowing the implementation relation with parameters called extraction patterns. These are intended to interpret implementation behaviour as target behaviour, and suitably constrain the former in connection to well-formedness and deadlock properties. We extend the results of our previous work and replace implementation relations previously presented by a single, improved scheme. We also remove all the restrictions previously placed upon target processes. Two basic kinds of results are obtained: realisability and compositionality. The latter means that a target composed of several connected systems may be implemented by connecting their respective implementations. The former means that, if target and implementation in fact have the same interface, then the implementation relation they should satisfy collapses into standard implementation pre-order. We also show how to represent processes and extraction patterns in a manner amenable to computer implementation, and detail a graph-theoretic restatement of the conditions defining the implementation relation, from which algorithms for their automatic verification are easily derived.
We present here an implementation relation which formalises the notion that a system built of communicating processes is an acceptable implementation of another base or specification system in the event that the two s...
详细信息
ISBN:
(纸本)076951071X
We present here an implementation relation which formalises the notion that a system built of communicating processes is an acceptable implementation of another base or specification system in the event that the two systems have different interfaces. Such a treatment has obvious applicability to the software development process, where an implementation component may be expressed at a different level of abstraction to the relevant specification component. We extend the results of our previous work and combine into a single scheme implementation relations previously presented. We also relax the restrictions previously placed upon specification processes. Using this new implementation relation, two basic kinds of results are obtained: realisability and compositionality. The former ensures that an implementation, when plugged into an appropriate environment, should yield a conventional implementation of the specification, and also that the implementation relation is acceptable when used in the event that specification and implementation systems have the same interfaces. The latter requires that a specification composed of several connected system may be implentented by connecting their respective implementations.
We investigate the notion that a system is an acceptable implementation of another base or target system, in the case that the two systems (or processes) have different interfaces. For instance, the base processes can...
详细信息
We investigate the notion that a system is an acceptable implementation of another base or target system, in the case that the two systems (or processes) have different interfaces. For instance, the base processes can be thought of as specifications, or ideal processes operating in an error-free environment, while the implementations model their actual realisations, operating in an error-prone environment and possibly employing a variety of fault-tolerant techniques. Using the CSP model, we relate implementations and base systems in terms of their observable behaviours. We obtain two fundamental results, viz. realisability and compositionality. The former ensures that implementations may be put to good use, while the latter guarantees that a target composed of several connected subsystems may be implemented by connecting their respective implementations.
We investigate the notion that a system, or process, is an acceptable implementation of another base or target process, in the case that they have different interfaces. Base processes can be thought of as specificatio...
详细信息
ISBN:
(纸本)354065691X
We investigate the notion that a system, or process, is an acceptable implementation of another base or target process, in the case that they have different interfaces. Base processes can be thought of as specifications, or ideal processes operating in an error-free environment, while implementations model their actual realisation, possibly employing a variety of fault-tolerant techniques. Using the CSP model, we relate implementations to targets in terms of their observable behaviours, through interface abstraction. We obtain two basic results: realisability and compositionality. The former ensures an implementation up to interface abstraction can be put to good use, in the sense that plugging it into an appropriate environment yields a conventional implementation. Compositionality requires that a target made up of subcomponents can be implemented by assembling their respective implementations.
Generalized synchronization languages are a model used to describe the behaviors of distributed applications whose synchronization constraints are expressed by generalized synchronization expressions an extension of s...
详细信息
ISBN:
(纸本)3540664122
Generalized synchronization languages are a model used to describe the behaviors of distributed applications whose synchronization constraints are expressed by generalized synchronization expressions an extension of synchronization expressions. Generalized synchronization languages were conjectured by Salomaa and Yu to be characterized by a semi-commutation. We show that this semi-commutation characterizes the images of generalized synchronization languages by a morphism-like class of rational functions.
In this paper, we consider the problem of shortest path interval routing, a space-efficient strategy for routing in distributed networks. In this scheme, an ordering of the vertices is chosen so that the edges of the ...
详细信息
In this paper, we consider the problem of shortest path interval routing, a space-efficient strategy for routing in distributed networks. In this scheme, an ordering of the vertices is chosen so that the edges of the network can be labeled with one or more subintervals of the vertex ordering: The resulting routing tables must be deterministic and route along shortest paths between all pairs of vertices. We first show constructively that any interval graph can be labeled with one circular subinterval on each edge;this extends a known result for proper interval graphs. We also provide a partial characterization for networks that admit linear interval routing when edges are labeled with exactly one interval, in terms of the biconnected components of any such network. This is the first such characterization when the paths are required to be shortest paths under the distance metric. Finally, we show that the class of networks that can be labeled with k greater than or equal to 1 subintervals per edge is closed under composition with a certain class of graphs. (C) 1998 John Wiley & Sons, Inc.
Thiagarajan and Walukiewicz [18] have defined a temporal logic LTrL on Mazurkiewice traces, patterned on the famous propositional temporal logic of linear time LTL defined by Pnueli. They have shown that this logic is...
详细信息
ISBN:
(纸本)3540648275
Thiagarajan and Walukiewicz [18] have defined a temporal logic LTrL on Mazurkiewice traces, patterned on the famous propositional temporal logic of linear time LTL defined by Pnueli. They have shown that this logic is equal in expressive power to the first order theory of finite and infinite traces. The hopes to get an "easy" decision procedure for LTrL, as it is the case for LTL, vanished very recently due to a result of Walukiewicz [19] who showed that the decision procedure for LTrL is non-elementary. However, tools like Mona [8] or Mosel [7] show that it is possible to handle non-elementary logics on significant examples. Therefore, it appears worthwhile to have a direct decision procedure for LTrL;in this paper we propose such a decision procedure, in a modular way. Since the logic LTrL is not pure future, our algorithm constructs by induction a finite family of Buchi automata for each LTrL-formula. As expected by the results of [19], the main difficulty comes from the "Until" operator.
Very recently a new temporal logic, for Mazurkiewicz traces, denoted LTrL, has been defined by Thiagarajan and Walukiewicz [15]. They have shown that this logic is equal in expressive power to the first order theory o...
详细信息
ISBN:
(纸本)3540642307
Very recently a new temporal logic, for Mazurkiewicz traces, denoted LTrL, has been defined by Thiagarajan and Walukiewicz [15]. They have shown that this logic is equal in expressive power to the first order theory of finite and infinite traces thus filling a prominent gap in the theory. We propose in this paper a entirely new, algebraic, proof of this result in the case of finite traces only. Our proof generalizes Cohen, Perrin and Pin's work on finite sequences [2], using as a basic tool a new extension of the wreath product principle on traces [7]. As a major consequence of our proof we show that, when dealing with finite traces only, no past modality is necessary to obtain a expressively complete logic. Precisely, we prove that the logic LTrLred, obtained from LTrL by not using the past modularity, has the same expressive power as the first order theory on finite traces.
The standard n × n torus consists of two sets of axes: horizontal and vertical ones. For routing h-relations, the bisection bound gives a lower bound of h · n/4. Several algorithms nearly matching this bound...
详细信息
The standard n × n torus consists of two sets of axes: horizontal and vertical ones. For routing h-relations, the bisection bound gives a lower bound of h · n/4. Several algorithms nearly matching this bound have been given. In this paper we analyze the routing capacity of modified tori: tessellations of the plane with triangles or hexagons and tori with added diagonals. On some of these networks the ratio of routing capacity and degree is higher than for ordinary tori, even though they are as easily constructed. Hence, they may constitute more cost effective alternatives. For networks with n 2 PUs, we get the following results: on a torus of hexagons, node degree 3, h-relations are performed in 0.37 · h · n steps; on a torus of triangles, node degree 6, in 0.13 · h · n; and on a torus with added diagonals, node degree 8, in h · n/12. The latter result matches the bisection bound for this network. Even faster is the routing on a torus of hexagons with diagonals, node degree 12: 0.053 · h · n. The algorithms are simple, inspired by the algorithm of Valiant and Brebner. The results can easily be extended to sorting, dynamic routing or routing for average-case inputs.
暂无评论