| 1. |
- Aceto, Luca, et al.
(författare)
-
A Rule Format for Unit Elements
- 2009
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper offers a meta-theorem for languages with a Structural Operational Semantics (SOS) in the style of Plotkin. Namely, it proposes a generic rule format for SOS guaranteeing that certain constants act as left- or right-unit elements for a set of binary operators. We show the generality of our format by applying it to a wide range of operators from the literature on process calculi.
|
|
| 2. |
- Aceto, Luca, et al.
(författare)
-
Algebraic properties for free!
- 2009
-
Ingår i: Bulletin of the European Association for Theoretical Computer Science. - : European Association for Theoretical Computer Science. - 0252-9742. ; 99, s. 81-103
-
Tidskriftsartikel (refereegranskat)abstract
- Algebraic properties specify some natural properties of programming and specification constructs. This paper provides an overview of techniques to guarantee or generate algebraic properties of language constructs by investigating the syntactic shape of the deduction rules defining their operational semantics.
|
|
| 3. |
- Aceto, Luca, et al.
(författare)
-
Impossibility results for the equational theory of timed CCS
- 2007
-
Ingår i: Algebra and Coalgebra in Computer Science. - Berlin : Springer Berlin/Heidelberg. - 9783540738572 - 9783540738596 ; , s. 80-95
-
Konferensbidrag (refereegranskat)abstract
- We study the equational theory of Timed CCS as proposed by Wang Yi in CONCUR'90. Common to Wang Yi's paper, we particularly focus on a class of linearly-ordered time domains exemplified by the positive real or rational numbers. We show that, even when the set of basic actions is a singleton, there are parallel Timed CCS processes that do not have any sequential equivalent and thus improve on the Gap Theorem for Timed CCS presented by Godskesen and Larsen in FSTTCS'92. Furthermore, we show that timed bisimilarity is not finitely based both for single-sorted and two-sorted presentations of Timed CCS. We further strengthen this result by showing that, unlike in some other process algebras, adding the untimed or the timed left-merge operator to the syntax and semantics of Timed CCS does not solve the axiomatizability problem.
|
|
| 4. |
|
|
| 5. |
- Aceto, Luca, et al.
(författare)
-
Lifting non-finite axiomatizability results to extensions of process algebras
- 2008
-
Ingår i: Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008. - New York : Springer-Verlag New York. - 9780387096797 - 9780387096803 ; , s. 301-316
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioral semantics over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational proofs over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller’s celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied.
|
|
