The Meaning of Negative Premises in Transition System Specifications II

R.J. van Glabbeek^{∗}

Computer Science Department, Stanford University Stanford, CA 94305, USA.

                                        rvg@cs.stanford.edu

This paper reviews several methods to associate transition relations to transition system specifications with negative premises in Plotkin’s structural operational style. Besides a formal comparison on generality and relative consistency, the methods are also evaluated on their taste in determining which specifications are meaningful and which are not.

1 Transition system specifications

In this paper V and A are two sets of variables and actions. Many concepts that will appear are parameterized by the choice of V and A, but as in this paper this choice is fixed, a corresponding index is suppressed.

Definition 1 (Signatures). A function declaration is a pair (f, n) of a function symbol f ∉ V and an arity n ∈ IN. A function declaration (c, 0) is also called a constant declaration. A signature is a set of function declarations. The set T T(Σ) of terms over a signature Σ is defined recursively by:

• V ⊆ T T(Σ),

• if (f, n) ∈ Σ and t_{1},…, t_{n} ∈ T T(Σ) then f(t_{1},…, t_{n}) ∈ T T(Σ).

A term c() is often abbreviated as c. T (Σ) is the set of closed terms over Σ, not containing any variables. A Σ-substitution σ is a partial function from V to T T(Σ). If σ is a substitution and S any syntactic object, then S[σ] denotes the object obtained from S by replacing, for x in the domain of σ, every occurrence of x in S by σ(x). In that case S[σ] is called a substitution instance of S.

Definition 2 (Transition system specifications). Let Σ be a signature. A positive Σ-literal is an expression t ⟶^{a} t′ and a negative Σ-literal an expression t −̸→^{a} or t −̸→^{a} t′ with t, t′ ∈ T T(Σ) and a ∈ A. For t, t′ ∈ T T(Σ) the literals t ⟶^{a} t′ and t −̸→^{a}, as well as t ⟶^{a} t′ and t −̸→^{a} t′, are said to deny each other. A transition rule over Σ is an expression of the form \frac{H}{α} with H a set of Σ-literals (the premises or antecedents of the the rule) and α a Σ-literal (the conclusion). A rule \frac{H}{α} with H = ∅ is also written α. A literal or transition rule is closed if it contains no variables. An action rule is a transition rule with a positive conclusion. A transition system specification (TSS) is a pair (Σ, R) with Σ a signature and R a set of action rules over Σ. A TSS is standard if its rules have no antecedents of the form t −̸→^{a} t′, and positive if all antecedents of its rules are positive.

∗This work was supported by ONR under grant number N00014-92-J-1974.

The first systematic study of transition system specifications with negative premises appears in Bloom, Istrail & Meyer [2]. The concept of a (positive) TSS presented above was introduced in Groote & Vaandrager [9]; the negative premises t −̸→^{a} were added in Groote [8]. The notion generalises the GSOS rule systems of [2] and constitutes the first formalization of Plotkin’s Structural Operational Semantics (SOS) [10] that is sufficiently general to cover most, if not all, of its applications. The premises t −̸→^{a} t′ are added here, mainly for technical reasons.

The following definition tells when a transition is provable from a TSS. It generalises the standard definition (see e.g. [9]) by (also) allowing the derivation of transition rules. The derivation of a transition t ⟶^{a} t′ corresponds to the derivation of the transition rule \frac{H}{t⟶^{a}t′} with H = ∅. The

case H ≠ ∅ corresponds to the derivation of t ⟶^{a} t′ under the assumptions H.

Definition 3 (Proof ). Let P = (Σ, R) be a TSS. A proof of a transition rule \frac{H}{α} from P is a well-founded, upwardly branching tree of which the nodes are labelled by Σ-literals, such that:

• the root is labelled by α, and

• if β is the label of a node q and K is the set of labels of the nodes directly above q, then 1. either K = ∅ and β ∈ H,

2. or \frac{K}{β} is a substitution instance of a rule from R.

If a proof of \frac{H}{α} from P exists, then \frac{H}{α} is provable from P, notation P ⊢ \frac{H}{α}. A closed negative literal α is refutable if P ⊢ β for a literal β denying α.

Definition 4 (Transition relation). Let Σ be a signature. A transition relation over Σ is a relation T ⊆ T (Σ) × A × T (Σ). Elements (t, a, t′) of a transition relation are written as t ⟶^{a} t′. Thus a transition relation over Σ can be regarded as a set of closed positive Σ-literals (transitions).

A closed literal α holds in a transition relation T, notation T ⊧ α, if α is positive and α ∈ T or

α = (t −̸→^{a} t′) and (t ⟶^{a} t′) ∉ T or α = (t −̸→^{a}) and (t ⟶^{a} t′) ∈ T for no t′ ∈ T (Σ). Write T ⊧ H,

for H a set of closed literals, if T ⊧ α for all α ∈ H.

A positive TSS specifies a transition relation in a straightforward way as the set of all provable transitions. But as pointed out in Groote [8], it is much less trivial to associate a transition relation to a TSS with negative premises. Several solutions are proposed in [8] and Bol & Groote [3]. Here I will present these solutions from a somewhat different point of view, and also review a few others.

P_{1}  \frac{c −̸→^{a}}{c ⟶^{b} c} \frac{c −̸→^{b}}{c ⟶^{a} c}

The TSS P_{1}^{1} can be regarded as an example of a TSS that does not specify a well-defined transition system. So unless a systematic way can be found to associate a meaning to TSSs like P_{1}, one has to accept that some TSSs are meaningless. Hence there are two questions to answer:

Which TSSs are meaningful, and which transition relations do they specify?  (1)

In this paper I present 11 possible answers to these questions, each consisting of a class of TSSs and a mapping from this class to transition relations. Two such solutions are consistent if they agree which transition relation to attach to a TSS in the intersection of their domains. Solution S′ extends S if the class of meaningful TSSs according to S′ extends that of S and the two are consistent, i.e. seen as partial functions S is included in S′.

1All my examples P_{i} consider TSSs (Σ, R) in which Σ consists of the single constant c only.

2 Model theoretic solutions

Solution 1 (Positive). A first and rather conservative answer to (1) is to take the class of positive TSSs as the meaningful ones, and associate with each positive TSS the transition relation consisting of the provable transitions.

Before proposing more general solutions, I will first recall two criteria from Bloom, Istrail & Meyer [2] and Bol & Groote [3] that can be imposed on solutions.

Definition 5 (Supported model). A transition relation T agrees with a TSS P if:

T ⊧ t ⟶^{a} t′ ⇔ there is a closed substitution instance \frac{H}{t⟶^{a}t′} of a rule of P with T ⊧ H.

T is a model of P if “⇐” holds; T is supported by P if “⇒” holds.

The first and most indisputable criterion imposed on a transition system T specified by a TSS P is that it is a model of P. This is called being sound for P in [2]. This criterion says that the rules of P, interpreted as implications in first-order or conditional logic, should evaluate to true statements about T. The second criterion, of being supported, says that T does not contain any transitions for which it has no plausible justification to contain them. In [2] being supported is called witnessing. Note that the universal transition relation on T (Σ) is a model of any TSS. It is however rarely the intended one, and the criterion of being supported is a good tool to rule it out. Next I check that Solution 1 satisfies both criteria.

Proposition 1 Let P be a positive TSS and T the set of transitions provable from P. Then T is a supported model of P. Moreover T is the least model of P.

Proof: That T is a supported model of P is an immediate consequence of the definition of provability. Furthermore, let T′ be any model of P, then by induction on the length of proofs it follows that T ⊆ T′. □

Starting from Proposition 1 there are at least three ways to generalise Solution 1 to TSSs with negative premises. One can generalise either the concept of a proof, or the least model property, or the least supported model property of positive TSSs. Starting with the last two possibilities, observe that in general no least model and no least supported model exists. A counterexample is given by the TSS P_{1} (given earlier), which has two minimal models, {c ⟶^{a} c} and {c ⟶^{b} c}, both of which are supported.

Solution 2 (Least). A TSS is meaningful iff it has a least model (this being its specified transition relation).

Solution 3 (Least supported). A TSS is meaningful iff it has a least supported model.

These two solutions turn out to have incomparable domains. The TSS P_{2} below has {c ⟶^{a} c} as its least model, but has no supported models. On the other hand P_{3} has two minimal models, namely {c ⟶^{b} c} and {c ⟶^{a} c} of which only the latter one is supported. This is its least supported model.

P_{2}  \frac{c −̸→^{a}}{c ⟶^{a} c}  P_{3}  \frac{c −̸→^{b}}{c ⟶^{a} c}

Obviously Solution 1 is extended by both solutions above. However, Solutions 2 and 3 turn out to be inconsistent with each other. P_{4} has both a least model and a least supported model, but they are not the same.

P_{4}  \frac{c −̸→^{a}}{c ⟶^{a} c} \frac{c ⟶^{b} c}{c ⟶^{a} c} \frac{c ⟶^{b} c}{c ⟶^{b} c}  P_{5}  \frac{c ⟶^{a} c}{c ⟶^{a} c}

Solution 2 is not very productive, because if fails to assign a meaning to the perfectly reasonable TSS P_{3}. Moreover, it can be criticized for yielding unsupported transition systems, as in the case of P_{2}. However, in P_{4} the least model {c ⟶^{a} c} appears to be a better choice than the least supported model {c ⟶^{a} c, c ⟶^{b} c}, as the ‘support’ for transition c ⟶^{b} c is not overwhelming. Thus, to my taste, Solution 3 is somewhat unnatural.

In Bloom, Istrail & Meyer [2] the following solution is applied.

Solution 4 (Unique supported). A TSS is meaningful iff it has a unique supported model.

The positive TSS P_{5} above has two supported models, ∅ and {c ⟶^{a} c}, and hence shows that Solution 4 does not extend Solution 1.

Although for the kind of TSSs considered in [2] (the GSOS rule systems) this solution coincides with all acceptable solutions mentioned in this paper, in general it suffers from the same drawback as Solution 3. The least supported model of P_{4} is even the unique supported model of this TSS. My conclusion is that the criterion of being supported is too weak to be of any use in this context.

