Step bisimulation is pomset equivalence on a parallel language without explicit internal choice

1993 ◽  
Vol 3 (1) ◽  
pp. 25-62 ◽  
Author(s):  
Douglas R. Troeger
Keyword(s):  
Equivalence Classes ◽  
Binary Choice ◽  
Parallel Composition ◽  
Focus Attention ◽  
Semantic Level ◽  
Parallel Language ◽  
Bisimulation Equivalence ◽  
Local Nondeterminism ◽  
Trace Equivalence ◽  
Single Set

We focus attention on a language ℒ generated by a set of elementary actions under operations of sequential composition, external binary choice, iteration, and non-nested disjoint parallel composition: that is, on an especially simple parallel language without explicit internal, or ‘local’, nondeterminism. ℒ is nondeterministic, despite the restriction to external choice, since a given action may occur in both subterms F and G of the parallel composition F ║ G. We exhibit a single set of equations that axiomatizes both step bisimulation and pomset equivalence on ℒ Given that step bisimulation and pomset equivalence are incomparable on the language ℒ+ obtained from ℒ by relaxing just the constraint on choice, the coincidence of these equivalences on ℒ suggests that the elimination of explicit internal choice can result in simplifications at the semantic level. We reinforce this impression by showing for ℒ that step bisimulation (i) coincides with pomset bisimulation equivalence, (ii) is real-time consistent, and (iii) has step trees as concrete representatives of its equivalence classes. Moreover, we show that none of these results holds for the language ℒ+ Finally, step trace equivalence is proved not to coincide with step bisimulation equivalence on ℒ.

scholarly journals Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's Merge

2004 ◽  
Vol 11 (1) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir ◽  
Bas Luttik
Keyword(s):  
Process Algebra ◽  
Binary Operation ◽  
Sharp Contrast ◽  
Parallel Composition ◽  
Finitely Based ◽  
Finite Axiomatization ◽  
Auxiliary Operation ◽  
Bisimulation Equivalence

This note shows that split-2 bisimulation equivalence (also known as timed equivalence) affords a finite equational axiomatization over the process algebra obtained by adding an auxiliary operation proposed by Hennessy in 1981 to the recursion free fragment of Milner's Calculus of Communicating Systems. Thus the addition of a single binary operation, viz. Hennessy's merge, is sufficient for the finite equational axiomatization of parallel composition modulo this non-interleaving equivalence. This result is in sharp contrast to a theorem previously obtained by the same authors to the effect that the same language is not finitely based modulo bisimulation equivalence.

scholarly journals A Modal Characterisation of Distributed Bisimulation

1991 ◽  
Vol 20 (347) ◽  
Author(s):  
Søren Christensen
Keyword(s):  
Special Kind ◽  
The Other ◽  
Proof System ◽  
Small Subset ◽  
Parallel Composition ◽  
Inference Rules ◽  
Bisimulation Equivalence ◽  
Distributed Bisimulation

In this paper we consider the distributed bisimulation equivalence defined by Hennessy and Castellani and later developed by Castellani. We present a logic in the style of Hennessy-Milner logic to charaterize the equivalence, i.e. we seek a logic such that whenever two processes are distributed bisimulation equivalent, they satisfy the same set of formulae and vice versa. Furthermore, for a small subset of CCS we provide a proof system which is shown to be sound and complete. The proof system is structural both in the structure of formulae and in the structure of processes. For the case of parallel composition of processes we present inference rules defined via a new combinator introduced. The combinator in question is left merge, a special kind of parallel composition in which the left operand has precedence over the other and must perform the first action observed.

A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes

1996 ◽  
Vol 6 (3) ◽  
pp. 251-259 ◽  
Author(s):  
Yoram Hirshfeld ◽  
Mark Jerrum ◽  
Faron Moller
Keyword(s):  
Polynomial Time ◽  
Composition Operator ◽  
Polynomial Time Algorithm ◽  
Time Algorithm ◽  
Parallel Composition ◽  
Elementary Processes ◽  
Parallel Processes ◽  
Bisimulation Equivalence

A polynomial-time algorithm is presented for deciding bisimulation equivalence of so-called Basic Parallel Processes: multisets of elementary processes combined by a commutative parallel-composition operator.

