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.

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>

scholarly journals A Game for Linear-time–Branching-time Spectroscopy

2021 ◽  
pp. 3-19
Author(s):  
Benjamin Bisping ◽  
Uwe Nestmann
Keyword(s):  
Linear Time ◽  
Time Spectrum ◽  
Branching Time ◽  
Finite State ◽  
Best Fit

AbstractWe introduce a generalization of the bisimulation game that can be employed to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. By measuring the use of expressive powers, we adapt the formula generation to just yield formulas belonging to the coarsest distinguishing behavioral preorders/equivalences from the linear-time–branching-time spectrum. The induced algorithm can determine the best fit of (in)equivalences for a pair of processes.

scholarly journals Ready To Preorder: Get Your BCCSP Axiomatization for Free!

2007 ◽  
Vol 14 (3) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Linear Time ◽  
Equational Theory ◽  
Time Spectrum ◽  
Basic Process ◽  
Branching Time ◽  
Discriminating Power

This paper contributes to the study of the equational theory of the semantics in van Glabbeek's linear time - branching time spectrum over the language BCCSP, a basic process algebra for the description of finite synchronization trees. It offers an algorithm for producing a complete (respectively, ground-complete) equational axiomatization of a behavioral congruence lying between ready simulation equivalence and partial traces equivalence from a complete (respectively, ground-complete) inequational axiomatization of its underlying precongruence--that is, of the precongruence whose kernel is the equivalence. The algorithm preserves finiteness of the axiomatization when the set of actions is finite. It follows that each equivalence in the spectrum whose discriminating power lies in between that of ready simulation and partial traces equivalence is finitely axiomatizable over the language BCCSP if so is its defining preorder.

scholarly journals Unifying Equivalences for Timed Transition Systems

10.29007/kkds ◽  
2018 ◽  
Author(s):  
Irina Virbitskaite ◽  
Natalya Gribovskaya ◽  
Eike Best
Keyword(s):  
Real Time ◽  
Linear Time ◽  
Time Spectrum ◽  
Branching Time ◽  
Real Time Systems ◽  
Transition Systems ◽  
Abstract Characterization ◽  
Time Systems ◽  
Open Maps

Timed transition systems are a widely studied model for real-time systems.The intention of the paper is to show how several categorical (open maps, path-bisimilarity and coalgebraic) approaches to an abstract characterization ofbisimulation relate to each other and to the numerous suggested behavioral equivalences of linear time -- branching time spectrum, in the setting of timed transition systems.

Sign in / Sign up

Export Citation Format

Share Document