This conclusion was also reached by Fages [5] in the setting of logic programming, who proposes to strengthen this criterion. Being supported can be rephrased as saying that a transition may only be present if there is a nonempty proof of its presence, starting from transitions that are also present. However, these premises in the proof may include the transition under derivation, thereby allowing for loops, as in the case of P_{4}. Now the idea behind a well-supported model is that the absence of a transition may be assumed a priory, as long as this assumption is consistent, but the presence of a transition needs to be proven without assuming the presence of (other) transitions. Thus a transition may only be present if it admits a valid proof, starting from negative literals only.

Definition 6 (Stable transition relation). A transition relation T is stable for a TSS P if:

T ⊧ t ⟶^{a} t′ ⇔ there is a closed transition rule \frac{N}{t⟶^{a}t′} without positive antecedents with P ⊢ \frac{N}{t⟶^{a}t′} and T ⊧ N.

T is well-supported by P if “⇒” holds.

Proposition 2 If T is stable for P, then it is a model of P. Moreover, any model of P satisfies “⇐”. Hence a stable transition relation is the same as a well-supported model.

Proof: Suppose there is a closed substitution instance \frac{H}{t⟶^{a}t′} of a rule of P with T ⊧ H. Assuming

that T is stable, for any t_{i} ⟶^{a_{i}} t′_{i} ∈ H there must be a closed transition rule _{\frac{N_{i}}{t_{i}⟶^{a_{i}}t′_{i}}} without positive

antecedents with P ⊢ _{\frac{N_{i}}{t_{i}⟶^{a_{i}}t′_{i}}} and T ⊧ N_{i}. Let N be the union of all those N_{i}’s and the negative

literals in H. Then, by combination of proof-fragments, \frac{N}{t⟶^{a}t′} is a closed transition rule without

positive antecedents with P ⊢ \frac{N}{t⟶^{a}t′} and T ⊧ N. Hence T ⊧ t ⟶^{a} t′.

The second statement follows by a trivial induction on the lenght of proofs, and the third one is an immediate corollary. □

Proposition 3 If a transition relation is well-supported by P, then it is supported by P.

Proof: Let T be well-supported by P, and let T ⊧ t ⟶^{a} t′. Then there is a closed transition rule \frac{N}{t⟶^{a}t′} without positive antecedents with P ⊢ \frac{N}{t⟶^{a}t′} and T ⊧ N. As the transition t ⟶^{a} t′ cannot be in N, there must be a non-empty proof of \frac{N}{t⟶^{a}t′}. Let \frac{K}{t⟶^{a}t′} be the closed substitution instance of a rule of P applied in the last step of this proof. After omitting this step from the proof, one is left with proofs for the literals in K. It follows that T ⊧ K, which had to be established. □

My concept of well-supportedness can easily be seen to coincide with the one of Fages [5]. The (earlier) concept of stability for TSSs stems from Gelfond & Lifschitz [7] in the context of logic programming. It has been adapted for TSSs by Bol & Groote [3]. In [3] stability was defined in terms of an operator Strip on TSSs without variables. If P is such a TSS and T a transition relation, Strip(P, T) is obtained from P by removing from P all rules with negative premises that do not hold in T, and removing from the remaining rules the negative premises that do hold (Definition 4.3 in [3]). This yields a positive TSS, whose associated transition relation is denoted ⟶_{Strip(P,T)}. Now T is said to be stable for P if T =⟶_{Strip(P,T)}. This definition is extended to TSSs P with variables by identifying such a TSS with the TSS of all closed substitution instances of rules in P.

Proposition 4 The concept of stability of Definition 6 coincides with that from [3].

Proof: Let P′ be a TSS and P be the TSS consisting of all closed substitution instances of rules in P. Note that T is stable for P in the sense of Definition 6 iff it is for P′.

The construction of Strip entails that Strip(P, T) ⊢ t ⟶^{a} t′ iff P ⊢ \frac{N}{t⟶^{a}t′} for a set of closed negative literals N with T ⊧ N. It follows immediately that both definitions are equivalent. □

The following two solutions are adaptations of Solutions 3 and 4, were the requirement of being supported has been replaced by that of being well-supported. The second is taken from [3].

Solution 5 (Stable). A TSS is meaningful iff it has a least stable transition relation.

Solution 5 (Stable). A TSS is meaningful iff it has a unique stable transition relation.

The particular numbering of these two solutions is justified by the following.

Proposition 5 Let T_{1} be a model of a TSS P and T_{2} be well-supported by P. If T_{1} ⊆ T_{2} then T_{1} = T_{2}. If follows (from the special case that T_{1} and T_{2} are both stable) that a TSS has a least stable transition relation iff it has a unique stable transition relation.

Proof: As T_{1} ⊆ T_{2} one has

T_{1} ⊧ t ⟶^{a} t′ ⇒ T_{2} ⊧ t ⟶^{a} t′

from which it follows that

T_{2} ⊧ t −̸→^{a} t′ ⇒ T_{1} ⊧ t −̸→^{a} t′  and  T_{2} ⊧ t −̸→^{a} ⇒ T_{1} ⊧ t −̸→^{a} .  (2)

Now suppose T_{2} ⊧ t ⟶^{a} t′. Then there is a closed transition rule \frac{N}{t⟶^{a}t′} without positive antecedents

with P ⊢ \frac{N}{t⟶^{a}t′} and T_{2} ⊧ N. By (2) we have T_{1} ⊧ N and hence T_{1} ⊧ t ⟶^{a} t′. □

Solution 5 improves Solutions 3 and 4 by rejecting the TSS P_{4} as meaningless. It also improves Solution 2 by rejecting the TSS P_{2} (whose least model was not supported). Surprisingly however, Solution 5 not only differs from the earlier solutions by being more fastidious; it also provides meaning to perfectly acceptable TSSs that were left meaningless by Solutions 2, 3 and 4.

P_{6}  \frac{c −̸→^{a}}{c ⟶^{b} c} \frac{c ⟶^{a} c}{c ⟶^{a} c}

An example is the TSS P_{6}. There is clearly no satisfying way to obtain c ⟶^{a} c. Hence c −̸→^{a} and consequently c ⟶^{b} c. {c ⟶^{b} c} is indeed the unique stable transition relation of this TSS. However, P_{6} has two minimal models, both of which are supported, namely {c ⟶^{b} c} and {c ⟶^{a} c}.

Proposition 6 Solution 5 (stable) is consistent with Solution 2 (least) and 3 (least supported).

Proof: If a TSS has both a (least) well-supported model and a least [supported] model, the two must be equal by Proposition 5. □

As the set of transitions provable from a positive TSS is by definition well-supported, Solution 5 (stable) extends Solution 1 (positive). Hence the relations between the solutions seen so far are as indicated in Figure 1 below. An arrow indicates an extension. The relation ⌣ indicates consistency and incomparible domains (neither one extends the other). There are no more extension and consistency relations than indicated in the figure (taking into account that positive⌣unique supported follows from the information displayed). All counterexamples appear earlier in this section.

[figure: positive (1); unique stable (5); least stable (5); unique supported (4); least supported (3); least model (2); ⌣; ⌣; ⌣]

Figure 1: Relations between Solutions 1–5

It is interesting to see how the various solutions deal with circular rules, such as \frac{c⟶^{a}c}{c⟶^{a}c}, and rules like \frac{c−̸→^{a}}{c⟶^{a}c}. The support-based solutions (3 and 4) may use a circular rule to obtain a transition that would be unsupported otherwise (Example P_{4}). This is my main argument to reject these solutions. In addition they may (or may not) reject TSSs as meaningless because of the presence of such a rule (Example P_{6}). On the other hand, Solutions 2 and 5 politely ignore these rules. To my taste, there are two acceptable attitudes towards circular rules: to ignore them completely (as done by Solutions 1, 2 and 5), or to reject any TSS with such a rule for being ambiguous, unless there is independent evidence for a transition c ⟶^{a} c. A strong argument in favor of the first approach is the existence of useful rules of which only certain substitution instances are circular (cf. [3]). A solution that caters to the second option will be proposed in the next section.

Solution 2 can treat a rule \frac{c−̸→^{a}}{c⟶^{a}c} as equivalent to c ⟶^{a} c (namely if there are no other closed terms than c, cf. P_{2}), which gives rise to unsupported transition relations. Solutions 3, 4 and 5 do not go so far, but use such a rule to choose between two otherwise equally attractive transition relations. This is illustrated by the TSS P_{7}, which determines the transition system {c ⟶^{a} c} according to each of the solutions 2, 3, 4 and 5.

P_{7}  \frac{c −̸→^{a}}{c ⟶^{b} c} \frac{c −̸→^{b}}{c ⟶^{a} c} \frac{c −̸→^{a}}{c ⟶^{a} c}

Note that ignoring rules like ^{\frac{c−̸→^{a}}{c⟶^{a}c}} is unacceptable, as this would yield unsound transition relations (non-models). But it could be argued that any TSS with such a rule should be rejected as meaningless, unless there is independent evidence for a transition c ⟶^{a} t. This would rule out P_{7}. Solutions that cater to this taste will be proposed in the next section.

3-Valued transition relations

3-valued interpretations of logical programs are considered, among others, in Van Gelder, Ross & Schlipf [6] and Przymusinski [12]. The same can be done for TSSs. The meaning of a TSS is then not given by a transition relation, i.e. a partition of T (Σ) × A × T (Σ) into the the transitions that hold and those that don’t, but a partition of T (Σ) × A × T (Σ) into three sets: true, false and unknown. Such a 3-valued interpretation is in logic programming often given as a pair ^{/} \T; F^{\} / of disjoint transition relations, representing the transitions that certainly hold, and those that certainly don’t. Here I find it easier to represent the same information as a pair T = ^{/} \CT, P T^{\} /, called a 3valued transition relation, with CT the set of transitions that certainly hold, and P T ⊇ CT the ones that possibly hold. Thus P T combines the values true and unknown, and is the complement of F. On 3-valued transition relations the information ordering ⊆ is defined by ^{/} \CT, P T^{\} / ⊆ ^{/} \CT′, P T′^{\} / iff CT ⊆ CT′ and P T ⊇ P T′, i.e. in ^{/} \CT′, P T′^{\} / the thruth or falsety of more transitions is known. In the ^{/} \T; F^{\} /-representation P T ⊇ P T′ translates to F ⊆ F′. A 3-valued transition relation ^{/} \CT, P T^{\} / is said to be 2-valued if CT = P T. Note that for a negative literal α, CT ⊧ α means that α possibly holds (no denying literal certainly holds), whereas P T ⊧ α means that α certainly holds (no denying literal possibly holds). This explains the following generalisation, based on the work of Przymusinski [12], of the concept of a stable transition relation (or well-supported model) to 3-valued interpretations.

