The meaning of Negative Premises in Transition System Specifications

We present a general theory for the use of negative premises in the rules of Transition System Specifications (TSSs). We formulate a criterion that should be satisfied by a TSS in order to be meaningful, that is, to unequivocally define a transition relation. We also provide powerful techniques for proving that a TSS satisfies this criterion, meanwhile constructing this transition relation. Both the criterion and the techniques originate from logic programming [van Gelder et al. 1988; Gelfond and Lifschitz 1988] to which TSSs are close. In an appendix we provide an extensive comparison between them. As in Groote [1993], we show that the bisimulation relation induced by a TSS is a congruence, provided that it is in ntyft/ntyxt-format and can be proved meaningful using our techniques. We also considerably extend the conservativity theorems of Groote [1993] and Groote and Vaandrager [1992]. ning example, we study the combined addition of priorities and abstraction to Basic Process Algebra...

• Type: Conference
• Year: 1990
• Where: LPNMR
• Authors: Roland N. Bol, Jan Friso Groote
• Keywords: Automated Reasoning, LPNMR 1990, Negative Premises, Process Algebra, Transition Relation