Next: An example: The Ticket Up: Constraint Multiset Rewriting Previous: Constraint Systems

## The language

In the following we will use the notion of multisets. We use and to denote multiset union and multiset difference, respectively.

Let be a finite set of predicate symbols, and a denumerable set of variables. An atomic formula over and has the form (with ), where , and are distinct variables in .

Now, let be a finite set of predicate symbols, and a denumerable set of variables. A multiset of atomic formulas , ..., (with ) over and , is indicated as , where and must have distinct variables for , and is an associative and commutative constructor. The empty multiset is denoted by .

In the rest of the paper will use , , to denote multisets of atomic formulas.

Let be a finite set of predicate symbols, and a constraint system. An rule over and has the form , where and are two multisets of atomic formulas over and , with distinct variables, and .

Note that and are possible rules.

In order to make the intuitive semantics of the previous specification precise, we introduce the ingredients for the operational reading of MSR rules. We first define the notion of ground formulas. Let be a finite set of predicate symbols, and a constraint system. A ground atomic formulas over and has the form (with ), where and .

In the following, we will denote by the application of a solution to a multiset of atomic formulas . Formally, , and if for and , .

Given an rule , over and , the set of ground instances of , denoted , is the set of ground multiset rewrite rules defined as follows:

A central notion for our semantics is that of current configuration given below.

Let be a finite set of predicate symbols, and a constraint system. An configuration is a multiset of ground atomic formulas over and .

Configurations can be ordered with respect multiset inclusion as follows. Given two multisets of atomic formulas if and only if for every atomic formula , where denotes the number of occurrences of in .

An specification is defined as follows.

The operational semantics of an specification can be defined as follows. Let be a configuration. A rule from is enabled at via the solution of the constraint if and only if .

Now, sup.pngpose is enabled at via . Firing this rule at yields the new configuration , written , if and only if , and .

A run is a sequence of configurations with and for which there exist such that for .

Let a set of configurations. The successor operator is defined as

whereas, the predecessor operator is defined as

The reflexive and transitive closures of the predecessor and successor operators are denoted and , respectively.

The reachability set is defined as , being the initial states of the specification under consideration.

Next: An example: The Ticket Up: Constraint Multiset Rewriting Previous: Constraint Systems
Giorgio Delzanno 2003-02-03