Definition 7 (3-Valued stabilily). A 3-valued transition relation ^{/} \CT, P T^{\} / is stable for a TSS P if:

CT ⊧ t ⟶^{a} t′ ⇔ there is a closed transition rule \frac{N}{t⟶^{a}t′} without positive antecedents with P ⊢ \frac{N}{t⟶^{a}t′} and P T ⊧ N,

and P T ⊧ t ⟶^{a} t′ ⇔ there is a closed transition rule \frac{N}{t⟶^{a}t′} without positive antecedents with P ⊢ \frac{N}{t⟶^{a}t′} and CT ⊧ N.

The definition in [12] is a bit more complicated, but can be shown to amount to the same concept. Note that a stable transition relation as in Definition 6 can be regarded as a stable 3-valued transition relation T = ^{/} \CT, P T^{\} / with CT = P T. Przymusinski [12] showed that every logic program admits a 3-valued stable transition relation, and the same can be said for TSSs. There is even a least one w.r.t. the information ordering. He also showed that the least 3-valued stable model coincides with the well-founded semantics of an arbitrary TSS (logical program) proposed earlier by Van Gelder, Ross & Schlipf [6]. See Section 4 for a variant of the approach of [6]. The TSS P_{1} has three 3-valued stable transition relations, namely ^{/} \{c ⟶^{a} c}, {c ⟶^{a} c}^{\} /, ^{/} \{c ⟶^{b} c}, {c ⟶^{b} c}^{\} / and ^{/} \∅, {c ⟶^{a} c, c ⟶^{b} c}^{\} /. The first two are 2-valued. For reasons of symmetry the latter, which is also the least, is most suited as the intended meaning of this TSS. This is its well-founded semantics. Hence the following solution.

3-Valued Solution I (Well-founded) Any TSS is meaningful. Its meaning is its information-least 3-valued stable transition relation.

The existence of this relation will be demonstrated in the next section. The example P_{1} shows that there need not be a least 3-valued stable transition relation w.r.t. the truth ordering, defined by requiring CT ⊆ CT′ and P T ⊆ P T′. 3-Valued Solution I is not numbered with the others, as it does not provides (2-valued) transition relations. However, a 2-valued relation can be obtained by restricting attention to those TSSs for which the least 3-valued stable transition relation ^{/} \CT, P T^{\} / satisfies T = P T. Alternatively, just the component CT (or just P T) of the least 3-valued stable transition relation ^{/} \CT, P T^{\} / could be taken to be the meaning of a TSS. These possibilities will be explored in the next section. Finally I mention another 3-valued answer to (1), based on a generalisation of the notion of a supported model which is left as an exercise to the reader.

3-Valued Solution II Any TSS is meaningful. Its meaning is its information-least 3-valued supported model.

3 Proof theoretic solutions

In this section I will propose solutions based on a generalization of the concept of a proof. Note that in a proof two kinds of steps are allowed, numbered 1 and 2 in Definition 3. Step 1 just allows hypotheses to enter, in case one wants to prove a transition rule. This step can not be used when merely proving transitions. The essence of the notion is step 2. This step reflects the postulate that the desired transition relation must be a model of the given TSS. As a consequence those and only those transitions are provable that appear in any model. When generalising the notion of a proof to derive negative literals it makes sense to import more postulates about the desired transition relation. Note that a transition relation T is supported iff

T |̸= t ⟶^{a} t′ ⇐ for each closed substitution instance \frac{H}{t⟶^{a}t′} of a rule of P one has T |̸= H.

and well-supported iff

T |̸= t ⟶^{a} t′ ⇐ for each set of negative closed literals N with P ⊢ \frac{N}{t⟶^{a}t′}, one has T |̸= N.

Therefore I propose the following two concepts of provability.

Definition 8 (Supported proof ). A supported proof of a closed literal α from a TSS P is like a closed (positive) proof (see Definition 3), but admitting steps of the form

3. β is negative and for each closed substitution instance of a rule of P whose conclusion denies

β, a literal in K denies one of its antecedents. α is s-provable, notation P ⊢_{s} α, if a supported proof of α from P exists. A literal is s-refutable if a denying literal is s-provable.

Definition 9 (Well-supported proof ). A well-supported proof of a closed literal α from a TSS P is like a closed (positive) proof (see Definition 3), but admitting steps of the form 3. β is negative and for every set N of negative closed literals such that P ⊢ \frac{N}{γ} for γ a closed

literal denying β, a literal in K denies one in N.

α is ws-provable, notation P ⊢_{ws} α, if a well-supported proof of α from P exists. A literal is ws-refutable if a denying literal is ws-provable.

Note that these proof-steps establish the validity of β when K is the set of literals established earlier. In case K and N are sets of closed literals and a literal in K denies one in N, one has T |̸= N for any transition relation T with T ⊧ K. Thus step 3 from Definition 9 allows to infer t −̸→^{a} t′ whenever it is manifestly impossible to infer t ⟶^{a} t′, or t −̸→^{a} whenever it is manifestly impossible to infer t ⟶^{a} t′ for some term t′. This practice is sometimes referred to as negation as failure [4]. Definition 8 allows such an inference only if the impossibility to derive t ⟶^{a} t′ can be detected by examining all possible proofs that consist of one step only. This corresponds with the notion of negation as finite failure of Clark [4]. The extension of these notions (especially ⊢_{ws}) from closed to open literals α, or to transition rules \frac{H}{α}, is somewhat problematic, and not needed in this paper. The following may shed more light on ⊢_{s} and ⊢_{ws}.

Proposition 7 Let P be a TSS. Then P ⊢_{s} t −̸→^{a} [t′] iff every closed substitution instance \frac{H}{t⟶^{a}t′} of a rule of P has an s-refutable antecedent. Moreover P ⊢_{ws} t−̸→^{a}[t′] iff every set N of closed negative literals with P ⊢ \frac{N}{t⟶^{a}t′} contains an ws-refutable literal.

Proof: Fairly trivial. □

Proposition 8 For P a TSS and α a closed literal one has P ⊢ α ⇒ P ⊢_{s} α ⇒ P ⊢_{ws} α.

Proof: The first statement is trivial. The second will be established with induction on the structure of a ⊢_{s}-proof of α. Let \frac{K}{α} be the last step in such a proof. As P ⊢_{s} K by means of strict subproofs, it follows by induction that P ⊢_{ws} K. Here I write P ⊢_{x} K for K a set of literals if P ⊢_{x} β for all β ∈ K. If α is positive, P ⊢_{ws} α follows immediately from the definition of provability. Thus suppose α is negative. Let \{α_{i}\}_{i∈I} be the set of negative literals in K, and let \frac{K_{i}}{α_{i}} for i ∈ I be the collection of last proof-steps in ⊢_{ws}-proofs of the α_{i}. Let L = ⋃_{i∈I} K_{i} ∪ (K − {α_{i}}_{i∈I}). Then clearly P ⊢_{ws} L, so it suffices to show that for every set N of negative closed literals such that P ⊢ \frac{N}{γ} for γ a literal denying α, a literal in L denies one in N.

Consider a ⊢-proof p of \frac{N}{γ} with N a set of negative literals and γ denies α. By the definition of ⊢_{s}, p contains a literal δ that denies a literal β in K. This literal is the label of a node right above the root. In case δ occurs in N, β is positive and therefore occurs in L. In case δ ∉ N, β must be negative and hence be α_{i} for certain i ∈ I. Because \frac{K_{i}}{α_{i}} is a valid step in a ⊢_{ws}-proof and P ⊢ \frac{N}{δ} with δ denying α_{i}, a literal in N must deny one in K_{i} ⊆ L. □

Proposition 9 Let a quasi-proof be defined as in Definition 3, but without the requirement of well-foundedness. If in a TSS P any quasi-proof is well-founded, then P ⊢_{s} α ⇔ P ⊢_{ws} α.

Proof: Suppose P ⊢_{ws} α. Let \frac{K}{α} be the last step in a ⊢_{ws}-proof of α. Applying induction on such proofs, I may assume P ⊢_{s} K. In case α is positive the desired result P ⊢_{s} α follows immediately, so suppose it is not. Let β be a literal that denies α and let \frac{H}{β} be a closed substitution instance of a rule of P. This instance constitutes a (positive) one-step proof p of \frac{H}{β} from P. I have to show that H contains an s-refutable literal. Suppose by contradiction that is does not. Then, by Proposition 7, for every positive literal γ ∈ H there must a closed substitution instance \frac{H_{γ}}{γ} of a rule of P, without s-refutable antecedents. Adding these rules to p yields a larger proof p′ of a rule \frac{H′}{β} with H′ = ⋃_{\{γ∈H|γ positive\}} H_{γ} ∪ \{γ ∈ H | γ negative\}. Iterating this procedure by applying the same reasoning to H′ etc. yields a quasi-proof of a statement \frac{N}{β} with N a set of s-irrefutable closed negative literals. By assumption this quasi-proof must be a proof. By the ws-provability of α it follows that N must contain a literal that is denied by a literal from K, and hence s-refutable. This yields a contradiction. □

Definition 10 For a 3-valued T = ^{/} \CT, P T^{\} / define T ⊧ α as \begin{cases}CT ⊧ α if α is positive \\ P T ⊧ α if α is negative \end{cases}.

For P a TSS and α a closed literal, write P ⊧_{s} α [resp. P ⊧_{3s} α] if T ⊧ α for any [3-valued] supported model T of P and P ⊧_{ws} α [resp. P ⊧_{3ws} α] if T ⊧ α for any [3-valued] well-supported model T of P. A notion ⊢_{x} is called

• consistent if there is no TSS deriving two literals that deny each other.

• sound w.r.t. ⊧_{x} if for any TSS P and closed literal α, P ⊢_{x} α ⇒ P ⊧_{x} α.

• complete w.r.t. ⊧_{x} if for any TSS P and closed literal α, P ⊢_{x} α ⇐ P ⊧_{x} α.

Proposition 10 ⊢_{ws} is consistent.

