Transition system specifications with negative premises
Jan Friso Groote · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1989
In this article the general approach to Plotkin style operational semantics of [12) is extended to Transition System Specifications (TSS's) with rules that may contain negative premises.Two problems arise: firstly the rules may be inconsistent, and secondly it is not obvious how a TSS determines a transition relation.We present a general method, based on the stratification technique in logic programming, to prove consistency of a set of rules and we show how a specific transition relation can be associated with a TSS in a natural way.Then a special format for the rules, the ntyftl ntyxt-fo rmat, is defined.It is shown that for this format three important theorems hold.The first theorem says that bisimulation is a congruence if all operators are defined using this format.The second theorem states that under certain restrictions a TSS in ntyft- format can be added conservatively to a TSS in pure ntyftl ntyxt-format.Finally, it is shown that the trace congruence for image finite processes induced by the pure ntyftl ntyxt-format is precisely bisimulation equivalence.