EFFICIENT ALGORITHMS FOR THE DYNAMICAL SIMULATION OF STRUCTURALLY FLEXIBLE MANIPULATORS

1989 ◽  
Vol 13 (4) ◽  
pp. 97-102 ◽  
Author(s):  
D.F. GOLLA ◽  
K.J. BUHARIWALA ◽  
P.C. HUGHES ◽  
G.M.T. D’ELEUTERIO
Keyword(s):  
Space Station ◽  
Flexible Manipulators ◽  
Recursive Algorithms ◽  
Focus Attention ◽  
Space Applications ◽  
Motion Equations ◽  
Dynamical Simulation ◽  
Space Manipulators ◽  
Computer Codes ◽  
Single Set

Canada’s Space Station Program has led to the need for highly efficient computer codes for the simulation of the dynamics of space manipulators with structurally flexible members. A discussion of dynamical principles and symbology are limited in this paper so that we may, in the brief space available, focus attention on how actually to solve the complex system of motion equations. Two types of algorithm are discussed: global algorithms of O(N3), in which a single set of motion equations is written for the manipulator as a whole; and recursive algorithms of O(N), in which motion equations are solved on a body-by-body basis. The algorithms described are compared numerically for computational efficiency. The recursive algorithms show superior speed for structurally flexible manipulators, especially in space applications where the initial body (orbiter) is unconstrained.

scholarly journals CCS with Hennessy's Merge has no Finite Equational Axiomatization

2003 ◽  
Vol 10 (34) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir ◽  
Bas Luttik
Keyword(s):  
Process Algebra ◽  
Parallel Composition ◽  
Finitely Based ◽  
Finite Axiomatization ◽  
Bisimulation Equivalence

This paper confirms a conjecture of Bergstra and Klop's from 1984 by establishing that the process algebra obtained by adding an auxiliary operator proposed by Hennessy in 1981 to the recursion free fragment of Milner's Calculus of Communicationg Systems is not finitely based modulo bisimulation equivalence. Thus Hennessy's merge cannot replace the left merge and communication merge operators proposed by Bergstra and Klop, at least if a finite axiomatization of parallel composition is desired.

scholarly journals A Menagerie of Non-Finitely Based Process Semantics over BPA*: From Ready Simulation Semantics to Completed Traces

1996 ◽  
Vol 3 (23) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Linear Time ◽  
Subject Classification ◽  
Regular Expressions ◽  
Basic Process ◽  
Branching Time ◽  
Finitely Based ◽  
Trace Semantics ◽  
Bisimulation Equivalence ◽  
Trace Equivalence

<p>Fokkink and Zantema ((1994) Computer Journal 37:259-267) have shown that<br />bisimulation equivalence has a finite equational axiomatization over the language<br />of Basic Process Algebra with the binary Kleene star operation (BPA*). In light<br />of this positive result on the mathematical tractability of bisimulation equivalence<br />over BPA*, a natural question to ask is whether any other (pre)congruence relation<br />in van Glabbeek's linear time/branching time spectrum is finitely (in)equationally<br />axiomatizable over it. In this paper, we prove that, unlike bisimulation equivalence,<br />none of the preorders and equivalences in van Glabbeek's linear time/branching time<br />spectrum, whose discriminating power lies in between that of ready simulation and<br />that of completed traces, has a finite equational axiomatization. This we achieve by<br />exhibiting a family of (in)equivalences that holds in ready simulation semantics, the<br />finest semantics that we consider, whose instances cannot all be proven by means of<br />any finite set of (in)equations that is sound in completed trace semantics, which is<br />the coarsest semantics that is appropriate for the language BPA*. To this end, for<br />every finite collection of (in)equations that are sound in completed trace semantics, we<br />build a model in which some of the (in)equivalences of the family under consideration<br />fail. The construction of the model mimics the one used by Conway ((1971) Regular<br />Algebra and Finite Machines, page 105) in his proof of a result, originally due to<br />Redko, to the effect that infinitely many equations are needed to axiomatize equality<br />of regular expressions.</p><p>Our non-finite axiomatizability results apply to the language BPA* over an arbitrary<br />non-empty set of actions. In particular, we show that completed trace equivalence<br />is not finitely based over BPA* even when the set of actions is a singleton.<br />Our proof of this result may be easily adapted to the standard language of regular expressions to yield a solution to an open problem posed by Salomaa ((1969) Theory<br />of Automata, page 143).<br />Another semantics that is usually considered in process theory is trace semantics.<br />Trace semantics is, in general, not preserved by sequential composition, and is<br />therefore inappropriate for the language BPA*. We show that, if the set of actions<br />is a singleton, trace equivalence and preorder are preserved by all the operators in<br />the signature of BPA, and coincide with simulation equivalence and preorder, respectively.<br />In that case, unlike all the other semantics considered in this paper, trace<br />semantics have nite, complete equational axiomatizations over closed terms.</p><p> </p><p>AMS Subject Classification (1991): 08A70, 03C05, 68Q10, 68Q40, 68Q45,<br />68Q55, 68Q68, 68Q70.<br />CR Subject Classification (1991): D.3.1, F.1.1, F.1.2, F.3.2, F.3.4, F.4.1.<br />Keywords and Phrases: Concurrency, process algebra, Basic Process Algebra<br />(BPA*), Kleene star, bisimulation, ready simulation, simulation, completed trace semantics,<br />ready trace semantics, failure trace semantics, readiness semantics, failures<br />semantics, trace semantics, equational logic, complete axiomatizations.</p><p> </p>