Proof: Let’s say that two proofs p and q deny each other if their roots are labelled with literals that deny each other. By induction on their structure I establish that no two proofs from the same TSS P deny each other. So let p and q be two ⊢_{ws}-proofs from P and assume that no two proper subproofs deny each other. By contradiction suppose the roots of p and q are labelled with t ⟶^{a} t′ and t −̸→^{a} (or t −̸→^{a} t′) respectively. Note that the bottom part of p is a positive proof of a rule \frac{N}{t⟶^{a}t′}, where N contains only negative literals. Let K be the set of literals labelling nodes directly above the root of q. Then from the last step of q it follows that N (and thus p) contains a negative literal that denies one in K, thus yielding proper subproofs of p and q that deny each other. □

As P ⊢ α ⇒ P ⊢_{s} α ⇒ P ⊢_{ws} α, if follows that also ⊢_{s} and ⊢ are consistent.

Proposition 11 ⊢_{ws} is sound w.r.t. ⊧_{ws} and ⊧_{3ws}. Likewise ⊢_{s} is sound w.r.t. ⊧_{s} and ⊧_{3s}.

Proof: Let P be a TSS and T a [3-valued] well-supported model of P. With a straightforward induction on the structure of proofs if follows that P ⊢_{ws} α ⇒ T ⊧ α. The other part goes likewise.

Lemma 1 If P is a TSS and t −̸→^{a} a closed literal, then P ⊢_{x} t −̸→^{a} iff P ⊢_{x} t −̸→^{a} t′ for any term t′ ∈ T (Σ).

Proof: This follows immediately from the observation that a closed literal γ denies t −̸→^{a} iff it denies t −̸→^{a} t′ for some t′ ∈ T (Σ). □

The following theorem implies that any TSS has a least 3-valued [well-]supported model w.r.t. the information ordering. This justifies 3-valued Solutions I and II mentioned earlier.

Theorem 1 Let P be TSS with CT the set of [w]s-provable transitions and P T the set of [w]sirrefutable transitions (the ones for which no denying literal is [w]s-provable). Then ^{/} \CT, P T^{\} / is a 3-valued [well-]supported model of P. It is even the least one w.r.t. the information ordering.

Proof: Note that for α positive P ⊢_{[w]s} α ⇔ CT ⊧ α, and for α negative, using Lemma 1, P ⊢_{[w]s} α ⇔ P T ⊧ α. Using this, it is straightforward to check that CT and P T satisfy the required equations. It follows from the soundness of ⊢_{[w]s} w.r.t. ⊧_{3[w]s} (Proposition 11) that / \CT, P T^{\} / is included in any other 3-valued [well-]supported model of P. □

Corollary 1 ⊢_{ws} is complete w.r.t. ⊧_{3ws}. Likewise ⊢_{s} is complete w.r.t. ⊧_{3s}.

Proof: If P ⊧_{3[w]s} α then by definition α certainly holds in all [well]-supported models ^{/} \CT, P T^{\} / (if α is positive then α ∈ CT and if α is t −̸→^{a} t′ then t ⟶^{a} t′ ∉ P T). Thus α certainly holds in the least such model w.r.t. the information ordering, which is the one of Theorem 1. This implies P ⊢_{[w]s} α. □

However, ⊢_{s} and ⊢_{ws} are not complete w.r.t. ⊧_{[w]s}. A trivial counterexample concerns TSSs like P_{2} that have no [well-]supported models. P_{2} ⊧_{[w]s} α for any α, which by Proposition 10 is not the case for ⊢_{[w]s}. A more interesting counterexample concerns the TSS P_{7}, which has only one [well-]supported model, namely {c ⟶^{a} c}. In spite of this, P_{7} ⊬_{[w]s} c ⟶^{a} c and P_{7} ⊬_{[w]s} c −̸→^{b}.

As argued in the previous section, there is a point in excluding P_{7} from the meaningful TSSs, since there is insufficient evidence for the transition c ⟶^{a} c. Here the incompleteness of ⊢_{[w]s} w.r.t. ⊧_{[w]s} comes as a blessing rather than a shortcoming.

3.1 Solutions based on completeness

I will now introduce the concept of a complete TSS: one in which any transition is either provable or refutable. Just as in the theory of logic there is a distinction between the completeness of a logic (e.g. first-order) and the completeness of a particular theory (e.g. arithmetic), here the completeness of a TSS is something different from the completeness of a proof-method ⊢_{x}. Let x be s or ws.

Definition 11 (Completeness of a TSS). A TSS P is x-complete if for any transition t ⟶^{a} t′ either P ⊢_{x} t ⟶^{a} t′ or P ⊢_{x} t −̸→^{a} t′. By ‘complete’ I will mean ‘ws-complete’.

Note that a TSS is [w]s-complete iff its least (and only) 3-valued [well-]supported model is 2-valued.

Solution 6 (Complete with support). A TSS is meaningful iff it is s-complete. The associated transition relation consists of the s-provable transitions.

Solution 7 (Complete). A TSS is meaningful iff it is (ws-)complete. The associated transition relation consists of the ws-provable transitions.

In Bol & Groote [3] a method called reduction for associating a transition relation with a TSS was proposed, inspired by the well-founded models of Van Gelder, Ross & Schlipf [6] in logic programming. In Section 4 I show that this solution coincides with Solution 7. Solution 7 can therefore be regarded as a proof theoretical characterization of the ideas from [6, 3]. Solution 6 may be new.

The TSS P_{6} is complete, but not complete with support. P_{3} is even complete with support. The following proposition says that a standard TSS (i.e. without premises t −̸→^{a} t′) is complete if every closed negative standard literal can be proved or refuted.

Proposition 12 A standard TSS P is complete iff for any closed literal t −̸→^{a} either P ⊢_{ws} t ⟶^{a} t′ for some closed term t′ or P ⊢_{ws} t −̸→^{a}.

Proof: “only if”: Immediately by Lemma 1.

“if”: Suppose P ⊬_{ws} t ⟶^{a} t′. In that case any set N = \{t_{i} −̸→^{a_{i}}| i ∈ I\} such that P ⊢ \frac{N}{t⟶^{a}t′} must

contain a literal t_{N} −̸→^{a_{N}} with P ⊬_{ws} t_{N} −̸→^{a_{N}}. By assumption, for such a literal there is a t′_{N} with P ⊢_{ws} t_{N} ⟶^{a_{N}} t′_{N}. It follows from Definition 9, taking K to be the set of all transitions t_{N} ⟶^{a_{N}} t′_{N} (one for each possible choice of N), that P ⊢_{ws} t −̸→^{a} t′. □

As literals t −̸→^{a} t′ do not appear in the antecedents of rules in a standard TSS, their occurrence in a well-supported proof-tree can be limited to the root. Thus Proposition 12 says that the concept of a complete TSS can be introduced without considering such literals at all. The reason that these were introduced nevertheless, is that Proposition 12 does not apply to completeness with support. A counterexample is given by the TSS Q.

Q t ⟶^{a} t_{1} \frac{t ⟶^{a} t_{2}}{t ⟶^{a} t_{2}}  R t ⟶^{a} t_{1} \frac{t ⟶^{a} t_{2}}{t ⟶^{b} t_{2}}

Q ⊬_{s} t ⟶^{a} t_{2} and Q ⊬_{s} t −̸→^{a} t_{2}, thus this TSS is incomplete with support. However, for any closed literal u −̸→^{a}, either Q ⊢_{s} u ⟶^{a} u′ for some term u′ or Q ⊢_{s} u −̸→^{a}. Moreover, even for the derivation of standard literals, nonstandard literals may be essential in supported proofs. The validity of R ⊢_{s} t −̸→^{b} for instance, can only be established by a proof tree containing t −̸→^{a} t_{2}.

Proposition 13 The set of [w]s-provable transitions of a [w]s-complete TSS P is a model of P.

Proof: Let P be an x-complete TSS and T the set of x-provable transitions. Suppose \frac{H}{t⟶^{a}t′} is a closed substitution instance of a rule in P, and T ⊧ H. By Definition 4 (of T ⊧ H) P ⊢_{x} β for each positive antecedent β in H, and P ⊢_{x} γ for no transition γ denying a negative antecedent in H. Thus, by completeness and Lemma 1, P ⊢_{x} β for any β in H. Hence P ⊢_{x} t ⟶^{a} t′. □

Proposition 14 The set of [w]s-provable transitions of any TSS is well-supported.

Proof: Let P be a TSS and T the set of x-provable transitions. Suppose T ⊧ t ⟶^{a} t′, i.e. P ⊢_{x} t ⟶^{a} t′ with t and t′ closed terms. Take a [well-]supported proof of this transition from P, and delete all branches above a node labelled with a negative literal. This yields a positive proof of a rule \frac{N}{t⟶^{a}t′} with N a set of closed negative literals. For any literal δ in N one has P ⊢_{x} δ. By the consistency of ⊢_{x} P ⊢_{x} β for no closed literal β deying δ. This implies T ⊧ δ. □

Proposition 15 Solution 6 [7] is strictly extended by Solution 4 [5].

Proof: Suppose P is [w]s-complete. By Propositions 13 and 14 the [w]s-provable transitions constitute a [well-]supported model of P, and by Proposition 11 this is the only such model. Strictness follows from the TSS P_{7}, which has an unique [well-]supported model, but is left meaningless by Solutions 6 and 7. □

3.2 Advantages of the proof theoretic solutions

Now I will turn to the advantages of the proof theoretic solutions over the model theoretic ones. At the end of Section 2 I discussed the rôle of rules like \frac{c−̸→^{a}}{c⟶^{a}c} and \frac{c⟶^{a}c}{c⟶^{a}c}. My suggestion was that any TSS containing the former rule should be rejected as meaningless, unless there is independent evidence for a transition c ⟶^{a} t. As shown by counterexample P_{7} all model theoretic solutions fail this test. The following proposition shows that the proof theoretic solutions behave better in this respect.

Proposition 16 Let P, P′ be TSSs that only differ in a rule \frac{c−̸→^{a}}{c⟶^{a}c} that is in P but not in P′. Then P is [w]s-complete only if P′ is [w]s-complete and proves the same literals as P, including c ⟶^{a} t for some term t.

Proof: Suppose P is complete. It cannot be that P ⊢_{[w]s} c −̸→^{a}, since in that case one could derive P ⊢_{[w]s} c ⟶^{a} c, contradicting Proposition 10 (consistency). Thus the label c −̸→^{a} does not appear in any proof of a literal from P. It follows that any literal provable from P is already provable from P′. By Lemma 1, since P ⊬_{[w]s} c −̸→^{a}, P ⊢_{[w]s} c ⟶^{a} t for some term t. □

