×

A congruence theorem for structured operational semantics with predicates and negative premises. (English) Zbl 0839.68060

Summary: We proposed a syntactic format, the panth format, for structured operational semantics in which besides ordinary transitions also predicates, negated predicates, and negative transitions may occur such that if the rules are stratifiable, strong bisimulation equivalence is a congruence for all the operators that can be defined within the panth format. To show that this format is useful we took some examples from the literature satisfying the panth format but no formats proposed by others. The examples touch upon issues such as priorities, termination, convergence, discrete time, recursion, (infinitary) Hennessy-Milner logic, and universal quantification.

MSC:

68Q55 Semantics in the theory of computing
PDFBibTeX XMLCite