Proper Augmented Marked Graphs : Properties, Characterizations and Applications
Augmented marked graphs possess a special structure for modelling distributed systems with shared resources. Not only inheriting the desirable properties of augmented marked graphs such as on liveness and reversibility, proper augmented marked graphs also exhibit other desirable properties, including boundedness and conservativeness. However, proper augmented marked graphs have a rather complicated definition that inevitably undermines the usability in system modelling. In this paper, based on composition of live and bounded marked graphs, new characterizations for proper augmented marked graphs are devised. Through these characterizations, proper augmented marked graphs can be effectively used in modelling and analyzing conflicting processes of a distributed system. Applications to distributed transaction processing with shared resources are discussed.