The number of states is a very important matter for model checking approach in Petri net's analysis. We first gave a formal definition of state number calculation problem: For a Petri net with an initial state (marking), how many states does it have? Next we showed the problem cannot be solved in polynomial time for a popular subclass of Petri nets, known as free choice workflow nets, if P≠NP. Then we proposed a polynomial time algorithm to solve the problem by utilizing a representational bias called as process tree. We also showed effectiveness of the algorithm through an application example.

In this study, flexible organic solar cells (OSCs) employing a solution-processed hole-transporting layer (HTL) and low temperature annealing active layer have been fabricated. Vanadium oxide (V$_{2}$O$_{5})$, poly(3,4-ethylene dioxythiophene):poly(styrene sulfonate) (PEDOT:PSS), V$_{2}$O$_{5}$/PEDOT:PSS or PEDOT:PSS/V$_{2}$O$_{5}$ is used as the HTL. Poly(3-hexythiophene) (P3HT):[6,6]-phenyl C61-butyric acid methyl ester (PCBM) is used as the active layer. HTL and active layer are all formed by a spin coating method on polyethylene terephthalate (PET) substrates. The OSC configuration has been optimized in the study to be PET/ITO/V$_{2}$O$_{5}$/PEDOT:PSS/P3HT:PCBM/LiF/Al. Based on a low annealing temperature of 90$^{circ}$C for P3HT:PCBM and parameters optimization of solution-processed V$_{2}$O$_{5}$/PEDOT:PSS, the OSC demonstrates a current density (JSC) and power conversion efficiency (PCE) of 6.08, mA/cm$^{2}$ and 1.57%, while an OSC without the HTL has PCE around 0.06%. The V$_{2}$O$_{5}$/PEDOT:PSS stacked HTL provides not only a stepwise hole-transporting energy diagram configuration but a smooth film surface for coating P3HT:PCBM active layer, which subsequently increases charge carrier transporting capability and extracts holes from the active layer to the anode.

Orthogonal frequency division multiplexing (OFDM) has great advantages of high spectrum efficiency and robustness against multipath fading. When the received signal is deeply suppressed by deep fading, path loss and shadowing, the received carrier power must be increased in order to avoid degrading communication quality and provide high reliability at the cost of lower system throughput. A repetition coding is very attractive in providing the high reliability with simple configuration and the low decoding complexity of maximal ratio combining. In order to analytically confirm the effectiveness of repetition coded OFDM systems, we theoretically analyze the effect of increasing the number of repetitions (diversity branches) and acquiring both time and frequency diversity gain, and then derive a closed-form equation of average bit error rate (BER) to easily but precisely evaluate the performance.

Network traffic load usually differs significantly at different times of a day due to users' different time-preference. Network congestion may happen in traffic peak times. In order to prevent this from happening, network service providers (NSPs) can either over-provision capacity for demand at peak times of the day, or use dynamic time-dependent pricing (TDP) scheme to reduce the demand at traffic peak times. Since over-provisioning network capacity is costly, many researchers have proposed TDP schemes to control congestion as well as to improve the revenue of NSPs. To the best of our knowledge, all the studies on TDP schemes consider only the monopoly or duopoly NSP case. In our previous work, the duopoly NSP case has been studied with the assumption that each NSP has complete information of quality of service (QoS) of the other NSP. In this paper, an oligopoly NSP case is studied. NSPs try to maximize their overall revenue by setting time-dependent price, while users choose NSPs by considering their own time preference, congestion status in the networks and the price set by the NSPs. The interactions among NSPs are modeled as an oligopoly Bertrand game. Firstly, assuming that each NSP has complete information of QoS of all NSPs, a unique Nash equilibrium of the game is established under the assumption that users' valuation of QoS is uniformly distributed. Secondly, the assumption of complete information of QoS of all NSPs is relaxed, and a learning algorithm is proposed for NSPs to achieve the Nash equilibrium of the game. Analytical and experimental results show that NSPs can benefit from TDP scheme, however, not only the competition effect but also the incomplete information among NSPs causes revenue loss for NSPs under the TDP scheme.

The maturation of inhibitory transmission through γ-aminobutyric acid (GABA) is required to induce ocular dominance (OD) plasticity in the visual cortex. However, only circuits that are mediated by specific GABAA receptors can selectively elicit OD plasticity, implying a role of local circuits involved in GABA inhibition in this process. In this study, in order to theoretically examine the effects of such local pathways associated with cortical inhibition on the induction of OD plasticity, we compared synaptic modification dynamics regulated by feedforward inhibition and those regulated by feedback inhibition. Feedforward inhibition facilitated competitive interactions between different groups of inputs conveying correlated activities, which were required for the emergence of experience-dependent plasticity. Conversely, feedback inhibition suppressed competitive interactions and prevented synapses from reflecting past sensory experience. Our results suggest that the balance between feedforward and feedback inhibition regulates the timing and level of cortical plasticity by modulating competition among synapses. This result suggests an importance of activity-dependent competition in experience-dependent OD plasticity, which is in line with the results of previous experiments.

