Soundness Verification of Data-Aware Process Models with Variable-to-Variable Conditions

Traditionally Business Process Modeling has only focused on the control-flow perspective, thus allowing process designers to specify the constraints on the activities of the process: the order and potential concurrency of their execution, their mutual exclusivity, the possibility of being repeated, etc. However, activities are executed by different resources, manipulate data objects and are constrained by the state of such objects. This requires that the traditional notion of soundness, typically introduced for control-flow-only models, is extended so as to consider data. Intuitively, a (data-aware) process model is sound if (1) it does not contain deadlocks, (2) no more activities are enabled when the process instance is marked as completed and finally (3) there are no parts of the model that cannot be executed. Although several data-aware notations have been introduced in the literature, not all of these are given a formal semantics. In this paper, we propose a technique for checking the data-aware soundness for a specific class of such integrated models, with a simple syntax and semantics, building on Data Petri Nets (DPNs). These are Petri nets enriched with case variables, where transitions are guarded by formulas that inspect and update such variables, and are of the form variable-operator-variable or variable-operator-constant. Even though DPNs are less expressive than Petri nets where data are carried by tokens, they elegantly capture business processes operating over simple case data, allowing to model complex data-aware decisions. We show that, if a DPN is data-aware sound, the Constraint Graph is a finite-state automaton; however, a finite-state Constraint Graph does not guarantee data-aware soundness, but provides a finite structure through which this property can be checked. Finally, we investigate further properties beyond data-aware soundness, such as the problem of verifying that an actor participating in the business process can unilaterally enforce data-aware soundness by restricting the possible executions of a bounded DPN, assuming this actor to be able to control the firing of some transitions and decide the value of some of the case variables whenever these are updated.

Graph SLAM Built over Point Clouds Matching for Robot Localization in Tunnels

This paper presents a fully original algorithm of graph SLAM developed for multiple environments—in particular, for tunnel applications where the paucity of features and the difficult distinction between different positions in the environment is a problem to be solved. This algorithm is modular, generic, and expandable to all types of sensors based on point clouds generation. The algorithm may be used for environmental reconstruction to generate precise models of the surroundings. The structure of the algorithm includes three main modules. One module estimates the initial position of the sensor or the robot, while another improves the previous estimation using point clouds. The last module generates an over-constraint graph that includes the point clouds, the sensor or the robot trajectory, as well as the relation between positions in the trajectory and the loop closures.

Representing Fitness Landscapes by Valued Constraints to Understand the Complexity of Local Search

Local search is widely used to solve combinatorial optimisation problems and to model biological evolution, but the performance of local search algorithms on different kinds of fitness landscapes is poorly understood. Here we consider how fitness landscapes can be represented using valued constraints, and investigate what the structure of such representations reveals about the complexity of local search. First, we show that for fitness landscapes representable by binary Boolean valued constraints there is a minimal necessary constraint graph that can be easily computed. Second, we consider landscapes as equivalent if they allow the same (improving) local search moves; we show that a minimal constraint graph still exists, but is NP-hard to compute. We then develop several techniques to bound the length of any sequence of local search moves. We show that such a bound can be obtained from the numerical values of the constraints in the representation, and show how this bound may be tightened by considering equivalent representations. In the binary Boolean case, we prove that a degree 2 or treestructured constraint graph gives a quadratic bound on the number of improving moves made by any local search; hence, any landscape that can be represented by such a model will be tractable for any form of local search. Finally, we build two families of examples to show that the conditions in our tractability results are essential. With domain size three, even just a path of binary constraints can model a landscape with an exponentially long sequence of improving moves. With a treewidth-two constraint graph, even with a maximum degree of three, binary Boolean constraints can model a landscape with an exponentially long sequence of improving moves.

A bottom-up algorithm for solving ♯2SAT

Counting models for a two conjunctive formula (2-CF) $F$, a problem known as $\sharp $2Sat, is a classic $\sharp $P complete problem. Given a 2-CF $F$ as input, its constraint graph $G$ is built. If $G$ is acyclic, then $\sharp $2Sat($F$) can be computed efficiently. In this paper, we address the case when $G$ has cycles. When $G$ is cyclic, we propose a decomposition on the constraint graph $G$ that allows the computation of $\sharp $2Sat($F$) in incremental way. Let $T$ be a cactus graph of $G$ containing a maximal number of independent cycles, and let $\overline{T}=(E(G)-E(T))$ be a subset of frond edges from $G$. The clauses in $\overline{T}$ are ordered in connected components $\{K_1, \ldots , K_r\}$. Each $(G \cup K_i), i=1,\ldots ,r$ is a knot (a set of intersected cycles) of the graph. The arrangement of the clauses of $\overline{T}$ allows the decomposition of $G$ in knots and provides a way of computing $\sharp $2Sat(F) in an incremental way. Our procedure has a bottom-up orientation for the computation of $\sharp $2Sat($F$). It begins with $F_0 = T$. In each iteration of the procedure, a new clause $C_i \in \overline{T}$ is considered in order to form $F_i = (F_{i-1} \wedge C_i)$ and then to compute $\sharp $2Sat$(F_i)$ based on the computation of $\sharp $2Sat$(F_{i-1})$.

Finding the Key Structure of Mechanical Parts with Formal Concept Analysis

Aiming at the problem that the assembly body model is difficult to classify and retrieve (large information redundancy and poor data consistency), an assembly body retrieval method oriented to key structures was presented. In this paper, a decision formal context is transformed from the 3D structure model. The 3D assembly structure model of parts is defined by the adjacency graph of function surface and qualitative geometric constraint graph. The assembly structure is coded by the linear symbol representation of compounds in chemical database. An importance or cohesion as the weight to a decision-making objective on the context is defined by a rough set method. A weighted concept lattice is introduced on it. An important formal concept means a key structure, since the concept represents the relations between parts’ function surfaces. It can greatly improve the query efficiency.

Research on Rapid Assembly Technology of Helicopter Transmissions

Research and application of rapid assembly technology can widely improve the design efficiency of helicopter transmissions. An assembly model of helicopter transmissions is presented by introducing Geometric Constraint Graph (GCG) method. A hierarchical model is obtained by multi-shrink decomposition. A corresponding data structure is generated according to the hierarchical model. CATIA based a parametric component database is built up. The Assembly modelling software is implemented by using VB. Finally, a helicopter transmissions example is taken as application and the rapid assembly for helicopter transmission system is achieved.