This paper proposes a rule format for Structural Operational Semantics guaranteeing that certain constants act as left or right zero elements for a set of binary operators. Our design approach is also applied to reformulate an earlier rule format for unit elements developed by some of the authors. Examples of left and right zero, as well as unit, elements from the literature are shown to be checkable using the provided formats.

2.

Aceto, Luca

et al.

ICE-TCS, School of Computer Science, Reykjavik University, Reykjavik, Iceland.

Cimini, Matteo

ICE-TCS, School of Computer Science, Reykjavik University, Reykjavik, Iceland.

Ingólfsdóttir, Anna

ICE-TCS, School of Computer Science, Reykjavik University, Reykjavik, Iceland.

Mousavi, Mohammad Reza

Department of Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands.

Reniers, Michael A.

Department of Mechanical Engineering, Eindhoven University of Technology, Eindhoven, The Netherlands.

This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats.

3.

Aceto, Luca

et al.

ICE-TCS, School of Computer Science, Reykjavik University, Reykjavik, Iceland.

Ingólfsdóttir, Anna

ICE-TCS, School of Computer Science, Reykjavik University, Reykjavik, Iceland.

Mousavi, Mohammad Reza

Department of Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands.

Reniers, Michel A.

Department of Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands.

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.

4.

Aerts, Arend

et al.

Control Systems Technology Group, Eindhoven University of Technology, Eindhoven, The Netherlands.

Mousavi, Mohammad Reza

Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).

Reniers, Michel A.

Control Systems Technology Group, Eindhoven University of Technology, Eindhoven, The Netherlands.

A Tool Prototype for Model-Based Testing of Cyber-Physical Systems2015Inngår i: Theoretical Aspects of Computing – ICTAC 2015: 12th International Colloquium Cali, Colombia, October 29–31, 2015, Proceedings / [ed] Martin Leucker, Camilo Rueda, and Frank D. Valencia, Cham: Springer, 2015, Vol. 9399, s. 563-572Konferansepaper (Fagfellevurdert)

Department of Computer Science, Reykjavík University, Reykjavík, Iceland.

Mousavi, Mohammad Reza

Department of Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands.

Reniers, Michel A.

Department of Mechanical Engineering, Eindhoven University of Technology, Eindhoven, The Netherlands.

Gabbay, Murdoch J.

Computer Science Department, Heriot-Watt University, Edinburgh, United Kingdom.

Nominal SOS2012Inngår i: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII) / [ed] Ulrich Berger & Michael Mislove, Amsterdam: Elsevier, 2012, s. 103-116Konferansepaper (Fagfellevurdert)

Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language. This paper investigates preservation of sound equations for several notions of bisimilarity on open terms: closed-instance (ci-)bisimilarity and formal-hypothesis (fh-)bisimilarity, both due to Robert de Simone, and hypothesis-preserving (hp-)bisimilarity, due to Arend Rensink. For both fh-bisimilarity and hp-bisimilarity, we prove that arbitrary sound equations on open terms are preserved by all disjoint extensions which do not add labels. We also define slight variations of fh- and hp-bisimilarity such that all sound equations are preserved by arbitrary disjoint extensions. Finally, we give two sets of syntactic criteria (on equations, resp. operational extensions) and prove each of them to be sufficient for preserving ci-bisimilarity.

7.

Mousavi, Mohammad Reza

et al.

Eindhoven University of Technology, Eindhoven, The Netherlands.

Phillips, Iain C. C.

Imperial College London, London, United Kingdom.

Reniers, Michel A.

Eindhoven University of Technology, Eindhoven, The Netherlands.

Ulidowski, Irek

University of Leicester, University Road, Leicester, United Kingdom.

Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications. Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their conformance to our intuition for such rules. We take two general frameworks (rule formats) for SOS with negative premises and SOS with orderings, and present semantics-preserving translations between them with respect to our preferred notion of semantics. Thanks to our semantics-preserving translation, we take existing congruence meta-results for strong bisimilarity from the setting of SOS with negative premises into the setting of SOS with orderings. We further compare the expressiveness of rule formats for SOS with orderings and SOS with negative premises. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning.