Modular Structural Operational Semantics with Strategies

In R. van Glabbeek and P. D. Mosses, editors, Proceedings of the 3rd Workshop on Structural Operational Semantics (SOS 2006), ENTCS 175(1), pages 3-17. Elsevier, 2007.

Abstract: Strategies are a powerful mechanism to control rule application in rule-based systems. For instance, different transition relations can be defined and then combined by means of strategies, giving rise to an effective tool to define the semantics of programming languages. We have endowed the Maude MSOS Tool (MMT), an executable environment for modular structural operational semantics, with the possibility of defining strategies over its transition rules, by combining MMT with the Maude strategy language interpreter prototype. The combination was possible due to Maude's reflective capabilities. One possible use of MMT with strategies is to execute Ordered SOS specifications. We show how a particular form of strategy can be defined to represent an OSOS order and therefore execute, for instance, SOS specifications with negative premises. In this context, we also discuss how two known techniques for the representation of negative premises in OSOS become simplified in our setting.

[pdf]

@inproceedings{BragaVerdejo06,
	Author = {Christiano Braga and Alberto Verdejo},
	Booktitle = {Proceedings of the 3rd Workshop on 
	             Structural Operational Semantics (SOS 2006)},
	Editor = {Rob van Glabbeek and Peter D. Mosses},
	Pages = {3-17},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {Modular Structural Operational Semantics with Strategies},
	Volume = {175(1)},
	Year = {2007}}