I also recommended two acceptable attitudes towards rule like \frac{c⟶^{a}c}{c⟶^{a}c}. Below I show that Solution 7 ignores such rules completely (which is one option), whereas Solution 6 rejects a TSS with such a rule, unless there is independent evidence for a transition c ⟶^{a} c (the other option).

Proposition 17 Let P, P′ be TSSs that only differ in a rule \frac{c⟶^{a}c}{c⟶^{a}c} that is in P but not in P′. Then P is ws-complete iff P′ is ws-complete. If P is ws-complete it proves the same literals as P′.

Proof: Any application of \frac{c⟶^{a}c}{c⟶^{a}c} can be eliminated from a positive or well-supported proof. □

Proposition 18 Let P, P′ be TSSs that only differ in a rule \frac{c⟶^{a}c}{c⟶^{a}c} that is in P but not in P′. Then

P is s-complete only if P′ is s-complete and proves the same literals as P, including c ⟶^{a} c.

Proof: Suppose P is complete. It is easy to eliminate applications of the rule \frac{c⟶^{a}c}{c⟶^{a}c} from any supported proof, so any literal provable from P is also provable from P′. Hence P′ is complete. Due to the rule \frac{c⟶^{a}c}{c⟶^{a}c} it is impossible to prove c −̸→^{a} c from P. Thus P ⊢_{s} c ⟶^{a} c. □

3.3 Solutions based on soundness

The remainder of this section is devoted to generalizations of the proof theoretic solutions. The first idea is to define the transition system associated to a TSS P just as in Solutions 6 and 7, that is as the set of [w]s-provable transitions, but without requiring that P is [w]s-complete. This amounts to taking as the meaning of P the component CT of its least [well-]supported model ^{/} \CT, P T^{\} /. In general this may yield unsound transition relations (non-models), which is not acceptable. This happens in the case of P_{1}, P_{2}, P_{4} and P_{7}. Thus the following restriction is needed.

Solution 8 (Sound with support). A TSS is meaningful if the set of s-provable transitions (this being the associated transition relation) constitutes a model.

Solution 8b A TSS is meaningful if the set of ws-provable transitions constitutes a model.

Note that by Proposition 14 the transition relation determined by such a TSS is even stable.

Proposition 19 Solution 8b coincides with Solution 7.

Proof: It follows immediatelty from Proposition 13 that a complete TSS is also meaningful in the sense of Solution 8b. Now let P be a TSS that is meaningful in the sense of Solution 8b and T the set of ws-provable transitions. Suppose P ⊬_{ws} t ⟶^{a} t′ for certain t, t′ ∈ T (Σ). Then T |̸= t ⟶^{a} t′. By the soundness of T every set N of closed negative literals such that P ⊢ \frac{N}{t⟶^{a}t′} must contain a literal δ with T |̸= δ. The latter means P ⊢_{ws} ϵ for a transition ϵ denying δ. Collecting all such ϵ’s (one for every choice of N) in a set K yields a well-supported proof of t −̸→^{a} t′. □

Proposition 20 Solution 8 is extended by Solutions 3 (least supported) and 8b (= 7, complete), and extends Solutions 1 (positive) and 6 (complete with support).

Proof: By Proposition 14 a TSS that is sound with support determines a transition relation that is a supported model. By Proposition 11 (the soundness of ⊢_{s} w.r.t. ⊧_{s}), this transition relation is included in any supported model. Therefore it constitutes the least.

By definition, the transition relation T_{1} determined by a TSS P that is sound with support is a model of P. The set T_{2} of transitions that are ws-provable from P is well-supported, by Proposition 14. By Proposition 8 T_{1} ⊆ T_{2} and Proposition 5 yields T_{1} = T_{2}. If follows that T_{2} is model too.

If a TSS P is positive, then P ⊢_{s} t ⟶^{a} t′ iff P ⊢ t ⟶^{a} t′. By Proposition 1 the (s-)provable transitions form a model.

The last statement follows immediately from Proposition 13. □

3.4 Solutions based on irrefutability

A second (and last) idea is to define the transition system T associated to a TSS P as the set of x-irrefutable transitions, i.e. T = {t ⟶^{a} t′ | P ⊬_{x} t −̸→^{a} t′}, in which x is s or ws. This amounts to taking as the meaning of P the component P T of its least [well-]supported model ^{/} \CT, P T^{\} /. This is consistent with Solutions 6 and 7, as for x-complete TSSs one has P ⊢_{x} t ⟶^{a} t′ ⇔ P ⊬_{x} t −̸→^{a} t′.

Proposition 21 The set of x-irrefutable transitions of any TSS consititutes a model.

Proof: Let P be a TSS and \frac{H}{t⟶^{a}t′} be a closed substitution instance of a rule of P. Let T be the set of x-irrefutable transitions and suppose T |̸= t ⟶^{a} t′, i.e. P ⊢_{x} t −̸→^{a} t′. I have to prove that T |̸= H. In case x = s it follows from Proposition 7 that H contains an x-refutable literal. I establish the same in case x = ws.

Suppose that P ⊬_{ws} u −̸→^{b} u′ for each positive antecedent α = (u ⟶^{b} u′) in H. Then for each such α there is a set N_{α} of ws-irrefutable negative closed literals with P ⊢ \frac{N_{α}}{α}. Let N be obtained from H by replacing α by N_{α} for each positive α in H. Then N contains negative literals only. Since P ⊢_{ws} t −̸→^{a} t′ and P ⊢ \frac{N}{t⟶^{a}t′}, N must contain a ws-refutable literal. This literal must be in H, which had to be established.

In case the x-refutable literal in H is positive, say u ⟶^{b} u′, we have P ⊢_{x} u −̸→^{a} u′, which implies T |̸= u ⟶^{b} u′. In case it is negative, say v −̸→^{c}, we have ∃v′ ∈ T (Σ) : P ⊢_{x} v ⟶^{c} v′, which by the consistency of ⊢_{x} implies ∃v′ : P ⊬_{x} v −̸→^{c} v′, which implies ∃v′ : T ⊧ v ⟶^{c} v′ and thus T |̸= v −̸→^{c}. In case of a literal v −̸→^{c} v′ just leave out the existential quantifications. □

For the moment I restrict attention to solutions yielding well-supported transition relations.

Solution 9a A TSS is meaningful if the set of s-irrefutable transitions (this being the associated transition relation) is well-supported.

Solution 9b A TSS is meaningful if the set of ws-irrefutable transitions is well-supported.

Note that by Proposition 21 the transition relation determined by such a TSS is even stable.

Proposition 22 Solution 9a coincides with Solution 6 and 9b with 7.

Proof: It follows immediatelty from Proposition 14 that the set of x-irrefutable transitions of a x-complete TSS is well-supported. Now let P be a TSS whose set T of x-irrefutable transitions is well-supported. Suppose P ⊬_{x} t −̸→^{a} t′ for certain t, t′ ∈ T (Σ). Then T ⊧ t ⟶^{a} t′. By the stability of T there is a set N of closed negative literals such that P ⊢ \frac{N}{t⟶^{a}t′} and T ⊧ N. The latter means T |̸= v ⟶^{c} v′ for any literal v −̸→^{c} v′ in N, which means P ⊢_{x} v −̸→^{c} v′. By Definition 4 and Lemma 1 the same holds for literals v −̸→^{c} in N. Therefore P ⊢_{x} t ⟶^{a} t′. □

3.5 Attaching meaning to all transition system specifications

In this section I will associate a transition relation to arbitrary TSSs. As illustruted by P_{1} and P_{2}, such a transition relation can not always be a supported model. I will insist on soundness (being a model), and thus have to give up support. Hence among the model theoretic solutions only Solution 2 (least model) can provide inspiration.

Let me first decide what to do with P_{1}. Since the associated transition relation should be a model, it must contain either c ⟶^{a} c or c ⟶^{b} c. For reasons of symmetry I cannot choose between these transitions, so the only way out is to include both. There is no reason to include even more transitions. Hence the transition system associated to P_{1} should be {c ⟶^{a} c, c ⟶^{b} c}.

The simplest model theoretic solution I thought of that gives this result is to define T_{1} as the union of all minimal models of a TSS. In many cases this will be the desired transition relation, but in can happen that T_{1} is not a model. In that case T_{2} is defined as the union of all minimal models containing T_{1}, and iterating this procedure until it stabilizes gives the associated transition relation.

However, in general this solution yields more transition then I would like to see. The transition system associated to P_{3} for instance would be {c ⟶^{a} c, c ⟶^{b} c}, whereas {c ⟶^{a} c} appears to be sufficient. The same would hold after addition of a second premise c −̸→^{a} to the only rule in P_{3}. In case there are other closed terms besides c the associated transition relation will be even larger. Therefore I will not pursue this idea further, and turn to the proof theoretic solutions instead. The reason for prefering transition c ⟶^{a} c over c ⟶^{b} c in P_{3} is not that c ⟶^{a} c is provable—after addition of the premise c −̸→^{a} it is not—but that c ⟶^{b} c is refutable. Therefore I consider:

Solution 9 (Irrefutable). Any TSS is meaningful. The associated transition relation consists of the ws-irrefutable transitions.

In the case of P_{1} this yields the desired result {c ⟶^{a} c, c ⟶^{b} c} and likewise P_{2}, P_{3} and P_{4} yield {c ⟶^{a} c}. The transition relation of P_{7} is the same as the one of P_{1}. This indicates that Solution 9 is inconsistent with Solutions 2–5. I don’t consider this to be a problem, as the model theoretic allocation of a transition relation to P_{7} was not very convincing.

A variant of Solution 9 is to associate to a TSS the set of its s-irrefutable transitions. This solution is inconsistent with Solution 1 (positive) as the transition relation of P_{5} would consist of c ⟶^{a} c. Note that this transition relation is supported. In order to rule out this anomaly one would have to restrict the meaningful TSSs to the ones for which the associated transition relation is well-supported, which yields Solution 9a, that has been shown to coincide with Solution 6.

Another variant is to stick to the ws-irrefutable transitions, but require those to form a supported model. Note that adding rules \frac{x⟶^{a}y}{x⟶^{a}y} for a ∈ A to an arbitrary TSS does not change the associated transition relation according to Solution 9, but makes this relation supported. Thus requiring the associated transion relation to be supported is not much of a restriction. Moreover, as rules like the one above should not make the difference between meaningful and meaningless TSSs, this requirement is not recommended.

