Menu
A graph is called supermagic if it admits a labeling of its edges by consecutive integers such that the sum of the labels of the edges incident with a vertex is independent of the particular vertex. In this paper we prove that the necessary conditions for an \(r\)-regular supermagic graph of order \(n\) to exist are also sufficient. All proofs are constructive and they are based on finding supermagic labelings of circulant graphs.A parameterized system consists of several similar processes whose number is determined by an input parameter. A challenging problem is to provide methods for the uniform verification of such systems, i.e., to show by a single proof that a system is correct for any value of the parameter.
This paper presents a method for verifying parameterized systems using predicate diagrams. Basically, predicate diagrams are graphs whose vertices are labelled with first-order formulas, representing sets of system states, and whose edges represent possible system transitions. These diagrams are used to represent the abstractions of parameterized systems described by specifications written in temporal logic.
This presented method integrates deductive verification and algorithmic techniques. Non-temporal proof obligations establish the correspondence between the original specification and the diagram, whereas model checking is used to verify properties over finite-state abstractions.