Algebra of communicating processes with abstraction
From MaRDI portal
This paper presents an equational axiom system \(ACP_{\tau}\), for communicating processes with silent actions (\(\tau\)-steps). The system is an extension of ACP, Algebra of Communicating Processes [see the authors, Inf. Control 60, 109-137 (1984)] with Milner's \(\tau\)-laws [see \textit{R. Milner}, A calculus of communicating processes (Berlin 1980; Zbl 0452.68027)] and an explicit abstraction ('hiding') operator. By means of a model of finite acyclic process graphs syntactic properties such as consistency and conservativity over ACP are proved. Also, the Expansion Theorem (which breaks down a parallel composition of n processes) is proved. By means of a term rewriting analysis using Dershowitz's recursive path orderings, termination of rewriting terms according to the \(ACP_{\tau}\) axioms is proved.
Recommendations
Cites work
- A note on simplification orderings
- A term model for synchronous processes
- Algebra of communicating processes with abstraction
- scientific article; zbMATH DE number 3852428 (Why is no real title available?)
- scientific article; zbMATH DE number 3878352 (Why is no real title available?)
- scientific article; zbMATH DE number 3978362 (Why is no real title available?)
- scientific article; zbMATH DE number 3986627 (Why is no real title available?)
- scientific article; zbMATH DE number 795666 (Why is no real title available?)
- Orderings for term-rewriting systems
- Process algebra for synchronous communication
- Processes and the denotational semantics of concurrency
- Synchronization trees
- Top-down design and the algebra of communicating processes
Cited in
(only showing first 100 items - show all)- The compression structure of a process
- Specification-oriented semantics for communicating processes
- Algebra of communicating processes with abstraction
- On the consistency of Koomen's fair abstraction rule
- Rewriting with a nondeterministic choice operator
- Algebraic solutions to recursion schemes
- Unification problems with one-sided distributivity
- Global renaming operators in concrete process algebra
- Transition systems, metric spaces and ready sets in the semantics of uniform concurrency
- An incompleteness result in process algebra
- The equivalence in the DCP model
- \(\tau\)-bisimulations and full abstraction for refinement of actions
- A compositional protocol verification using relativized bisimulation
- A calculus of mobile processes. I
- Enriched categorical semantics for distributed calculi
- From algebra to operational semantics
- TIC: a tImed calculus
- LOTOS extended with probabilistic behaviours
- A formal axiomatization for alphabet reasoning with parametrized processes
- Example verifications using alphabet axioms
- A decision algorithm for distributive unification
- A theory of processes with localities
- Automatizing parametric reasoning on distributed concurrent systems
- Using integer programming to verify general safety and liveness properties
- On the operational semantics of nondeterminism and divergence
- A polynomial algorithm for deciding bisimilarity of normed context-free processes
- Actors, actions, and initiative in normative system specification
- An equational axiomatization for multi-exit iteration
- A complete axiomatization of finite-state ACSR processes
- A process algebra of communicating shared resources with dense time and priorities
- Essential transitions to bisimulation equivalences
- The algebra of communicating processes with empty process
- A general conservative extension theorem in process algebras with inequalities
- Termination modulo equations by abstract commutation with an application to iteration
- Process algebra with language matching
- Two finite specifications of a queue
- Finite axiom systems for testing preorder and De Simone process languages
- Dynamic connectors for concurrency
- Bisimulation indexes and their applications
- Additive models of probabilistic processes
- A formal approach to object-oriented software engineering
- Rule formats for distributivity
- The quest for minimal quotients for probabilistic and Markov automata
- Modular specification of process algebras
- Fixed points in free process algebras. I
- Bisimulation of automata
- Process rewrite systems.
- Algorithmic analysis of programs with well quasi-ordered domains.
- A fixpoint theory for non-monotonic parallelism
- Branching time and orthogonal bisimulation equivalence
- DP lower bounds for equivalence-checking and model-checking of one-counter automata
- A theory of bisimulation for the -calculus
- Deriving structural labelled transitions for mobile ambients
- Topology in process calculus. I: Limit behaviour of agents
- Performance evaluation in stochastic process algebra dtsdPBC
- Congruence from the operator's point of view. Syntactic requirements on modal characterizations
- Off-the-shelf automated analysis of liveness properties for just paths
- Discrete time stochastic and deterministic Petri box calculus dtsdPBC
- Models and emerging trends of concurrent constraint programming
- Compositional verification of asynchronous concurrent systems using CADP
- A structural transformation from p- to MSVL
- Computable processes and bisimulation equivalence
- Resources in process algebra
- Control protocol synthesis for multi-agent systems with similar actions instantiated from agent and requirement templates
- SOS rule formats for idempotent terms and idempotent unary operators
- Pure bigraphs: structure and dynamics
- Refinement of actions for real-time concurrent systems with causal ambiguity
- \(\pi\)-calculus with noisy channels
- Polarized process algebra with reactive composition
- Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC
- Determinism \(\to\) (event structure isomorphism \(=\) step sequence equivalence)
- scientific article; zbMATH DE number 1670866 (Why is no real title available?)
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Parallel processes with implicit computational capital
- Process algebra having inherent choice: revised semantics for concurrent systems
- Composing models
- Connection between logical and algebraic approaches to concurrent systems
- Reactive Turing machines
- Process algebra and model checking
- Modelling and verifying the AODV routing protocol
- scientific article; zbMATH DE number 3862421 (Why is no real title available?)
- Combine and conquer: relating BIP and Reo
- A ground-complete axiomatisation of finite-state processes in a generic process algebra
- A Framework for Automatically Checking Anonymity with μCRL
- Behavioural equivalences of a probabilistic pi-calculus
- Modeling Routing Protocols in Adhoc Networks
- scientific article; zbMATH DE number 3990852 (Why is no real title available?)
- scientific article; zbMATH DE number 4011914 (Why is no real title available?)
- scientific article; zbMATH DE number 4056992 (Why is no real title available?)
- Readies and Failures in the Algebra of Communicating Processes
- scientific article; zbMATH DE number 64019 (Why is no real title available?)
- An algebra of behavioural types
- Value-passing CCS with noisy channels
- Fair expressions and regular languages over lists
- Network algebra for asynchronous dataflow∗
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes
- scientific article; zbMATH DE number 4117829 (Why is no real title available?)
- Diagnosis from scenarios
- scientific article; zbMATH DE number 919840 (Why is no real title available?)
This page was built for publication: Algebra of communicating processes with abstraction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1067408)