On Some Equivalence Relations for Probabilistic Processes1

1992 ◽  
Vol 17 (3) ◽  
pp. 211-234
Author(s):  
Dung T. Huynh ◽  
Lu Tian
Keyword(s):  
Polynomial Time ◽  
Graph Isomorphism ◽  
Polynomial Time Algorithm ◽  
Time Algorithm ◽  
Isomorphism Problem ◽  
Equivalence Relations ◽  
Transition Systems ◽  
Bisimulation Equivalence ◽  
Finite Trace ◽  
Trace Equivalence

In this paper, we investigate several equivalence relations for probabilistic labeled transition systems: bisimulation equivalence, readiness equivalence, failure equivalence, trace equivalence, maximal trace equivalence and finite trace equivalence. We formally prove the inclusions (equalities) among these equivalences. We also show that readiness, failure, trace, maximum trace and finite trace equivalences for finite probabilistic labeled transition systems are decidable in polynomial time. This should be contrasted with the PSPACE completeness of the same equivalences for classical labeled transition systems. Moreover, we derive an efficient polynomial time algorithm for deciding bisimulation equivalence for finite probabilistic labeled transition systems. The special case of initiated probabilistic transition systems will be considered. We show that the isomorphism problem for finite initiated labeled probabilistic transition systems is NC(1) equivalent to graph isomorphism.

scholarly journals A menagerie of non-finitely based process semantics over BPA* – from ready simulation to completed traces

1998 ◽  
Vol 8 (3) ◽  
pp. 193-230 ◽  
Author(s):  
LUCA ACETO ◽  
WAN FOKKINK ◽  
ANNA INGÓLFSDÓTTIR
Keyword(s):  
Linear Time ◽  
Time Spectrum ◽  
Finite Collection ◽  
Regular Expressions ◽  
Branching Time ◽  
Finitely Based ◽  
Finite Set ◽  
Trace Semantics ◽  
Bisimulation Equivalence ◽  
Trace Equivalence

