| Abstract |
Gap-order constraints are a subclass of difference
constraints introduced in the field of constraint databases.
When incorporated within multiset rewriting, they can be used to specify
concurrent systems with an arbitrary number of components each one with
integer data paths and weak form of update of local states.
In this paper we study the expressive power of the specification language
\MSRGAP~resulting from this combination.
Our main result is that the expressiveness of the monadic fragment of \MSRGAP~
lies between Petri Nets and Turing Machines.
The undecidability of reachability distinguishes monadic
\MSRGAP~from Petri Nets.
The decidability of control state reachability distinguishes
monadic \MSRGAP~from Turing Machines.
Thus our investigations identify a class of infinite state systems
more expressive than Petri Nets for which problems related to
the automated verification of safety properties are still decidable. |
