| 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.
|
|
| 6. |
|
|
| 7. |
- Cranen, Sjoerd, et al.
(författare)
-
A rule format for associativity
- 2008
-
Ingår i: CONCUR 2008 - Concurrency Theory. - Berlin : Springer Berlin/Heidelberg. - 9783540853602 - 9783540853619 - 354085360X ; , s. 447-461
-
Konferensbidrag (refereegranskat)abstract
- We propose a rule format that guarantees associativity of binary operators with respect to all notions of behavioral equivalence that are defined in terms of (im)possibility of transitions, e.g., the notions below strong bisimilarity in van Glabbeek's spectrum. The initial format is a subset of the De Simone format. We show that all trivial generalizations of our format are bound for failure. We further extend the format in a few directions and illustrate its application to several formalisms in the literature. A subset of the format is studied to obtain associativity with respect to graph isomorphism.
|
|
| 8. |
- Dechesne, Francien, et al.
(författare)
-
Operational and epistemic approaches to protocol analysis : bridging the gap
- 2007
-
Ingår i: Logic for Programming, Artificial Intelligence, and Reasoning. - Berlin : Springer Berlin/Heidelberg. - 9783540755586 - 9783540755609 ; , s. 226-241
-
Konferensbidrag (refereegranskat)abstract
- Operational models of protocols, on one hand, are readable and conveniently match their implementation, at a certain abstraction level. Epistemic models, on the other hand, are appropriate for specifying knowledge-related properties such as anonymity. These two approaches to specification and analysis have so far developed in parallel and one has either to define ad hoc correctness criteria for the operational model or use complicated epistemic models to specify the operational behavior. We work towards bridging this gap by proposing a combined framework which allows modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic with temporal and epistemic operators.
|
|
| 9. |
|
|
| 10. |
- Hojjat, Hossein, et al.
(författare)
-
A framework for performance evaluation and functional verification in stochastic process algebras
- 2008
-
Ingår i: SAC '08. - New York : Association for Computing Machinery (ACM). - 9781595937537 ; , s. 339-346
-
Konferensbidrag (refereegranskat)abstract
- Despite its relatively short history, a wealth of formalisms exist for algebraic specification of stochastic systems. The goal of this paper is to give such formalisms a unifying framework for performance evaluation and functional verification. To this end, we propose an approach enabling a provably sound transformation from some existing stochastic process algebras, e.g., PEPA and MTIPP, to a generic form in the mCRL2 language. This way, we resolve the semantic differences among different stochastic process algebras themselves, on one hand, and between stochastic process algebras and classic ones, such as mCRL2, on the other hand. From the generic form, one can generate a state space and perform various functional and performance-related analyses, as we illustrate in this paper.
|
|
