A Congruence Theorem for Structured Operational Semantics With Predicates and Negative Premises

. 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. Collation: pp. 20, ill. 2, tab. 5, ref. 25. Key Words & Phrases: structured operational semantics, term deduction system, transition system specification, strong bisimulation, congruence theorem, predicate, negative premise, negated predicate, stratifiable, stratification. 1980 Mathematics Subject Classification (1985 Revision): 68Q..