Home | Search | Help  
Home Page Università di Genova

Technical Report Details

Date 6-6-2005
Number DISI-TR-05-09
Title On the Expressiveness of Multiset Rewriting with Gap-order Constraints
Authors Giorgio Delzanno
Bibtex Entry
E-mail giorgio@disi.unige.it
Link http://www.disi.unige.it/person/DelzannoG/MSR/DelGAP.ps.gz
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.
Back to Technical Reports