The multislope ski-rental problem is an extension of the classical ski-rental problem, where the player has several options of paying both of a per-time fee and an initial fee, in addition to pure renting and buying options. Damaschke gave a lower bound of 3.62 on the competitive ratio for the case where arbitrary number of options can be offered. In this paper we propose a scheme that for the number of options given as an input, provides a lower bound on the competitive ratio, by extending the method of Damaschke. This is the first to establish a lower bound for each of the 5-or-more-option cases, for example, a lower bound of 2.95 for the 5-option case, 3.08 for the 6-option case, and 3.18 for the 7-option case. Moreover, it turns out that our lower bounds for the 3- and 4-option cases respectively coincide with the known upper bounds. We therefore conjecture that our scheme in general derives a matching lower and upper bound.

A workflow may be extended to adapt to market growth, legal reform, and so on. The extended workflow must be logically correct, and inherit the behavior of the existing workflow. Even if the extended workflow inherits the behavior, it may be not logically correct. Can we modify it so that it satisfies not only behavioral inheritance but also logical correctness? This is named behavioral inheritance preserving soundizability problem. There are two kinds of behavioral inheritance: protocol inheritance and projection inheritance. In this paper, we tackled protocol inheritance preserving soundizability problem using a subclass of Petri nets called workflow nets. Limiting our analysis to acyclic free choice workflow nets, we formalized the problem. And we gave a necessary and sufficient condition on the problem, which is the existence of a key structure of free choice workflow nets called TP-handle. Based on this condition, we also constructed a polynomial time procedure to solve the problem.

A service-oriented architecture builds the entire system using a combination of independent software components. Such an architecture can be applied to a wide variety of computer systems. The problem of synthesizing service implementation models from choreography representing the overall specifications of service interaction is known as the choreography realization problem. In automatic synthesis, software models should be simple enough to be easily understood by software engineers. In this paper, we discuss a semi-formal method for synthesizing hierarchical state machine models for the choreography realization problem. The proposed method is evaluated using metrics for intelligibility.

In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.

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.

In this paper, we propose a time and memory efficient Ultra Wide Band Short Range Radar (UWB SRR) system for measuring relative target velocities of up to 150km/hr. First, for the proposed detector, we select the required design parameters for good performance. The parameters are the number of coherent integrations, non-coherent integrations, and FFT points. The conventional detector uses a Fast Fourier Transform (FFT) to extract the range and velocity of the target simultaneously. Therefore, it requires high computation effort, high FFT processing time, and a huge amount of memory. However, the proposed pulse radar detector first decides the target range and then computes the target velocity using FFT sequentially for the decided range index. According to our theoretical and simulation analyses, the FFT processing time and the memory requirement are reduced compared to those of the conventional method. Finally, we show that the detection performance of the proposed detector is superior to that of the conventional detector in a background of Additive White Gaussian Noise (AWGN).

Due to network users' different time-preference, network traffic load usually significantly differs at different time. In traffic peak time, network congestion may happen, which make the quality of service for network users deteriorate. There are essentially two ways to improve the quality of services in this case: (1) Network service providers (NSPs) over-provision network capacity by investment; (2) NSPs use time-dependent pricing (TDP) to reduce the traffic at traffic peak time. However, over-provisioning network capacity can be costly. Therefore, some researchers have proposed TDP to control congestion as well as improve the revenue of NSP. But to the best of our knowledge, all of the literature related time-dependent pricing scheme only consider the monopoly NSP case. In this paper, a duopoly NSP case is studied. The NSPs try to maximize their overall revenue by setting time-dependent price, while users choose NSP by considering their own preference, congestion status in the networks and the price set by the NSPs. Analytical and experimental results show that the TDP benefits the NSPs, but the revenue improvement is limited due to the competition effect.

Wireless sensor network (WSN) using network coding is vulnerable to pollution attacks. Existing authentication schemes addressing this attack either burden the sensor node with a higher computation overhead, or fail to provide an efficient way to mitigate two recently reported attacks: tag pollution attacks and repetitive attacks, which makes them inapplicable to WSN. This paper proposes an efficient hybrid cryptographic scheme for WSN with securing network coding. Our scheme can resist not only normal pollution attacks, but the emerging tag pollution and repetitive attacks in an efficient way. In particular, our scheme is immediately suited for distributing multiple generations using a single public key. Experimental results show that our scheme can significantly improve the computation efficiency at a sensor node under the two above-mentioned attacks.

Petri nets are a kind of formal language that are widely applied in concurrent systems associated with resource allocation due to their abilities of the natural description on resource allocation and the precise characterization on deadlock. Weighted System of Simple Sequential Processes with Resources (WS3PR) is an important subclass of Petri nets that can model many resource allocation systems in which 1) multiple processes may run in parallel and 2) each execution step of each process may use multiple units from a single resource type but cannot use multiple resource types. We first prove that the liveness problem of WS3PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS3PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS3PR is live iff each SCW has no BM. A sufficient condition is also proposed to guarantee that an SCW has no BM. Additionally, we show some advantages of using SCW to analyze the deadlock problem compared to other siphon-based ones, and discuss the relation between SCW and siphon. These results are valuable to the further research on the deadlock prevention or avoidance for WS3PR.