Fokkink and Zantema (Fokkink and Zantema 1994) have shown that bisimulation equivalence has a finite equational axiomatization over the language of Basic Process Algebra with the binary Kleene star operation (BPA*). In light of this positive result on the mathematical tractability of bisimulation equivalence over BPA*, a natural question to ask is whether any other (pre)congruence relation in van Glabbeek's linear time/branching time spectrum is finitely (in)equationally axiomatizable over it. In this paper, we prove that, unlike bisimulation equivalence, none of the preorders and equivalences in van Glabbeek's linear time/branching time spectrum, whose discriminating power lies in between that of ready simulation and that of completed traces, has a finite equational axiomatization. This we achieve by exhibiting a family of (in)equivalences that holds in ready simulation semantics (which is the finest semantics that we consider) and whose instances cannot all be proved by means of any finite set of (in)equations that is sound in completed trace semantics (which is the coarsest semantics that is appropriate for the language BPA*). To this end, for every finite collection of (in)equations that are sound in completed trace semantics, we build a model in which some of the (in)equivalences of the family under consideration fail. The construction of the model mimics the one used by Conway (Conway 1971, p. 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions.Our non-finite axiomatizability results apply to the language BPA* over an arbitrary non-empty set of actions. In particular, we show that completed trace equivalence is not finitely based over BPA* even when the set of actions is a singleton. Our proof of this result may be adapted to the standard language of regular expressions to yield a solution to an open problem posed by Salomaa (Salomaa 1969, p. 143).Another semantics that is usually considered in process theory is trace semantics. Trace semantics is, in general, not preserved by sequential composition, and is therefore inappropriate for the language BPA*. We show that, if the set of actions is a singleton, trace equivalence and preorder are preserved by all the operators in the signature of BPA*, and coincide with simulation equivalence and preorder, respectively. In that case, unlike all the other semantics considered in this paper, trace semantics have finite, complete equational axiomatizations over closed terms.

Fifth Edition: the New Standard

2000 ◽  
Vol 5 (6) ◽  
pp. 1-7
Author(s):  
Christopher R. Brigham ◽  
James B. Talmage ◽  
Leon H. Ensalada
Keyword(s):  
Musculoskeletal System ◽  
Medical Information ◽  
Objective Assessment ◽  
Scientific Data ◽  
Practical Application ◽  
Fourth Edition ◽  
Appropriate Use ◽  
Medical Evaluation ◽  
Single Set

Abstract The AMA Guides to the Evaluation of Permanent Impairment (AMA Guides), Fifth Edition, is available and includes numerous changes that will affect both evaluators who and systems that use the AMA Guides. The Fifth Edition is nearly twice the size of its predecessor (613 pages vs 339 pages) and contains three additional chapters (the musculoskeletal system now is split into three chapters and the cardiovascular system into two). Table 1 shows how chapters in the Fifth Edition were reorganized from the Fourth Edition. In addition, each of the chapters is presented in a consistent format, as shown in Table 2. This article and subsequent issues of The Guides Newsletter will examine these changes, and the present discussion focuses on major revisions, particularly those in the first two chapters. (See Table 3 for a summary of the revisions to the musculoskeletal and pain chapters.) Chapter 1, Philosophy, Purpose, and Appropriate Use of the AMA Guides, emphasizes objective assessment necessitating a medical evaluation. Most impairment percentages in the Fifth Edition are unchanged from the Fourth because the majority of ratings currently are accepted, there is limited scientific data to support changes, and ratings should not be changed arbitrarily. Chapter 2, Practical Application of the AMA Guides, describes how to use the AMA Guides for consistent and reliable acquisition, analysis, communication, and utilization of medical information through a single set of standards.

Do You Want to See the Tree? Ignore the Forest

2014 ◽  
Vol 61 (3) ◽  
pp. 205-214 ◽  
Author(s):  
Nicolas Poirel ◽  
Claire Sara Krakowski ◽  
Sabrina Sayah ◽  
Arlette Pineau ◽  
Olivier Houdé ◽  
...  
Keyword(s):  
Visual Recognition ◽  
Local Level ◽  
Local Information ◽  
Visual Environment ◽  
Global Information ◽  
Focus Attention ◽  
Global Level ◽  
Hierarchical Stimuli ◽  
Priming Paradigm ◽  
The One

The visual environment consists of global structures (e.g., a forest) made up of local parts (e.g., trees). When compound stimuli are presented (e.g., large global letters composed of arrangements of small local letters), the global unattended information slows responses to local targets. Using a negative priming paradigm, we investigated whether inhibition is required to process hierarchical stimuli when information at the local level is in conflict with the one at the global level. The results show that when local and global information is in conflict, global information must be inhibited to process local information, but that the reverse is not true. This finding has potential direct implications for brain models of visual recognition, by suggesting that when local information is conflicting with global information, inhibitory control reduces feedback activity from global information (e.g., inhibits the forest) which allows the visual system to process local information (e.g., to focus attention on a particular tree).

Sign in / Sign up

Export Citation Format

Share Document