检索结果-内蒙古大学图书馆

A well-structured framework for analysing petri net extensions

INFORMATION AND computation 2004年第1-2期195卷 1-29页

作者： Finkel, A McKenzie, P Picaronny, C Ecole Normale Super CNRS URA 8643 Lab Specificat & Verificat F-94235 Cachan France Univ Montreal Montreal PQ H3C 3J7 Canada

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.

关键词： lopic and verification of computer program theory of parallel and distributed computation algorithms decidability

来源：评论

学校读者我要写书评

暂无评论

Relating communicating processes with different interfaces

引用

FUNDAMENTA INFORMATICAE 2004年第1期59卷 1-37页

作者： Burton, J Koutny, M Pappalardo, G Newcastle Univ Sch Comp Sci Newcastle Upon Tyne NE1 7RU Tyne & Wear England Univ Catania Dipartimento Matemat & Informat I-95125 Catania Italy

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.

关键词： theory of parallel and distributed computation behaviour abstraction refinement communicating sequential processes compositionality verification

来源：评论

学校读者我要写书评

暂无评论

Implementing communicating processes in the event of interface difference 2

Implementing communicating processes in the event of interfa...

引用

2nd International Conference on Application of Concurrency to System Design (ACSD 2001)

作者： Burton, J Koutny, M Pappalardo, G Newcastle Univ Dept Comp Sci Newcastle Upon Tyne NE1 7RU Tyne & Wear England

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.

关键词： theory of parallel and distributed computation behaviour abstraction refinement communicating sequential processes compositionality

来源：评论

学校读者我要写书评

暂无评论

Behaviour abstraction for communicating sequential processes

引用

FUNDAMENTA INFORMATICAE 2001年第1期48卷 21-54页

作者： Koutny, M Pappalardo, G Newcastle Univ Dept Comp Sci Newcastle Upon Tyne NE1 7RU Tyne & Wear England Univ Catania Dipartimento Matemat & Informat I-95125 Catania Italy

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.

关键词： theory of parallel and distributed computation behaviour abstraction communicating sequential processes compositionality

来源：评论

学校读者我要写书评

暂无评论

A model of behaviour abstraction for communicating processes 16th

A model of behaviour abstraction for communicating processes

引用

16th Annual Symposium on Theoretical Aspects of Computer Science

作者： Koutny, M Pappalardo, G Univ Newcastle Upon Tyne Dept Comp Sci Newcastle Upon Tyne NE1 7RU Tyne & Wear England Univ Catania Dipartmento Matemat I-95125 Catania Italy

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.

关键词： theory of parallel and distributed computation behaviour abstraction communicating sequential processes

来源：评论

学校读者我要写书评

暂无评论

Generalized synchronization languages 12th

引用

12th International Symposium on Fundamental of computation theory

作者： Ryl, I Roos, Y Clerbout, M Univ Lille 1 CNRS URA 369 LIFL F-59655 Villeneuve Dascq France

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.

关键词： automata and formal languages theory of parallel and distributed computation

来源：评论

学校读者我要写书评

暂无评论

Partial characterizations of networks supporting shortest path interval labeling schemes

引用

NETWORKS 1998年第2期32卷 103-113页

作者： Narayanan, L Shende, S Concordia Univ Dept Comp Sci Montreal PQ H3G 1M8 Canada Univ Nebraska Dept Comp Sci & Engn Lincoln NE 68588 USA

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.

关键词： theory of parallel and distributed computation interval routing algorithms graph theory

来源：评论

学校读者我要写书评

暂无评论

A (non-elementary) modular decision procedure for LTrL

A (non-elementary) modular decision procedure for LTrL

引用

23rd International Symposium on the Mathematical Foundations of Computer Science (MFCS 98)

作者： Gastin, P Meyer, R Petit, A Univ Paris 07 LIAFA F-75251 Paris 05 France ENS Cachan LSV URA 2236 F-94235 Cachan France

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.

关键词： Topics logic in computer science automata and formal languages theory of parallel and distributed computation model checking

来源：评论

学校读者我要写书评

暂无评论

Expressive completeness of LTrL on finite traces: An algebraic proof

引用

15th Annual Symposium on Theoretical Aspects of Computer Science (STACS 98)

作者： Meyer, R Petit, A ENS CNRS URA 2236 LSV F-94235 Cachan France

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.

关键词： Topics logic in computer science automata and formal languages theory of parallel and distributed computation

来源：评论

学校读者我要写书评

暂无评论

Routing on Triangles, Tori and Honeycombs

引用

International Journal of Foundations of Computer Science 1997年第3期8卷 269-287页

作者： Jop F. Sibeyn Max-Planck-Institut für Informatik Im Stadtwald 66123 Saarbrücken Germany

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.

关键词： theory of parallel and distributed computation VLSI structures parallel algorithms

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：