It has become common practice for software projects to adopt third-party dependencies. Developers are encouraged to update any outdated dependency to remain safe from potential threats of vulnerabilities. In this study, we present an approach to aid developers show whether or not a vulnerable code is reachable for JavaScript projects. Our prototype, SōjiTantei, is evaluated in two ways (i) the accuracy when compared to a manual approach and (ii) a larger-scale analysis of 780 clients from 78 security vulnerability cases. The first evaluation shows that SōjiTantei has a high accuracy of 83.3%, with a speed of less than a second analysis per client. The second evaluation reveals that 68 out of the studied 78 vulnerabilities reported having at least one clean client. The study proves that automation is promising with the potential for further improvement.

This paper introduces methods to modify a buggy sequential gate-level circuit to conform to the specification. In order to preserve the optimization efforts, the modifications should be as small as possible. Assuming that the locations to be modified are given, our proposed method finds an appropriate set of fan-in signals for the patch function of those locations by iteratively calculating the state correspondence between the specification and the buggy circuit and applying a method for debugging combinational circuits. The experiments are conducted on ITC99 benchmark circuits, and it is shown that our proposed method can work when there are at most 30,000 corresponding reachable state pairs between two circuits. Moreover, a heuristic method using the information of data-path FFs is proposed, which can find a correct set of fan-ins for all the benchmark circuits within practical time.

Business process similarity measure is required by many applications, such as business process query, improvement, redesign, and etc. Many process behavior similarity measures have been proposed in the past two decades. However, to the best of our knowledge, most existing work only focuses on the direct causality transition relations and totally neglect the concurrent and transitive transition relations that are proved to be equally important when measuring process behavior similarity. In this paper, we take the weakness of existing process behavior similarity measures as a starting point, and propose a comprehensive approach to measure the business process behavior similarity based on the so-called Extended Transition Relation set, ETR-set for short. Essentially, the ETR-set is an ex-tended transition relation set containing direct causal transition relations, minimum concurrent transition relations and transitive causal transition relations. Based on the ETR-set, a novel process behavior similarity measure is defined. By constructing a concurrent reachability graph, our approach finds an effective technique to obtain the ETR-set. Finally, we evaluate our proposed approach in terms of its property analysis as well as conducting a group of control experiments.

Workflow nets (WF-nets for short) are a standard way to automate business processes. Well-Structured WF-nets (WS WF-nets for short) are an important subclass of WF-nets because they have a well-balanced capability to expression power and analysis power. In this paper, we revealed structural and behavioral properties of WS WF-nets. Our results on structural properties are: (i) There is no EFC but non-FC WF-net in WS WF-nets; (ii) A WS WF-net is sound iff it is a van Hee et al.'s ST-net. Our results on behavioral properties are: (i) Any WS WF-net is safe; (ii) Any WS WF-net is separable; (iii) A necessary and sufficient condition on reachability of sound WS WF-net (N,[pIk]). Finally we illustrated the usefulness of the proposed properties with an application example of analyzing workflow evolution.

Petri Net (PN) is a frequently-used model for deadlock detection. Among various detection methods on PN, reachability analysis is the most accurate one since it never produces any false positive or false negative. Although suffering from the well-known state space explosion problem, reachability analysis is appropriate for small- and medium-scale programs. In order to mitigate the explosion problem several kinds of techniques have been proposed aiming at accelerating the reachability analysis, such as net reduction and abstraction. However, these techniques are for general PN and do not take the particularity of application into consideration, so their optimization potential is not adequately developed. In this paper, the feature of mutual exclusion-based program is considered, therefore several strategies are proposed to accelerate the reachability analysis. Among these strategies a customized net reduction rule aims at reducing the scale of PN, two marking compression methods and two pruning methods can reduce the volume of reachability graph. Reachability analysis on PN can only report one deadlock on each path. However, the reported deadlock may be a false alarm in which situation real deadlocks may be hidden. To improve the detection efficiency, we proposed a deadlock recovery algorithm so that more deadlocks can be detected in a shorter time. To validate the efficiency of these methods, a prototype is implemented and applied to SPLASH2 benchmarks. The experimental results show that these methods accelerate the reachability analysis for mutual exclusion-based deadlock detection significantly.