4 Reduction

In this section I show that the method of reduction of Bol & Groote [3] coincides with Solution 7.

In [3] the operations T rue, P os and Red^{κ} for κ an ordinal are defined on TSSs without variables. The operator T rue deletes all rules with negative premises and thus yields a positive TSS. The operator P os deletes all negative premises from rules, and hence also yields a positive TSS. Finally the operator Red^{κ} deletes all rules that

• contain a positive premise that for some λ < κ is not provable from P os(Red^{λ}(P)) or

• contain a negative premise that for some λ < κ is refutable from T rue(Red^{λ}(P))

and in the remaining rules deletes all premises that are

• positive and for some λ < κ provable from T rue(Red^{λ}(P)) or

• negative and for some λ < κ not refutable from P os(Red^{λ}(P)).

The idea is that the positive TSSs T rue(Red^{κ}(P)) only prove transitions that surely hold, whereas the positive TSSs P os(Red^{κ}(P)) prove all transitions that possibly hold. Thus “not provable (or refutable, see Definition 3) from P os(Red^{λ}(P))” means “not provable (resp. refutable) at all”. Now a TSS without variables is said to be positive after reduction if for certain ordinal κ, Red^{κ}(P) is a positive TSS. In that case T rue(Red^{κ}(P)) = Red^{κ}(P) = P os(Red^{κ}(P)) and Red^{κ+1} is a TSS in which no rule has premises. The transition relation associated to such a TSS consists of the transitions provable from Red^{κ}(P), which are the rules of Red^{κ+1}(P). The case of TSSs with variables reduces to the case without variables by taking the set of all closed substitution instances of the rules in such a TSS.

Lemma 2 Let P be a TSS without variables.

1. For any closed positive literal α: P ⊢_{ws} α ⇒ ∃κ : T rue(Red^{κ}(P)) ⊢ α, and

2. for any closed negative literal α: P ⊢_{ws} α ⇒ ∃κ : P os(Red^{κ}(P)) does not refute α.

Proof: With induction on the structure of proofs. Suppose P ⊢_{ws} α by means of a proof p and the statements are established of β’s obtainable by subproofs. Let H be the set of labels directly above the root of p. For any literal β ∈ H, one has P ⊢_{ws} β by means of a subproof of p. Thus, for β positive ∃λ : T rue(Red^{λ}(P)) ⊢ β and for β negative ∃λ : P os(Red^{λ}(P)) does not refute β. Let κ be a strict upperbound of all those λ’s.

Now there are two cases. If α is positive, there is a rule \frac{H}{α} in P. By construction, all premises of this rule are deleted in the reduction process, and \frac{∅}{α} is a rule in Red^{κ}(P). Hence T rue(Red^{κ}(P)) ⊢ α.

Now suppose α is negative and P os(Red^{κ}(P)) refutes α. This means that P os(Red^{κ}(P)) ⊢ γ for γ a literal denying α, which implies that Red^{κ}(P) ⊢ \frac{N}{γ} for N a set of negative closed literals. Since p is a well-supported proof, a literal β ∈ H denies a literal δ in N. β must be positive, so ∃λ < κ : T rue(Red^{λ}(P)) ⊢ β, and δ is refutable from T rue(Red^{λ}(P)). It follows that at least one of the rules needed in the proof of \frac{N}{γ} has been deleted in Red^{κ}(P), contradicting Red^{κ}(P) ⊢ \frac{N}{γ}. Hence P os(Red^{κ}(P)) does not refute α. □

Proposition 23 Let P be a TSS without variables and α a closed literal. Then

Red^{κ}(P) ⊢_{ws} α ⇒ P ⊢_{ws} α.

Proof: By transfinite induction on κ. Suppose the statement has been established for all ordinals λ < κ. By definition T rue(P) ⊢ t ⟶^{a} t′ ⇒ P ⊢_{ws} t ⟶^{a} t′ and if β is negative and for all γ denying β we have P os(P) ⊬ γ then P ⊢_{ws} β. Substituting Red^{λ}(P) for P yields

(i) If β is positive and for some λ < κ provable from T rue(Red^{λ}(P)) then P ⊢_{ws} β, and

(ii) if β is negative and for some λ < κ not refutable from P os(Red^{λ}(P)) then P ⊢_{ws} β. Apply a (nested) induction on the structure of a well-supported proof p of α from Red^{κ}(P). Let K be the set of labels directly above the root of p. By induction P ⊢_{ws} β for any β ∈ K. In case α is positive, \frac{K}{α} must be a rule in Red^{κ}(P). Hence for a certain set H of premises \frac{K∪H}{α} must be a rule in P. The premises in H are deleted in the definition of Red^{κ}, and thus, by (i) and (ii), are ws-provable from P. It follows that P ⊢_{ws} α.

Now let α be negative. Suppose P ⊢ \frac{N}{γ} with γ a literal denying α and N a set of closed negative literals. I have to show that P ⊢_{ws} β for a literal β denying a literal δ in N. There are two cases.

• Suppose N contains a literal δ that for some λ < κ is refutable from T rue(Red^{λ}(P)). This means that T rue(Red^{λ}(P)) ⊢ β with β denying δ. Obviously Red^{λ}(P) ⊢ β, hence Red^{λ}(P) ⊢_{ws} β and by induction P ⊢_{ws} β.

• Suppose N contains no such literal. By induction on the structure of proofs I establish that P ⊢ \frac{N}{ϵ} ⇒ Red^{λ}(P) ⊢ \frac{N}{ϵ} for any transition ϵ and λ ≤ κ. Namely, suppose q is a proof of \frac{N}{ϵ} from P. Then for any ζ ≠ ϵ appearing in q we have P ⊢ \frac{N}{ζ} by means of a smaller proof, and hence Red^{λ}(P) ⊢ \frac{N}{ζ} for any λ ≤ κ, which implies P os(Red^{λ}(P)) ⊢ ζ. It follows that q employs no rule that is deleted in the construction of Red^{μ}(P) for μ ≤ κ. Thus, by cutting the branches in q that sprout from deleted premises in Red^{μ}(P), a proof q′ from Red^{μ}(P) is obtained of a rule \frac{N′}{ϵ} with N′ ⊆ N. Therefore Red^{μ}(P) ⊢ \frac{N}{ϵ}, as claimed. In particular Red^{κ}(P) ⊢ \frac{N}{γ}. By the definition of a well-supported proof (p), a literal β in K denies one in N. As remarked already, P ⊢_{ws} β. □

Theorem 2 A TSS is positive after reduction iff it is complete. In that case the associated transition relation is the set of ws-provable transitions.

Proof: Without limitation of generality I can restrict attention to TSSs P without variables.

Suppose P is positive after reduction. In that case there is an ordinal κ such that the rules of Red^{κ}(P) have no premises. Thus for any transition t −̸→^{a} t′ either Red^{κ}(P) ⊢_{ws} t ⟶^{a} t′ or Red^{κ}(P) ⊢_{ws} t −̸→^{a} t′. By Proposition 23 the same holds for P, which therefore must be complete.

As ⊢_{ws} is sound we have Red^{κ}(P) ⊢ t ⟶^{a} t′ ⇔ P ⊢_{ws} t ⟶^{a} t′.

Now suppose P is complete. For each closed literal α with P ⊢_{ws} α, there is an ordinal κ given by Lemma 2. Let μ be a strict upperbound of those κ’s. I will show that Red^{μ}(P) is positive. Let \frac{H}{α} be a rule in P and β ∈ H a negative premises. In case P ⊬_{ws} β, by completeness or Proposition 12 I have P ⊢_{ws} γ for a (positive) literal γ denying β, i.e. β is ws-refutable from P. By Lemma 2.1 β is refutable from T rue(Red^{κ}(P)) for some κ < μ. Hence \frac{H}{β} does not occur in Red^{μ}(P). In case P ⊢_{ws} β, Lemma 2.2 implies that β will be deleted from H in Red^{μ}(P). □

It is possible to simplify the definition of Red^{κ} by deleting only (rules with) negative premises. I.e. Red^{κ} deletes all rules that contain a negative premise that for some λ < κ is refutable from T rue(Red^{λ}(P)), and in the remaining rules deletes all negative premises that for some λ < κ are not refutable from P os(Red^{λ}(P)). For this version of Red Lemma 2, Proposition 23 and Theorem 2 remain true, with only slightly adapted proofs. Thus this simplified method of reduction gives the same meaning to TSSs as the original one.

5 Solutions based on stratification

Here I review two methods to assign meaning to transition system specifications based on the technique of (local) stratification, as proposed in the setting of logic programming by Przymusinski [11]. This technique was tailored for TSSs by Groote [8].

Definition 12 (stratification). A function S : (T (Σ) × A × T (Σ)) → λ, where λ is an ordinal, is called a stratification of a TSS P = (Σ, R) if for every rule \frac{H}{α} ∈ R and every substitution σ : V → T (Σ) it holds that

for all positive literals β ∈ H : S(σ(β)) ≤ S(σ(α)) and

for all transitions β denying a negative literal in H : S(σ(β)) < S(σ(α)).

A stratification is strict if also for all positive literals β ∈ H : S(σ(β)) < S(σ(α)). A TSS with a (strict) stratification is said to be (strictly) stratified.

In a stratified TSS no transition depends negatively on itself. A transition relation is associated to such a TSS one stratum S_{κ} = {α | S(α) = κ} at a time. A transition in S_{0} is present iff it is provable in the sense of Definition 3, and as soon as one knows the about validity of all transitions α with S(α) < κ for an ordinal κ, one knows the validity of all negative premises that could occur in a proof of a transition in stratum κ, which determines the validity of those transitions.

Definition 13 Let P be a TSS with a stratification S with range λ. The transition relations T_{κ} with κ < λ are defined by transfinite recursion through

T_{κ} = \{α | S(α) = κ ∧ P ⊢ \frac{H}{α} for a set of closed literals H with ⋃_{μ<κ} T_{μ} ⊧ H\}.

The transition relation T_{P,S} associated with P (and based on S) is ⋃_{μ<λ} T_{μ}.

