| 1. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
A Congruence Rule Format with Universal Quantification
- 2007
-
Ingår i: Proceedings of the 4th Workshop on Structural Operational Semantics. - Amsterdam : Elsevier. ; , s. 109-124
-
Konferensbidrag (refereegranskat)abstract
- We investigate the addition of universal quantification to the meta-theory of Structural Operational Semantics (SOS). We study the syntax and semantics of SOS rules extended with universal quantification and propose a congruence rule format for strong bisimilarity that supports this new feature. © 2007 Elsevier B.V. All rights reserved.
|
|
| 2. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
On well-foundedness and expressiveness of promoted tyft : being promoted makes a difference
- 2007
-
Ingår i: Proceedings of the 3rd Workshop on Structural Operational Semantics. - Amsterdam : Elsevier. ; , s. 45-56
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we solve two open problems posed by Karen L. Bernstein regarding her promoted tyft format for structured operational semantics. We show that, unlike formats with closed terms as labels, such as the tyft format, the well-foundedness assumption cannot be dropped for the promoted tyft format while preserving the congruence result. We also show that the well-founded promoted tyft format is incomparable to the tyft format with closed terms as labels, i.e., there are transition relations that can be specified by the promoted tyft format but not by the tyft format, and vice versa. © 2007 Elsevier B.V. All rights reserved.
|
|
| 3. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
SOS formats and meta-theory : 20 years after
- 2007
-
Ingår i: Theoretical Computer Science. - Amsterdam : Elsevier. - 0304-3975 .- 1879-2294. ; 373, s. 238-272
-
Tidskriftsartikel (refereegranskat)abstract
- In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS's) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues. In this paper, we provide an overview of SOS rule formats and meta-theorems formulated around them. © 2007 Elsevier Ltd. All rights reserved.
|
|