Geocast communication provides efficient group communication services to distribute information to terminals that exist in some geographical domain. For various services which use geocast communication, ad hoc network is useful as network structure. Ad hoc networks are a kind of self-organing network where terminals communicate directly with each other without network infrastructure. For ad hoc networks, terminal power saving is an important issue, because terminals are driven by the battery powered system. One approach for this issue is reducing the radio transmission range of each terminal, but it degrades reachability of user data for each terminal. In this paper, we propose a design method for radio transmission range using the target problem to improve both terminal power saving and reachability for geocast communication in an ad hoc network. Moreover, we evaluate the proposed method considering both routing protocols and media access control protocols, and clarify the applicability of the proposed method to communication protocols.

Analysis of security governed by dynamics of power systems, which we refer to as dynamic security analysis, is a primary but challenging task because of its hybrid nature, that is, nonlinear continuous-time dynamics integrated with discrete switchings. In this paper, we formulate this analysis problem as checking the reachability of a mathematical model representing dynamic performances of a target power system. We then propose a computational approach to the analysis based on the so-called RRT (Rapidly-exploring Random Tree) algorithm. This algorithm searches for a feasible trajectory connecting an initial state possibly at a lower security level and a target set with a desirable higher security level. One advantage of the proposed approach is that it derives a concrete control strategy to guarantee the desirable security level if the feasible trajectory is found. The performance and effectiveness of the proposed approach are demonstrated by applying it to two running examples on power system studies: single machine-infinite system and two-area system for frequency control problem.

We study the problem of transforming one list (vertex) coloring of a graph into another list coloring by changing only one vertex color assignment at a time, while at all times maintaining a list coloring, given a list of allowed colors for each vertex. This problem is known to be PSPACE-complete for bipartite planar graphs. In this paper, we first show that the problem remains PSPACE-complete even for bipartite series-parallel graphs, which form a proper subclass of bipartite planar graphs. We note that our reduction indeed shows the PSPACE-completeness for graphs with pathwidth two, and it can be extended for threshold graphs. In contrast, we give a polynomial-time algorithm to solve the problem for graphs with pathwidth one. Thus, this paper gives sharp analyses of the problem with respect to pathwidth.

Workflow nets are a standard way for modeling and analyzing workflows. There are two aspects in a workflow: definition and instance. In form of workflow nets, a workflow definition and a workflow instance are respectively represented as a net structure and a marking. The correctness of the workflow definition can be checked by using a workflow nets' property, called soundness. On the other hand, the correctness of the workflow instance can be checked by using a Petri nets' well-known property, called reachability. The reachability problem is known to be intractable. In this paper, we have shown that the reachability problem for (i) sound extended free-choice workflow nets with a marking representing one workflow instance or (ii) acyclic well-structured workflow nets with a marking representing one or more workflow instances can be solved in polynomial time.

We study the problem of reconfiguring one list edge-coloring of a graph into another list edge-coloring by changing only one edge color assignment at a time, while at all times maintaining a list edge-coloring, given a list of allowed colors for each edge. Ito, Kamiski and Demaine gave a sufficient condition so that any list edge-coloring of a tree can be transformed into any other. In this paper, we give a new sufficient condition which improves the known one. Our sufficient condition is best possible in some sense. The proof is constructive, and yields a polynomial-time algorithm that finds a transformation between two given list edge-colorings of a tree with n vertices via O(n2) recoloring steps. We remark that the upper bound O(n2) on the number of recoloring steps is tight, because there is an infinite family of instances on paths that satisfy our sufficient condition and whose reconfiguration requires Ω(n2) recoloring steps.

The marking construction problem (MCP) of Petri nets is defined as follows: “Given a Petri net N, an initial marking Mi and a target marking Mt, construct a marking that is closest to Mt among those which can be reached from Mi by firing transitions.” MCP includes the well-known marking reachability problem of Petri nets. MCP is known to be NP-hard, and we propose two schemas of heuristic algorithms: (i) not using any algorithm for the maximum legal firing sequence problem (MAX LFS) or (ii) using an algorithm for MAX LFS. Moreover, this paper proposes four pseudo-polynomial time algorithms: MCG and MCA for (i), and MCHFk and MC_feideq_a for (ii), where MCA (MC_feideq_a, respectively) is an improved version of MCG (MCHFk). Their performance is evaluated through results of computing experiment.

