Reachability graph is a very important tool to analyze the dynamic properties of Petri nets, but the concurrent relation of transitions in Petri nets cannot be represented by reachability graph. Petri net is a concurr...Reachability graph is a very important tool to analyze the dynamic properties of Petri nets, but the concurrent relation of transitions in Petri nets cannot be represented by reachability graph. Petri net is a concurrent system, while reachability graph is a serial one. However, concurrency is a kind of property which is not only very significant but also difficult to be analyzed and controlled. This paper presents the concepts of concurrent reachable marking and concurrent reachable graph in order to represent and analyze the concurrent system. The algorithm constructing concurrent reachable marking set and concurrent reachability graph is also shown so that we can study the response problems among services in a network computing environment and analyze the throughput of the system. The Dining Philosophers Problem, which is a classic problem of describing the management of concurrent resources, is given as an example to illustrate the significance of concurrent reachability graph.展开更多
Logic Petri nets （LPNs） are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method fo...Logic Petri nets （LPNs） are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reach- able markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.展开更多
In order to guarantee the correctness of business processes, not only control-flow errors but also data-flow errors should be considered. The control-flow errors mainly focus on deadlock, livelock, soundness, and so o...In order to guarantee the correctness of business processes, not only control-flow errors but also data-flow errors should be considered. The control-flow errors mainly focus on deadlock, livelock, soundness, and so on. However, there are not too many methods for detecting data-flow errors. This paper defines Petri nets with data operations(PN-DO) that can model the operations on data such as read, write and delete. Based on PN-DO, we define some data-flow errors in this paper. We construct a reachability graph with data operations for each PN-DO, and then propose a method to reduce the reachability graph. Based on the reduced reachability graph, data-flow errors can be detected rapidly. A case study is given to illustrate the effectiveness of our methods.展开更多
Hybrid Petri nets(HPNs) are widely used to describe and analyze various industrial hybrid systems that have both discrete-event and continuous discrete-time behaviors. Recently,many researchers attempt to utilize them...Hybrid Petri nets(HPNs) are widely used to describe and analyze various industrial hybrid systems that have both discrete-event and continuous discrete-time behaviors. Recently,many researchers attempt to utilize them to characterize power and energy systems. This work proposes to adopt an HPN to model and analyze a microgrid that consists of green energy sources. A reachability graph for such a model is generated and used to analyze the system properties.展开更多
Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts wi...Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts with respect to a criterion for analyzing programs,and has been widely used in specification level for model reduction,but researches on slicing of Petri nets are still limited.According to the idea of program slicing,this paper extends slicing technologies of Petri nets to four kinds of slices,including backward static slice,backward dynamic slice,forward static slice and forward dynamic slice.Based on the structure properties,the algorithms of obtaining two kinds of static slice are constructed.Then,a new method of slicing backward dynamic slice is proposed based on local reachability graph which can locally reflect the dynamic properties of Petri nets.At last,forward dynamic slice can be obtained through the reachability marking graph under a special marking.The algorithms can be used to reduce the size of Petri net,which can provide the basic technical support for simplifying the complexity of formal verification and analysis.展开更多
It is increasingly common to find graphs in which edges are of different types, indicating a variety of relation- ships. For such graphs we propose a class of reachability queries and a class of graph patterns, in whi...It is increasingly common to find graphs in which edges are of different types, indicating a variety of relation- ships. For such graphs we propose a class of reachability queries and a class of graph patterns, in which an edge is specified with a regular expression of a certain form, ex- pressing the connectivity of a data graph via edges of var- ious types. In addition, we define graph pattern matching based on a revised notion of graph simulation. On graphs in emerging applications such as social networks, we show that these queries are capable of finding more sensible informa- tion than their traditional counterparts. Better still, their in- creased expressive power does not come with extra complex- ity. Indeed, （1） we investigate their containment and mini- mization problems, and show that these fundamental prob- lems are in quadratic time for reachability queries and are in cubic time for pattern queries. （2） We develop an algorithm for answering reachability queries, in quadratic time as for their traditional counterpart. （3） We provide two cubic-time algorithms for evaluating graph pattern queries, as opposed to the NP-completeness of graph pattern matching via subgraph isomorphism. （4） The effectiveness and efficiency of these al- gorithms are experimentally verified using real-life data and synthetic data.展开更多
Program synthesis is an exciting topic that desires to generate programs satisfying user intent automatically. But in most cases, only small programs for simple or domain-specific tasks can be synthesized. The major o...Program synthesis is an exciting topic that desires to generate programs satisfying user intent automatically. But in most cases, only small programs for simple or domain-specific tasks can be synthesized. The major obstacle of synthesis lies in the huge search space. A common practice in addressing this problem is using a domain-specific language, while many approaches still wish to synthesize programs in general programming languages. With the rapid growth of reusable libraries, component-based synthesis provides a promising way, such as synthesizing Java programs which are only composed of APIs (application programming interfaces). However, the efficiency of searching for proper solutions for complex tasks is still a challenge. Given an unfamiliar programming task, programmers would search for API usage knowledge from various coding resources to reduce the search space. Considering this, we propose a novel approach named ProSy to synthesize API-based programs in Java. The key novelty is to retrieve related knowledge from Javadoc and Stack Overflow and then construct a probabilistic reachability graph. It assigns higher probabilities to APIs that are more likely to be used in implementing the given task. In the synthesis process, the program sketch with a higher probability will be considered first;thus, the number of explored reachable paths would be decreased. Some extension and optimization strategies are further studied in the paper. We implement our approach and conduct several experiments on it. We compare ProSy with SyPet and other state-of-the-art API-based synthesis approaches. The experimental results show that ProSy reduces the synthesis time of SyPet by up to 80%.展开更多
文摘Reachability graph is a very important tool to analyze the dynamic properties of Petri nets, but the concurrent relation of transitions in Petri nets cannot be represented by reachability graph. Petri net is a concurrent system, while reachability graph is a serial one. However, concurrency is a kind of property which is not only very significant but also difficult to be analyzed and controlled. This paper presents the concepts of concurrent reachable marking and concurrent reachable graph in order to represent and analyze the concurrent system. The algorithm constructing concurrent reachable marking set and concurrent reachability graph is also shown so that we can study the response problems among services in a network computing environment and analyze the throughput of the system. The Dining Philosophers Problem, which is a classic problem of describing the management of concurrent resources, is given as an example to illustrate the significance of concurrent reachability graph.
基金This work is supported by the National Basic Research Program of China （2010CB328101） the National Natural Science Foundation of China （Grant Nos. 61170078 and 61173042）+2 种基金 the Doctoral Program of Higher Education of the Specialized Research Fund of China （20113718110004） Basic Research Program of Qingdao City of China （13- 1-4-116-jch） and the SDUST Research Fund of China （2011KYTD 102）.
文摘Logic Petri nets （LPNs） are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reach- able markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.
基金supported in part by the National Key R&D Program of China(2017YFB1001804)Shanghai Science and Technology Innovation Action Plan Project(16511100900)
文摘In order to guarantee the correctness of business processes, not only control-flow errors but also data-flow errors should be considered. The control-flow errors mainly focus on deadlock, livelock, soundness, and so on. However, there are not too many methods for detecting data-flow errors. This paper defines Petri nets with data operations(PN-DO) that can model the operations on data such as read, write and delete. Based on PN-DO, we define some data-flow errors in this paper. We construct a reachability graph with data operations for each PN-DO, and then propose a method to reduce the reachability graph. Based on the reduced reachability graph, data-flow errors can be detected rapidly. A case study is given to illustrate the effectiveness of our methods.
基金supported by the Deanship of Scientific Research(DSR)King Abdulaziz University,Jeddah(23-135-35-HiCi)
文摘Hybrid Petri nets(HPNs) are widely used to describe and analyze various industrial hybrid systems that have both discrete-event and continuous discrete-time behaviors. Recently,many researchers attempt to utilize them to characterize power and energy systems. This work proposes to adopt an HPN to model and analyze a microgrid that consists of green energy sources. A reachability graph for such a model is generated and used to analyze the system properties.
基金Supported by the National Natural Science Foundation of China(No.90818023)the National Basic Research Program of China(No.2010CB328101)+2 种基金Shanghai Science&Technology Research Plan(No.09JC1414200,09510701300)"Dawn"Program of Shanghai Education Commission,Program for Changjiang Scholars and Innovative Research Team in University(PCSIRT),National Major Projects of Scienceand Technology(No.2009ZX01036-001-002:part 5)Natural Science Foundation of Educational Government of Anhui Province(No.KJ2011A086)
文摘Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts with respect to a criterion for analyzing programs,and has been widely used in specification level for model reduction,but researches on slicing of Petri nets are still limited.According to the idea of program slicing,this paper extends slicing technologies of Petri nets to four kinds of slices,including backward static slice,backward dynamic slice,forward static slice and forward dynamic slice.Based on the structure properties,the algorithms of obtaining two kinds of static slice are constructed.Then,a new method of slicing backward dynamic slice is proposed based on local reachability graph which can locally reflect the dynamic properties of Petri nets.At last,forward dynamic slice can be obtained through the reachability marking graph under a special marking.The algorithms can be used to reduce the size of Petri net,which can provide the basic technical support for simplifying the complexity of formal verification and analysis.
文摘It is increasingly common to find graphs in which edges are of different types, indicating a variety of relation- ships. For such graphs we propose a class of reachability queries and a class of graph patterns, in which an edge is specified with a regular expression of a certain form, ex- pressing the connectivity of a data graph via edges of var- ious types. In addition, we define graph pattern matching based on a revised notion of graph simulation. On graphs in emerging applications such as social networks, we show that these queries are capable of finding more sensible informa- tion than their traditional counterparts. Better still, their in- creased expressive power does not come with extra complex- ity. Indeed, （1） we investigate their containment and mini- mization problems, and show that these fundamental prob- lems are in quadratic time for reachability queries and are in cubic time for pattern queries. （2） We develop an algorithm for answering reachability queries, in quadratic time as for their traditional counterpart. （3） We provide two cubic-time algorithms for evaluating graph pattern queries, as opposed to the NP-completeness of graph pattern matching via subgraph isomorphism. （4） The effectiveness and efficiency of these al- gorithms are experimentally verified using real-life data and synthetic data.
基金This paper was supported by the National Natural Science Foundation of China under Grant No.61690203the National Key Research and Development Program of China under Grant No.2018YFB0204301.
文摘Program synthesis is an exciting topic that desires to generate programs satisfying user intent automatically. But in most cases, only small programs for simple or domain-specific tasks can be synthesized. The major obstacle of synthesis lies in the huge search space. A common practice in addressing this problem is using a domain-specific language, while many approaches still wish to synthesize programs in general programming languages. With the rapid growth of reusable libraries, component-based synthesis provides a promising way, such as synthesizing Java programs which are only composed of APIs (application programming interfaces). However, the efficiency of searching for proper solutions for complex tasks is still a challenge. Given an unfamiliar programming task, programmers would search for API usage knowledge from various coding resources to reduce the search space. Considering this, we propose a novel approach named ProSy to synthesize API-based programs in Java. The key novelty is to retrieve related knowledge from Javadoc and Stack Overflow and then construct a probabilistic reachability graph. It assigns higher probabilities to APIs that are more likely to be used in implementing the given task. In the synthesis process, the program sketch with a higher probability will be considered first;thus, the number of explored reachable paths would be decreased. Some extension and optimization strategies are further studied in the paper. We implement our approach and conduct several experiments on it. We compare ProSy with SyPet and other state-of-the-art API-based synthesis approaches. The experimental results show that ProSy reduces the synthesis time of SyPet by up to 80%.
