Cyclic vertex connectivity cκ and cyclic edge connectivity cλ are two important kinds of conditional connectivity, which reflect the number of vertices or edges that can be removed before the graph is disconnected and at least two components contain a cycle, respectively. They have important applications in various networks such as computer networks or biochemical networks. In addition, a fullerene is a special kind of molecule in chemistry. A classic fullerene graph is a 3-connected cubic planar graph with only pentagonal and hexagonal faces. (4, 5, 6)-fullerene graphs are atypical fullerene graphs which also contain 4-faces. In this paper, we prove that cκ=cλ for (4,5,6)-fullerene graphs except for four exceptional graphs with order less than 16. We also give O(ν)-algorithms to determine the cyclic vertex connectivity and the cyclic edge connectivity of (4,5,6)-fullerene graphs.

AI-based process model analysis has attracted more and more interest. Model quality is crucial for such research. At present, inter-organizational business process (IOBP) has been widely used in the model design and development of the distributed system. Before implementing the intelligent analysis of the IOBP model, conformance as a foundation for model quality checking plays a key role because it ensures in advance that the participants can successfully interact without violating the global communication constraints imposed by the choreography. In fact, the multi-instance participant is a common requirement in IOBP. This paper provides a formal approach and framework supporting the conformance between BPMN choreography and collaboration while considering multi-instance participants and message communication modes. As a core, the formalization proposed is based on BNF syntax and structured CSP# processes. It can well support multi-instance features and multiple communication modes. Combined with CSP#, the formal definitions of communication modes and verification properties are given. On this basis, an integrated framework is provided to support automated formal verification referring to multiple communication modes. Finally, a set of experiments is conducted to demonstrate the effectiveness of the proposal.

In the study of cycles and paths, the meta-conjecture of Bondy that sufficient conditions for Hamiltonicity often imply pancyclicity has motivated research on the existence of cycles and paths of many lengths. Hendry further introduced the stronger concepts of cycle extendability and path extendability, which require that every cycle or path can be extended to another one with one additional vertex. These concepts have been studied extensively, but there exist few results on path extendability in digraphs, as far as we know. In this paper, we make the first attempt in this direction. We establish a number of extremal and degree conditions for path extendability in general digraphs. Moreover, we prove that every path of length at least two in a regular tournament is extendable, with some exceptions. One of our proof approaches is a new contraction operation to transform nonextendable paths into nonextendable cycles.