Communication-free Petri nets provide a net semantics for Basic Parallel Processes, which form a subclass of Milner's Calculus of Communicating Systems (CCS) a process calculus for the description and algebraic manipulation of concurrent communicating systems. It is known that the reachability problem for communication-free Petri nets is NP-complete. Lacking the synchronization mechanism, the expressive power of communication-free Petri nets is somewhat limited. It is therefore importance to see whether the power of communication-free Petri nets can be enhanced without sacrificing their analytical capabilities. As a first step towards this line of research, in this paper our main concern is to investigate, from the decidability/complexity viewpoint, the reachability problem for a number of variants of communication-free Petri nets, including communication-free Petri nets augmented with 'static priorities,' 'dynamic priorities,' 'states,' 'inhibitor arcs,' and 'timing constraints.'

A method for the exact cost performance analysis of autonomous discrete-time piecewise affine systems is presented. Cost performance refers to the average trajectory cost over the entire region of attraction of the origin. The trajectory cost is based on the infinite-horizon cost. First, a reverse reachability algorithm which constructs the explicit piecewise quadratic trajectory cost function over the entire region of attraction of the origin is presented. Then, an explicit expression for the integral of a quadratic function over a simplex of arbitrary dimension is derived. Thus, the piecewise quadratic trajectory cost function can be integrated exactly and efficiently in order to determine the cost performance of the system as a whole. This alleviates the need to perform a large number of simulations.

We propose an efficient reachability estimation scheme for group membership services in mobile ad hoc networks (MANETs). The periodical message exchange-based scheme, i.e., a typical reachability estimation scheme, requires message exchanges even when the reachability status does not change. It is presumed that the reachability between nodes is maintained while the nodes move around in a limited range. The proposed scheme exploits a virtual grid for the course-grained estimation. A region in the virtual grid can be used to represent the movement range which does not change the reachability. Each node calculates how long it will stay in a region, and issues the duration information only when it gets out of the current region.

Petri nets are known as a modeling language for concurrent and distributed systems. In recent years, various object-oriented Petri nets were proposed, and we are proposing a kind of object-oriented Petri nets, called multi agent nets (MANs). In this letter, we consider the reachability analysis of MANs. We propose an algorithm for generating an abstract state space of a multi agent net, and report results of computational experiments.

We can model embedded systems as hybrid systems. Moreover, they are distributed and real-time systems. Therefore, it is important to specify and verify randomness and soft real-time properties. For the purpose of system verification, we formally define probabilistic linear hybrid automaton and its symbolic reachability analysis method. It can describe uncertainties and soft real-time characteristics.

Petri nets are a well-known graphical and modeling tool for concurrent and distributed systems, and there have been many results on the theory, and also on practical applications. In the last decade, various Object-Oriented Petri nets (OO-nets) are proposed. As object orientation was adopted for programming languages, extension to OO-nets inspired from object-oriented programming is a natural flow. This article presents state-of-the-art on OO-nets.

We study the complexity of the reachability problem for a new subclass of Petri nets called simple-circuit Petri nets, which properly contains several well known subclasses such as conflict-free, BPP, normal Petri nets and more. A new decomposition approach is applied to developing an integer linear programming formulation for characterizing the reachability sets of such Petri nets. Consequently, the reachability problem is shown to be NP-complete. The model checking problem for some temporal logics is also investigated for simple-circuit Petri nets.

Services that operate normally, independently, will behave differently when simultaneously initiated with another service. This behavior is called a feature interaction. A feature interaction, where the next state can not be determined uniquely for one event, is called a non-determinacy feature interaction. To detect the interaction, judgment has to be made as to whether the state, where the non-determinacy occurs, is reachable from the initial state or not. For the judgment, many methods have been proposed. But, still now, it is required huge computation time to judge the reachability. This paper proposes a new method to test the reachability using a little knowledge elicited beforehand. By using the proposed method computation time was reduced drastically. Besides, by applying the proposed method to a benchmark, the proposed method was confirmed to be effective and reasonable.

We give an overview of the computational complexity of linear and mesh-connected cellular and iterative arrays with respect to well known models of sequential and parallel computation. We discuss one-way communication versus two-way communication, serial input versus parallel input, and space-efficient simulations. In particular, we look at the parallel complexity of cellular arrays in terms of the PRAM theory and its implications, e.g., to the parallel complexity of recurrence equations and loops. We also point out some important and fundamental open problems that remain unresolved. Next, we investigate the solvability of some reachability and safety problems concerning machines operating in parallel and cite some possible applications. Finally, we briefly discuss the complexity of the "commutativity analysis" technique that is used in the areas of parallel computing and parallelizing compilers.