The simple repetitive control system proposed by Yamada et al. is a type of servomechanism for periodic reference inputs. This system follows a periodic reference input with a small steady-state error, even if there is periodic disturbance or uncertainty in the plant. In addition, simple repetitive control systems ensure that transfer functions from the periodic reference input to the output and from the disturbance to the output have finite numbers of poles. Yamada et al. clarified the parameterization of all stabilizing simple repetitive controllers. Recently, Yamada et al. proposed the parameterization of all stabilizing two-degrees-of-freedom (TDOF) simple repetitive controllers that can specify the input-output characteristic and the disturbance attenuation characteristic separately. However, when using the method of Yamada et al., it is complex to specify the low-pass filter in the internal model for the periodic reference input that specifies the frequency characteristics. This paper extends the results of Yamada et al. and proposes the parameterization of all stabilizing TDOF simple repetitive controllers with specified frequency characteristics in which the low-pass filter can be specified beforehand.

Parametric images can help investigate disease mechanisms and vital functions. To estimate parametric images, it is necessary to obtain the tissue time activity curves (tTACs), which express temporal changes of tracer activity in human tissue. In general, the tTACs are calculated from each voxel's value of the time sequential PET images estimated from dynamic PET data. Recently, spatio-temporal PET reconstruction methods have been proposed in order to take into account the temporal correlation within each tTAC. Such spatio-temporal algorithms are generally quite computationally intensive. On the other hand, typical algorithms such as the preconditioned conjugate gradient (PCG) method still does not provide good accuracy in estimation. To overcome these problems, we propose a new spatio-temporal reconstruction method based on the dynamic row-action maximum-likelihood algorithm (DRAMA). As the original algorithm does, the proposed method takes into account the noise propagation, but it achieves much faster convergence. Performance of the method is evaluated with digital phantom simulations and it is shown that the proposed method requires only a few reconstruction processes, thereby remarkably reducing the computational cost required to estimate the tTACs. The results also show that the tTACs and parametric images from the proposed method have better accuracy.

This paper considers online vertex exploration problems in a simple polygon where starting from a point in the inside of a simple polygon, a searcher is required to explore a simple polygon to visit all its vertices and finally return to the initial position as quickly as possible. The information of the polygon is given online. As the exploration proceeds, the searcher gains more information of the polygon. We give a 1.219-competitive algorithm for this problem. We also study the case of a rectilinear simple polygon, and give a 1.167-competitive algorithm.

A Boolean network model is one of the models of gene regulatory networks, and is widely used in analysis and control. Although a Boolean network is a class of discrete-time nonlinear systems and expresses the synchronous behavior, it is important to consider the asynchronous behavior. In this paper, using a Petri net, a new modeling method of asynchronous Boolean networks with control inputs is proposed. Furthermore, the optimal control problem of Petri nets expressing asynchronous Boolean networks is formulated, and is reduced to an integer programming problem. The proposed approach will provide us one of the mathematical bases of control methods for gene regulatory networks.

A timed Petri net, an extended model of an ordinary Petri net with introduction of discrete time delay in firing activity, is practically useful in performance evaluation of real-time systems and so on. Unfortunately though, it is often too difficult to solve (efficiently) even most basic problems in timed Petri net theory. This motivates us to do research on analyzing complexity of Petri net problems and on designing efficient and/or heuristic algorithms. The minimum initial marking problem of timed Petri nets (TPMIM) is defined as follows: “Given a timed Petri net, a firing count vector X and a nonnegative integer π, find a minimum initial marking (an initial marking with the minimum total token number) among those initial ones M each of which satisfies that there is a firing scheduling which is legal on M with respect to X and whose completion time is no more than π, and, if any, find such a firing scheduling.” In a production system like factory automation, economical distribution of initial resources, from which a schedule of job-processings is executable, can be formulated as TPMIM. The subject of the paper is to propose two pseudo-polynomial time algorithms TPM and TMDLO for TPMIM, and to evaluate them by means of computer experiment. Each of the two algorithms finds an initial marking and a firing sequence by means of algorithms for MIM (the initial marking problem for non-timed Petri nets), and then converts it to a firing scheduling of a given timed Petri net. It is shown through our computer experiments that TPM has highest capability among our implemented algorithms including TPM and TMDLO.

In our privious paper, we proposed an algorithm that determines delay times of a timed Petri net from the structural information of a signaling pathway, but Petri net structures containing cycles and inhibitory arcs were not considered. This paper provides conditions for cycle-contained Petri nets to have reasonable delay times. Furthermore, handling of inhibitory arcs are discussed in terms of the reaction rate of inhibitory interaction in signaling pathway, especially the conversion process of Petri net with inhibitory arc to the one without inhibitory arc is given.