scholarly journals The Saga of the Axiomatization of Parallel Composition

2007 ◽  
Vol 14 (11) ◽  
Author(s):  
Luca Aceto ◽  
Anna Ingólfsdóttir
Keyword(s):  
Real Time ◽  
Parallel Composition ◽  
Process Algebras ◽  
Finite Axiomatizability ◽  
Nondeterministic Choice

This paper surveys some classic and recent results on the finite axiomatizability of bisimilarity over CCS-like languages. It focuses, in particular, on non-finite axiomatizability results stemming from the semantic interplay between parallel composition and nondeterministic choice. The paper also highlights the role that auxiliary operators, such as Bergstra and Klop's left and communication merge and Hennessy's merge operator, play in the search for a finite, equational axiomatization of parallel composition both for classic process algebras and for their real-time extensions.

MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS

2012 ◽  
Vol 23 (04) ◽  
pp. 831-851 ◽  
Author(s):  
GUOQIANG LI ◽  
XIAOJUAN CAI ◽  
SHOJI YUEN
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Expressive Power ◽  
Behavioral Model ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Modeling And Analysis ◽  
Compositional System ◽  
Time Systems ◽  
Timed Automaton

Timed automata are commonly recognized as a formal behavioral model for real-time systems. For compositional system design, parallel composition of timed automata as proposed by Larsen et al. [22] is useful. Although parallel composition provides a general method for system construction, in the low level behavior, components often behave sequentially by passing control via communication. This paper proposes a behavioral model, named controller automata, to combine timed automata by focusing on the control passing between components. In a controller automaton, to each state a timed automaton is assigned. A timed automaton at a state may be preempted by the control passing to another state by a global labeled transition. A controller automaton properly extends the expressive power because of the stack, but this can make the reachability problem undecidable. Given a strict partial order over states, we show that this problem can be avoided and a controller automaton can be faithfully translated into a timed automaton.

scholarly journals A Family of Resource-Bound Real-Time Process Algebras

2006 ◽  
Vol 162 ◽  
pp. 221-226 ◽  
Author(s):  
Insup Lee ◽  
Anna Philippou ◽  
Oleg Sokolsky
Keyword(s):  
Real Time ◽  
Time Process ◽  
Process Algebras ◽  
Resource Bound

scholarly journals Expressiveness modulo bisimilarity of regular expressions with parallel composition

2015 ◽  
Vol 26 (6) ◽  
pp. 933-968 ◽  
Author(s):  
JOS C. M. BAETEN ◽  
BAS LUTTIK ◽  
TIM MULLER ◽  
PAUL VAN TILBURG
Keyword(s):  
Finite Automata ◽  
Regular Expressions ◽  
Parallel Composition ◽  
Process Algebras ◽  
Star Operation

The languages accepted by finite automata are precisely the languages denoted by regular expressions. In contrast, finite automata may exhibit behaviours that cannot be described by regular expressions up to bisimilarity. In this paper, we consider extensions of the theory of regular expressions with various forms of parallel composition and study the effect on expressiveness. First we prove that adding pure interleaving to the theory of regular expressions strictly increases its expressiveness modulo bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style parallel composition gives a further increase in expressiveness, still insufficient, however, to facilitate the expression of all finite automata up to bisimilarity. Finally, we prove that the theory of regular expressions with ACP-style parallel composition and encapsulation is expressive enough to express all finite automata up to bisimilarity. Our results extend the expressiveness results obtained by Bergstra, Bethke and Ponse for process algebras with (the binary variant of) Kleene's star operation.

scholarly journals Compositional and Symbolic Model-Checking of Real-Time Systems

1996 ◽  
Vol 3 (59) ◽  
Author(s):  
Kim G. Larsen ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Symbolic Model Checking ◽  
Automatic Verification ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Symbolic Model ◽  
Verification Tools ◽  
State Region ◽  
Time Systems

Efficient automatic model-checking algorithms for<br />real-time systems have been obtained in recent years<br />based on the state-region graph technique of Alur,<br />Courcoubetis and Dill. However, these algorithms are<br />faced with two potential types of explosion arising from<br />parallel composition: explosion in the space of control<br />nodes, and explosion in the region space over clock variables.<br />In this paper we attack these explosion problems by<br />developing and combining compositional and symbolic<br />model-checking techniques. The presented techniques<br />provide the foundation for a new automatic verification<br />tool Uppaal. Experimental results indicate that<br />Uppaal performs time- and space-wise favorably compared<br />with other real-time verification tools.

scholarly journals Finite Equational Bases in Process Algebra: Results and Open Questions

2005 ◽  
Vol 12 (19) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir ◽  
Bas Luttik
Keyword(s):  
Process Algebra ◽  
State Of The Art ◽  
Linear Time ◽  
Time Spectrum ◽  
Parallel Composition ◽  
Basic Process ◽  
Process Algebras ◽  
Open Questions ◽  
The Subject ◽  
Sequential Processes

Van Glabbeek (1990) presented the linear time-branching time spectrum of behavioral equivalences for finitely branching, concrete, sequential processes. He studied these semantics in the setting of the basic process algebra BCCSP, and tried to give finite complete and omega-complete axiomatizations for them. (An axiomatization E is omega-complete when an equation can be derived from E if, and only if, all its closed instantiations can be derived from E.) Obtaining such axiomatizations in concurrency theory often turns out to be difficult, even in the setting of simple languages like BCCSP. This has raised a host of open questions that have been the subject of intensive research in recent years. Most of these questions have been settled over BCCSP, either positively by giving a finite complete or omega-complete axiomatization, or negatively by proving that such an axiomatization does not exist. Still some open questions remain. This paper reports on these results, and on the state-of-the-art on axiomatizations for richer process algebras, containing constructs like sequential and parallel composition.

scholarly journals In search of lost time: Axiomatising parallel composition in process algebras

2021 ◽  
Author(s):  
Luca Aceto ◽  
Elli Anastasiadi ◽  
Valentina Castiglioni ◽  
Anna Ingolfsdottir ◽  
Bas Luttik
Keyword(s):  
Parallel Composition ◽  
Process Algebras ◽  
Lost Time

scholarly journals A Categorical Axiomatics for Bisimulation

1998 ◽  
Vol 5 (22) ◽  
Author(s):  
Gian Luca Cattani ◽  
John Power ◽  
Glynn Winskel
Keyword(s):  
Higher Order ◽  
Parallel Composition ◽  
Process Algebras ◽  
Process Calculi ◽  
Open Map ◽  
Kleisli Category ◽  
Open Maps

We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. We work with 2-monads, T, on Cat. Operations on processes, such as nondeterministic sum, prexing and parallel composition are modelled using functors in the Kleisli category for the 2-monad T. We may define the notion of open map for any such 2-monad; in examples of interest, that agrees exactly with the usual notion of functional bisimulation. Under a condition on T, namely that it be a dense KZ-monad, which we define, it follows that functors in Kl(T) preserve open maps, i.e., they respect functional bisimulation. We further<br />investigate structures on Kl(T) that exist for axiomatic reasons,<br />primarily because T is a dense KZ-monad, and we study how those structures help to model operations on processes. We outline how this analysis gives ideas for modelling higher order processes. We conclude by making comparison with the use of presheaves and profunctors to model process calculi.

Sign in / Sign up

Export Citation Format

Share Document