23924378
A switched delay line based optical switch architecture with a bypass line
This paper proposes a new switching architecture to be used in all-optical networks. The proposed switch, M-B-Quadro switch, is extended from an original 2/spl times/2 two-stage multi-buffer switched delay line based optical switching node, known as M-Quadro node. By incorporating bypass lines and employing a novel switch control strategy, denoted as LAVS, the switching node can effectively resolve packet contentions, thus reducing the packet deflection probability substantially.
1232058
CORNet: A Scalable and Bandwidth-Efficient Optical Burst Switching Ring Architecture for Metro Area Networks
The rapid evolution of networks has been driven by new advances in enabling technologies and the explosive growth of Internet traffic. optical burst switching (OBS) is not only cost-effective, but also provides high throughput, high bandwidth utilization, and low transmission latency. These benefits make OBS a viable solution for next-generation metro area networks (MANs) in which the traffic models are changed more dramatically than today's networks. Based on wavelength division multiplexing (WDM) technology, this study presents a loss-free optical burst switching metro ring architecture, designated the collision-free optic-burst ring network (CORNet). The proposed architecture ensures a collision-free transmission of data bursts, while retaining the advantage of the statistical multiplexing provided by conventional OBS networks. The simulation results confirm the effectiveness of the proposed CORNet architecture
359393
PAM: A Process Algebra Manipulator
PAM is a general proof tool for process algebras. It allows users to define their own calculi and then perform algebraic style proofs in these calculi by directly manipulating process terms. The logic that PAM implements is equational logic plus recursion, with some features tailored to the particular requirements of process algebras. Equational reasoning is implemented by rewriting, while recursion is dealt with by induction. Proofs are constructed interactively, giving users the freedom to control the proof processes.
18855634
Symbolic Transition Graph with Assignment
A new model for message-passing processes is proposed which generalizes the notion of symbolic transition graph as introduced in [HL95], by allowing assignments to be carried in transitions. The main advantage of this generalization is that a wider class of processes can be represented as finite state graphs. Two kinds of operational semantics, ground and symbolic, are given to such graphs. On top of them both ground and symbolic bisimulations are defined and are shown to agree with each other. An algorithm is also presented which computes bisimulation formulae for finite state symbolic transition graphs with assignments, in terms of the greatest solutions of predicate equation systems.
37655914
Unique Fixpoint Induction for Mobile Processes
Complete proof systems for bisimulation equivalences in the π-calculus with recursion are presented. The key inference rule dealing with recursion is unique fixpoint induction which generalises that used in [Mil84] for regular pure-CCS. It is shown that the proof systems are sound, and also complete when restricted to the subset of π-calculus where recursions are guarded and the parallel composition is disallowed. These results on the one hand extend the proof systems for recursion-free π-calculus in [Lin94, Lin95] to infinite processes, on the other hand extend the inference system for guarded regular pure-CCS of [Mil84] to π-calculus.
208092
Axiomatising timed automata
Abstract. Timed automata has been developed as a basic semantic model for real time systems. Its algorithmic aspects for automated analysis have been well studied. But so far there is still no satisfactory algebraic theory to allow the derivation of semantical equivalence of automata by purely syntactical manipulation. The aim of this paper is to provide such a theory. We present an inference system of timed bisimulation equivalence for timed automata based on a CCS-style regular language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgments of the proof system are conditional equations of the form 
$\phi \rhd t = u$ where 
$\phi$ is a clock constraint and t,u are terms denoting timed automata. The inference system is shown to be sound and complete for timed bisimulation. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value–passing processes.
38630140
Proof Systems for Message-Passing Process Algebras
We give sound and complete proof systems for a variety of bisimulation based equivalences over a message-passing process algebra. The process algebra is a generalisation of CCS where the actions consist of receiving and sending messages or data on communication channels; the standard prefixing operator a.p is replaced by the two operators c?x.p and c!e.p and in addition messages can be tested by a conditional construct. The various proof systems are parameterised on auxiliary proof systems for deciding on equalities or more general boolean identities over the expression language for data. The completeness of these proof systems are thus relative to the completeness of the auxiliary proof systems.