Note that each transition in such a set H or denying a literal in H is in a lower stratum than α. Hence ⋃_{μ<κ} T_{μ} ⊧ H iff T_{P,S} ⊧ H. In Bol & Groote [3] T_{κ} is defined by T_{κ} = {α | P_{κ} ⊢ α} where P_{κ} is the set of all rules \frac{H^{κ}}{α} obtained from closed substitution instances \frac{H}{α} of rules from P with S(α) = κ and ⋃_{μ<κ} T_{μ} ⊧ H − H^{κ}. Here H^{κ} = {β ∈ H | β positive ∧ S(β) = κ}.

Proposition 24 Definition 13 agrees with the definition in [3].

Proof: Suppose α ∈ T_{κ} according to Definition 13. Let p be a closed proof of \frac{H}{α} where H is a set of literals with ⋃_{μ<κ} T_{μ} ⊧ H. Let p′ be obtained from p by deleting all branches above nodes labelled with a transition β with S(β) < κ. Then p′ is a proof from P of a rule \frac{H′}{α} with ⋃_{μ<κ} T_{μ} ⊧ H′. All rules used in p′ are also rules in P_{κ}, except that there the premises from H′ are deleted. It follows that P_{κ} ⊢ α. The other direction is straightforward. □

The definition in [3] can in turn be seen to coincide with the original one in Groote [8].

Proposition 25 If P is a TSS with stratification S and α a closed literal, then P ⊢_{ws} α iff T_{P,S} ⊧ α.

Proof: Define S(α) for α negative to be the least strict upperbound of {S(β) | β denies α}. Under this definition the two conditions in Definition 12 can be combined into

for all literals β ∈ H : S(σ(β)) ≤ S(σ(α)).

For α, β closed write α < β if either S(α) < S(β) or S(α) = S(β) with α negative and β positive.

“if”: With induction on <. Suppose T_{P,S} ⊧ α and the statement has been obtained for literals β with β < α. If α is positive then α ∈ T_{S(α)} and there is a set H of closed literals with P ⊢ \frac{H}{α} and ⋃_{μ<S(α)} T_{μ} ⊧ H, which implies T_{P,S} ⊧ H. As β < α for each β ∈ H, P ⊢_{ws} H and thus P ⊢_{ws} α. In case α is negative, then for each transition γ that denies α one has T_{P,S} |̸= γ, i.e. γ ∉ T_{S(γ)}. Hence, each set H of closed literals with P ⊢ \frac{H}{γ} contains a literal δ with ⋃_{μ<S(γ)} T_{μ} |̸= δ. This implies the existence of a literal β denying δ such that ⋃_{μ<S(γ)} T_{μ} ⊧ β. This holds in particular for sets H only containing negative literals, and in such a case β < δ < γ < α and T_{P,S} ⊧ β, so P ⊢_{ws} β. This for every choice of γ and a negative H. Definition 9 yields P ⊢_{ws} α.

“only if”: Suppose P ⊢_{ws} α with α negative. Then for any transition β denying α Proposition 10 gives P ⊬_{ws} β, and by “if” T_{P,S} |̸= β. By Definition 4 this implies T_{P,S} ⊧ α. Similarly suppose P ⊢_{ws} t ⟶^{a} t′. Then P ⊬_{ws} t −̸→^{a} t′, so by “if” T_{P,S} |̸= t −̸→^{a} t′. By definition this implies T_{P,S} ⊧ t ⟶^{a} t′. This proof benefits highly from the consideration of literals of the form t −̸→^{a} t′. □

Proposition 26 Let P be a TSS with two stratifications S and S′. Then T_{P,S} = T_{P,S′}.

Proof: This is Lemma 2.5.4 in [8]. Here it is an immediate corollary of Proposition 25. □

The last proposition says that for a stratified TSS the choice of the stratification in the construction of the transition relation is immaterial. This enables the following solution to (1).

Solution 10 (Stratified) [11, 8]. A TSS is meaningful iff it is stratified. The associated transition relation is given in Definition 13.

Proposition 27 Solution 10 strictly extends Solution 1 and is strictly extended by Solution 7.

Proof: If P is positive take S(α) = 0 for all α. This is a stratification and T_{P,S} = T_{0} = {α | P ⊢ α}. The second statement is an immediate consequence of Proposition 25, using that for any transition

t ⟶^{a} t′ either T ⊧ t ⟶^{a} t′ or T ⊧ t −̸→^{a} t′.

Strictness follows from P_{3} and P_{6}, which are stratified but not positive, and P_{8} below, which is complete but not stratified. □

P_{8} c ⟶^{a} c \frac{c −̸→^{a}}{c ⟶^{a} c}

Solution 11 (Strictly stratified) [8]. A TSS is meaningful iff it is strictly stratified. The associated transition relation is as in Definition 13, but with ‘P ⊢ \frac{H}{α} ’ replaced by ‘\frac{H}{α} is a closed substitution instance of a rule of P ’.

Proposition 28 Solution 11 is strictly extended by Solutions 10 and 6 (complete with support).

Proof: Note that T_{P,S} in Definition 13 would not change if P ⊢ \frac{H}{α} were replaced by ‘\frac{H}{α} is provable by means of a proof in which for all transitions β labelling a non-leaf we have S(β) = S(α) = κ’. This follows from the first four sentences in the proof of Proposition 24. In the special case that S is stratified, this modified definition agrees with the one proposed in Solution 11, which establishes the consistency of Solutions 10 and 11.

Just like in Proposition 25 one can prove that if P is a TSS with a strict stratification S and α is a closed literal, then P ⊢_{s} α ⇔ T_{P,S} ⊧ α. This implies that Solution 6 extends Solution 11.

Strictness follows from P_{5} and P_{6}, which are stratified but not strictly so, and P_{8}, which is complete with support but not strictly stratified. □

6 Compositionality

In concurrency theory it is common practice to group together representations of concurrent systems in equivalence classes. This is done when these representations are thought to represent the same system, or at least systems whose essential properties are the same. As system representations often closed terms over some signature are concidered. The equivalence relation employed is then formulated in terms of the transition relation between closed terms obtained from a given TSS over that signature. In order to allow modular reasoning it is important to use an equivalence relation that is a congruence. This means that the meaning (the associated equivalence class) of a closed term f(t_{1}, ..., t_{n}) is completely determined by the meaning of the subterms t_{1}, ..., t_{n}. The most popular equivalence relation is bisimulation equivalence. In Bol & Groote [3] it was established that for complete TSSs whose rules satisfy a syntactic criterion (the well-founded ntyft/ntyxt format, developed earlier in [9, 8]), bisimulation equivalence is guaranteed to be a congruence, and so are many other equivalence relations. Moreover, a counterexample was given againts the extension of this result to TSSs that are meaningful according to Solution 5 (stable). Of course the example concerned an incomplete TSS in well-founded ntyft/ntyxt format with a unique stable transition relation for which bisimulation is not a congruence. This TSS also has a unique supported model, and thus shows that the congruence theorem does not generalise to Solution 4 either. Here I show that also Solution 9—or any other proof theoretic solution for that matter—does not lend itself to such a generalisation, indicating that Solution 7 (complete) is the most general one for which this nice result holds. My counterexample concerns the following TSS S over a signature with constants c, d and e and a unary function f.

S c ⟶^{a} f(c) \frac{x ⟶^{a} y −̸→^{a}}{f(x) ⟶^{a} c} d ⟶^{a} e

This TSS is surely in the well-founded ntyft/ntyxt format. It has a unique 3-valued stable transition relation, namely

/ \{c ⟶^{a} f(c), d ⟶^{a} e, f(d) ⟶^{a} c}, {c ⟶^{a} f(c), d ⟶^{a} e, f(d) ⟶^{a} c, f(c) ⟶^{a} c}^{\} /.

Thus the transitions c ⟶^{a} f(c), d ⟶^{a} e and f(d) ⟶^{a} c are ws-provable, and with the exception of f(c) ⟶^{a} c, all other transitions are ws-refutable. Note, by the way, that for this TSS there is no difference between s-provability and ws-provability, or between s- and ws-refutability. This can be verified directly, or through Proposition 9. As the 3-valued relation above is not 2-valued, the TSS is incomplete (has no meaning according to Solution 7). It also has no meaning under Solution 5 (stable). The 3-valued transition relation constitutes the most acceptable interpretation of S. If we insist on 2-valued relations, the proof theorectic approach offers only one choice, namely whether or not to include the transition f(c) ⟶^{a} c. Each of these possibilities yields a transition relation for which bisimulation is not a congruence, and if fact no equivalence relation used in concurrency theory is a congruence. The only properties of such equivalence relations needed here, is that systems for which the reachable parts of the transition relation are isomorphic are equivalent, and a system without outgoing transitions (a deadlock) cannot be equivalent to a system with an outgoing a-transition. Solution 9 (irrefutable) includes the transition f(c) ⟶^{a} c. Now c and f(c) are equivalent (the reachable part of the transition relation from each of them is an a-loop), but f(c) and f(f(c)) are inequivalent (f(f(c)) deadlocks). Taking only the provable transitions (instead of the irrefutable ones) would exclude the transition f(c) ⟶^{a} c. In that case c and d are equivalent, but f(c) and f(d) are not.

7 Conclusion

I presented 11 answers to the question which transition system specifications are meaningful and which transition relations they specify. The relations between these 11 solutions are indicated in Figure 2. There S_{1} \overline{}S_{2} indicates that solution S_{2} extends S_{1}, as defined in Section 1, and

