scholarly journals Structural Invariants for the Verification of Systems with Parameterized Architectures

Author(s):  
Marius Bozga ◽  
Javier Esparza ◽  
Radu Iosif ◽  
Joseph Sifakis ◽  
Christoph Welzel
2019 ◽  
Vol 141 (10) ◽  
Author(s):  
Rajneesh Kumar Rai ◽  
Sunil Punjabi

Isomorphism (structural similarity) of kinematic chains (KCs) of mechanisms is an important issue in the structural synthesis, which must be identified to avoid the duplicate structures. Duplication causes incorrect family size, i.e., distinct KCs with a given number of links (n) and degree of freedom (dof). Besides simple joints kinematic chains (SJKCs), multiple joints kinematic chains (MJKCs) are also widely used because of their compact size and the methods dealing with such KCs are few. The proposed method deals with two different structural invariants, i.e., primary structural invariants (provide only the necessary condition of isomorphism), such as link connectivity number (LCN) of all the links, link connectivity number of chain (CCN), joint connectivity number (JCN) of all the joints, and joint connectivity number of chain (JCNC), and secondary structural invariants (provide the sufficient condition of isomorphism), such as power transmission (P) and transmission efficiency (Te). Primary structural invariants are calculated using a new link–link connectivity matrix (LLCM), whereas secondary structural invariants are calculated using the concept of entropy of information theory. The method has been successfully tested for 10 and 11 links MJKCs (illustrative examples taken in the paper) and for the families of 18 MJKCs with 8 links, 2 MJs, 1-dof, and 3 independent loops; 22 MJKCs with 8 links, 1 MJ, 1-dof, and 3 independent loops; and 83 MJKCs with 9 links, 1 MJ, 2-dof, and 3 independent loops.


2014 ◽  
Vol 24 (2-3) ◽  
pp. 316-383 ◽  
Author(s):  
PIERRE-ÉVARISTE DAGAND ◽  
CONOR McBRIDE

AbstractProgramming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: We can finally write correct-by-construction software. However, this extreme accuracy is also a curse: A datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: The users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.


1998 ◽  
Vol 53 (8) ◽  
pp. 699-703 ◽  
Author(s):  
Ivan Gutman ◽  
Sven J. Cyvina ◽  
Vesna Ivanov-Petrović

Abstract The regular-hexagon-shaped benzenoid hydrocarbons: B1 = benzene (C6H6), B2 = coronene (C24H12), B3 = circumcoronene (C54H18), B4 = circumcircumcoronene (C150H30), etc. possess unique topological properties. General expressions for the most important of such properties (number of fun-damental structural invariants, number of Kekule and Clar structures, number of aromatic sextets, Wiener and Szeged indices, spectral moments) are given, including a number of results that are communicated here for the first time. Cyclic conjugation in circumcoronenes is analyzed by means of its energy-effect, and found to agree with the predictions of Clar's aromatic sextet theory only in the case of B1 and B2.


1991 ◽  
Vol 179 (1-2) ◽  
pp. 21-28 ◽  
Author(s):  
S. Nikolić ◽  
N. Trinajstić ◽  
Z. Mihalić ◽  
S. Carter

Mathematics ◽  
2018 ◽  
Vol 6 (10) ◽  
pp. 174
Author(s):  
Allen D. Parks

It is shown that the set of all networks of fixed order n form a semigroup that is isomorphic to the semigroup BX of binary relations on a set X of cardinality n. Consequently, BX provides for Green’s L,R,H, and D equivalence classifications of all networks of fixed order n. These classifications reveal that a fixed-order network which evolves within a Green’s equivalence class maintains certain structural invariants during its evolution. The “Green’s symmetry problem” is introduced and is defined as the determination of all symmetries (i.e., transformations) that produce an evolution between an initial and final network within an L or an R class such that each symmetry preserves the required structural invariants. Such symmetries are shown to be solutions to special Boolean equations specific to each class. The satisfiability and computational complexity of the “Green’s symmetry problem” are discussed and it is demonstrated that such symmetries encode information about which node neighborhoods in the initial network can be joined to form node neighborhoods in the final network such that the structural invariants required by the evolution are preserved, i.e., the internal dynamics of the evolution. The notion of “propensity” is also introduced. It is a measure of the tendency of node neighborhoods to join to form new neighborhoods during a network evolution and is used to define “energy”, which quantifies the complexity of the internal dynamics of a network evolution.


1999 ◽  
Vol 291 (1-3) ◽  
pp. 83-102 ◽  
Author(s):  
M. Isabel García-Planas ◽  
M. Dolors Magret

2000 ◽  
Vol 38 (4) ◽  
pp. 1033-1049 ◽  
Author(s):  
I. Baragaña ◽  
V. Fernández ◽  
I. Zaballa

Sign in / Sign up

Export Citation Format

Share Document