Transition system specifications with negative premises (Q685387)

The general approach to Plotkin style operational semantics of \textit{J. F. Groote} and \textit{F. W. Vaandrager} [Structured operational semantics and bisimulation as a congruence, Inf. Comput. 100, No. 2, 202-260 (1992; Zbl 0752.68053)] 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 consistent TSS should determine 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 format of the rules, called the ntyft/ntyxt-format, is defined. A rule is in ntyft-format if it has the form \[ {\{t_ k\overset {a_ k} \longrightarrow y_ k\mid k\in K\}\cup \{t_ l\overset {b_ l} \nrightarrow \mid l\in L\}}\over f(x_ 1,...,x_ n)\overset {a} \longrightarrow t \] where \(K,L\) are index sets, \(t_ k,t_ i,t\) terms, \(y_ k,x_ 1,...,x_ n\) pairwise different variables, \(f\) a function symbol and \(a_ k,b_ l,a\) transition labels. A rule is in ntyxt-format if it is an instantiation of \[ {\{t_ k\overset {a_ k} \longrightarrow y_ k\mid k\in K\}\cup \{t_ l\overset {b_ l} \nrightarrow \mid l\in L\}}\over x\overset {a} \longrightarrow t \] where \(x\) is a variable, different from \(y_ k\). The ntyft/ntyxt-format is an extension of the tyft/tyxt-format that has been introduced in [loc. cit.]. It is shown that for the ntyft/ntyxt-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 ntyft/ntyxt-format. Finally, it is shown that the trace congruence for image finite processes induced by the pure ntyft/ntyxt-format is precisely bisimulation equivalence.