[figure: positive (1); stratified (10); complete (7); stable (5); strictly stratified (11); complete with support (6); unique supported (4); least supported (3); sound with support (8); least model (2); #; #; #; #; irrefutable (9)]

Figure 2: Relations between Solutions 1–11

S_{1}#S_{2} indicates that S_{1} and S_{2} are inconsistent. By the definition of extension and consistency, [figure: S_{1}; S_{2}; S_{3}] implies S_{1} \overline{}S_{3} (transitivity) and S_{1} # S_{2} \overline{}S_{3} implies S_{1}#S_{3} (conflict heredity). All extensions are strict and there are no more extensions or inconsistencies than indicated in the figure (or derivable by transitivity and conflict heredity). The arrows in Figure 2 have been established in Propositions 1, 27, 28, 15 and 20 and in the third sentence of Section 3.4, whereas the remaining consistency results follow from Proposition 6. Strictness, the absence of further extensions and the inconsistencies follow from the information collected in Table 1, which indicates which of the TSSs P_{1}–P_{8} given in this paper are meaningful according to each of the solutions. A ‘−’ indicates that the TSS is meaningless, a ‘+’ that it has the same meaning as given by Solution 9, and a ‘∗’ that is has a meaning different from the one given by Solution 9.

Solution  P_{1} P_{2} P_{3} P_{4} P_{5} P_{6} P_{7} P_{8}
1 positive  − − − − + − − −
2 least  − + − + + − ∗ +
3 least supported  − − + ∗ + − ∗ +
4 unique supported  − − + ∗ − − ∗ +
5 stable  − − + − + + ∗ +
6 complete with support − − + − − − − +
7 complete  − − + − + + − +
8 sound with support  − − + − + − − +
9 irrefutable  + + + + + + + +
10 stratified  − − + − + + − −
11 strictly stratified  − − + − − − − −

Table 1: Counterexamples

Logic programming

Everything said in this paper about transition system specifications applies equally well to proposition system specifications (PSSs). These are obtained by replacing the set A of actions by a set of predicate declarations (p, n) with p ∉ V a predicate symbol (different from any function symbol) and n ∈ IN. A literal is then an expression p(t_{1},…, t_{n}) or ¬p(t_{1},…, t_{n}) with t_{i} ∈ T T(Σ). From here on all concepts are defined as before. Note that a logic program is a PSS obeying some finiteness conditions. Hence everything said applies to logic programming too.

Note that a PSS can be seen as a special kind of TSS. First of all an n-ary predicate p can be expressed in terms of an n-ary function f_{p} and the unary predicate holds, namely by defining holds(f_{p}(t_{1}, ..., t_{n})) as p(t_{1}, ..., t_{n}). Next, if p is a unary predicate then p(t) can be encoded as the transition t ⟶^{p} 0, with 0 a constant introduced specially for this purpose (cf. Verhoef [13]).

Likewise a TSS can be encoded as a PSS by considering ⟶^{a} to be a binary predicate for any a ∈ A, or, as in Bol & Groote [3], ⟶ as a single ternary predicate with a ∈ A interpreted as a term. A negative literal t −̸→^{a} t′ denotes ¬(t ⟶^{a} t′) and t −̸→^{a} can be seen as an abbreviation of the (infinite) conjunction of t −̸→^{a} t′ for t′ ∈ T T(Σ). These translations preserve all concepts of this paper. In order to avoid the infinite conjunction, Bol & Groote introduce the unary version of ⟶^{a} (or actually the binary version of ⟶) as a separate predicate, linked to the binary (ternary)

version by the rule \frac{x ⟶^{a} y}{x ⟶^{a}}, implicitly present in every TSS. As shown in anomaly A.3 in [3] this

translation does not preserve Solution 2 (least model). However, it does preserve the other concepts.

In this paper I do not touch issues that are relevant in logic programming, but not manifestly so for transition system specifications. For these, and many more references, see Apt & Bol [1].

Evaluation of the solutions

Solution 1 is the classical interpretation of TSSs without negative premises, and Solutions 2 (least model) and 3 (least supported model) are two straightforward generalisations. Solution 4 (unique supported model) stems from Bloom, Istrail & Meyer [2], where it was used to ascertain that TSSs in their so-called GSOS format are meaningful (such TSSs have unique supported models). My counterexample P_{4} shows that Solution 4 yields contraintuitive results and is therefore not suited to base such a conclusion on. Fortunately, TSSs in the GSOS format are even strictly stratified, which is one of the most restrictive criteria for meaningful TSSs considered. Solution 3 can be rejected on the same grounds as Solution 4 and Solution 2 is not very useful because it leaves most TSSs with negative premises meaningless (cf. P_{3}).

Solution 10 (stratified) stems from Przymusinski [11] and is the perhaps the best known solution in logic programming. A variant that also satisfies the criterion of Solution 4 is Solution 11 (strictly stratified), proposed by Groote [8].

Solution 5 (unique stable transition relation) stems from Gelfond & Lifschitz [7] and is generally considered to be the most general acceptable solution available. Counterexample P_{7} however suggests that this solution may yield debatable results, although to a lesser extent than Solutions 3 and 4.

Solution 7 (well-founded, positive after reduction, complete) is essentially due to Van Gelder, Ross & Schlipf [6]. It is the most general solution without undesirable properties. In Bol & Groote [3], where this solution has been adapted to TSSs, an example in the area of concurrency is given (the modelling of a priority operator in basic process algebra with abstraction) that can be handled with Solution 7, but not with Solution 10. This example can neither be handled by Solution 8, showing that the full generality of Solution 7 can be useful in applications.

My presentation of Solution 7 differs so much from the original one [6, 3] that I gave it a new name. It is based on a concept of provability incorporating the notion of negation as failure of Clark [4]. Theorem 2 establishes the correspondence between my version and the one from [6, 3], whereas Theorem 1 establishes the correspondence with the work of Przymusinski [12]. I think that my proof-theoretic characterization of Solution 7, and to some extent also the one of Solution 5, can be useful in applications, among others because it allows induction on proofs. The following proposition on transition equivalence of TSSs for instance follows immediately from the definitions given here, whereas it would be nontrivial when starting from the original definitions. As a matter of fact, I need this proposition in another paper, and the search for it inspired me to write this one.

Proposition 29 Let P and P′ be TSSs over the same signature, such that P ⊢ \frac{N}{α} ⇔ P′ ⊢ \frac{N}{α} for any closed action rule \frac{N}{α} with only negative antecedents. Then

• A transition relation T is stable for P iff it is stable for P′. Hence P is meaningful according to Solution 5 iff P′ is, and in that case they determine the same transition relation.

• P ⊢_{ws} β ⇔ P′ ⊢_{ws} β for any closed literal β. Hence P is meaningful according to Solution 7 iff P′ is, and in that case they determine the same transition relation.

• According to Solution 9 P and P′ are meaningful and determine the same transition relation.

Solutions 6 (complete with support), 8 (sound with support), and 9 (irrefutable) may be new. The first two are based on a notion of provability that is somewhat simpler to apply, and only incorporates the notion of negation as finite failure [4]. Moreover, Solution 6 only yields unique supported models, like Solution 11 (and 4). Solution 9 appears to be the best way to associate a transition relation to arbitrary TSSs. However, it has the disadvantage that it sometimes yields unstable transition relations, and even unsupported models. A good example from concurrency theory of an incomplete TSS is Basic Process Algebra with a priority operator, unguarded recursion and renaming, as defined in Groote [8]. This TSS has no supported models. Solution 9 does give a meaning to this TSS, but it appears rather arbitrary and not very useful. In particularly, recursively defined processes do no longer satisfy their defining equation, which makes algebraic reasoning virtually impossible. Also the absence of a congruence theorem as demonstrated in Section 6 is a bad property of this Solution. Hence Solution 7 (complete) remains the most general completely acceptable answer to (1). In case 3-valued solutions are allowed, this solution generalises to all transition system specifications in the shape of the well-founded semantics.

Specifying transition relations

This paper dealt with the problem of associating a transition relation to a given TSS. A related problem is to find a good TSS to specify a given transition relation. Here “good” could be something like “finite” or “in ntyft/ntyxt format”. Without such a restriction the transition relation itself can be used as TSS, regarding every transition as a rule without premises. The problem can be further parametrised by specifying the desired transition relation up to a given notion of equivalence only. In this light the solutions of Figure 2 can be compared also on their expressiveness, i.e. are there transition relations that can be specified by a good TSS that is meaningful according to solution S, but not by one that fits in solution S′? This issue is left for future research.

Acknowledgments

This paper benefited greatly from the insightful comments of Roland Bol. Also thanks to the audience of the PAM seminar for useful feedback.

References

[1] K.R. Apt & R. Bol (1994): Logic programming and negation: A survey. Journal of Logic Programming 19–20, pp. 9–71.

[2] B. Bloom, S. Istrail & A.R. Meyer (1988): Bisimulation can’t be traced: Preliminary report. In Conference Record of the 15^{th} ACM Symposium on Principles of Programming Languages, San Diego, California, pp. 229–239. Full version available as Technical Report 90-1150, Department of Computer Science, Cornell University, Ithaca, New York, August 1990. Accepted to appear in Journal of the ACM.

[3] R.N. Bol & J.F. Groote (1991): The meaning of negative premises in transition system specifications (extended abstract). In J. Leach Albert, B. Monien & M. Rodríguez, editors: Proceedings 18^{th} ICALP, Madrid, LNCS 510, Springer-Verlag, pp. 481–494. Full version appeared as Report CS-R9054, CWI, Amsterdam, 1990.

[4] K.L. Clark (1978): Negation as failure. In H. Gallaire & J. Minker, editors: Logic and Databases, Plenum Press, New York, pp. 293–322.

[5] F. Fages (1991): A new fixpoint semantics for general logic programs compared with the well-founded and the stable model semantics. New Generation Computing 9(4).

[6] A. van Gelder, K. Ross & J.S. Schlipf (1988): Unfounded sets and well–founded semantics for general logic programs. In Proceedings of the 7^{th} ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pp. 221–230. Alternatively see The wellfounded semantics for general logic programs, JACM 38(3), pp. 620–650, 1991.

[7] M. Gelfond & V. Lifschitz (1988): The stable model semantics for logic programming. In R. Kowalski & K. Bowen, editors: Proceedings 5^{th} International Conference on Logic Programming, MIT Press, Cambridge, Massachusetts, pp. 1070–1080.

[8] J.F. Groote (1993): Transition system specifications with negative premises. Theoretical Computer Science 118(2), pp. 263–299.

[9] J.F. Groote & F.W. Vaandrager (1992): Structured operational semantics and bisimulation as a congruence. Information and Computation 100(2), pp. 202–260.

[10] G.D. Plotkin (1981): A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University.

[11] T.C. Przymusinski (1988): On the declarative semantics of deductive databases and logic programs. In Jack Minker, editor: Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann Publishers, Inc., Los Altos, California, pp. 193–216.

[12] T.C. Przymusinski (1990): The well-founded semantics coincides with the three-valued stable semantics. Fundamenta Informaticae XIII(4), pp. 445–463.

[13] C. Verhoef (1994): A congruence theorem for structured operational semantics with predicates and negative premises. In B. Jonsson & J. Parrow, editors: Proceedings CONCUR 94, Uppsala, Sweden, LNCS 836, Springer-Verlag, pp. 433–448.