The supervisory control problem for discrete event system(DES) under control involves identifying the supervisor, if one exists, which, when synchronously composed with the DES,results in a system that conforms to the...The supervisory control problem for discrete event system(DES) under control involves identifying the supervisor, if one exists, which, when synchronously composed with the DES,results in a system that conforms to the control specification. In this context, we consider a non-deterministic DES under complete observation and control specification expressed in action-based propositional μ-calculus. The key to our solution is the process of quotienting the control specification against the plan resulting in a new μ-calculus formula such that a model for the formula is the supervisor. Thus the task of control synthesis is reduced a problem of μ-calculus satisfiability. In contrast to the existing μ-calculus quotienting-based techniques that are developed in deterministic setting, our quotienting rules can handle nondeterminism in the plant models. Another distinguishing feature of our technique is that while existing techniques use a separate μ-calculus formula to describe the controllability constraint(that uncontrollable events of plants are never disabled by a supervisor), we absorb this constraint as part of quotienting which allows us to directly capture more general state-dependent controllability constraints. Finally, we develop a tableau-based technique for verifying satisfiability of quotiented formula and model generation. The runtime for the technique is exponential in terms of the size of the plan and the control specification. A better complexity result that is polynomial to plant size and exponential to specification size is obtained when the controllability property is state-independent. A prototype implementation in a tabled logic programming language as well as some experimental results are presented.展开更多
The spectrum allocation for cognitive radio networks(CRNs) has received considerable studies under the assumption that the bandwidth of spectrum holes is static. However, in practice, the bandwidth of spectrum holes i...The spectrum allocation for cognitive radio networks(CRNs) has received considerable studies under the assumption that the bandwidth of spectrum holes is static. However, in practice, the bandwidth of spectrum holes is time-varied due to primary user/secondary user(PU/SU) activity and mobility, which result in non-determinacy. This paper studies the spectrum allocation for CRNs with non-deterministic bandwidth of spectrum holes. We present a novel probability density function(PDF) through order statistics as well as its simplified form to describe the statistical properties of spectrum holes, with which a statistical spectrum allocation model based on stochastic multiple knapsack problem(MKP) is formulated for spectrum allocation with non-deterministic bandwidth of spectrum holes. To reduce the computational complexity, we transform this stochastic programming problem into a constant MKP through exploiting the properties of cumulative distribution function(CDF), which can be solved via MTHG algorithm by using auxiliary variables. Simulation results illustrate that the proposed statistical spectrum allocation algorithm can achieve better performance compared with the existing algorithms when the bandwidth of spectrum holes is time-varied.展开更多
Watson Crick automata are finite automata working on double strands. Extensive research work has already been done on non deterministic Watson Crick automata and on deterministic Watson Crick automata. Parallel Commun...Watson Crick automata are finite automata working on double strands. Extensive research work has already been done on non deterministic Watson Crick automata and on deterministic Watson Crick automata. Parallel Communicating Watson Crick automata systems have been introduced by E. Czeziler et al. In this paper we discuss about a variant of Watson Crick automata known as the two-way Watson Crick automata which are more powerful than non-deterministic Watson Crick automata. We also establish the equivalence of different subclasses of two-way Watson crick automata. We further show that recursively enumerable (RE) languages can be realized by an image of generalized sequential machine (gsm) mapping of two-way Watson-Crick automata.展开更多
Modeling and forecasting of the groundwater water table are a major component of effective planning and management of water resources. One way to predict the groundwater level is analysis using a non-deterministic mod...Modeling and forecasting of the groundwater water table are a major component of effective planning and management of water resources. One way to predict the groundwater level is analysis using a non-deterministic model. This study assessed the performance of such models in predicting the groundwater level at Kashan aquifer. Data from 36 piezometer wells in Kashan aquifer for 1999 to 2010 were used. The desired statistical interval was divided into two parts and statistics for 1990 to 2004 were used for modeling and statistics from 2005 to 2010 were used for valediction of the model. The Akaike criterion and correlation coefficients were used to determine the accuracy of the prediction models. The results indicated that the AR(2) model more accurately predicted ground water level in the plains;using this model, the groundwater water table was predicted for up to 60 mo.展开更多
In this paper, we study the supervisory control problem of discrete event systems assuming that cyber-attacks might occur. In particular, we focus on the problem of liveness enforcement and consider a sensor-reading m...In this paper, we study the supervisory control problem of discrete event systems assuming that cyber-attacks might occur. In particular, we focus on the problem of liveness enforcement and consider a sensor-reading modification attack(SM-attack) that may disguise the occurrence of an event as that of another event by intruding sensor communication channels. To solve the problem, we introduce non-deterministic supervisors in the paper, which associate to every observed sequence a set of possible control actions offline and choose a control action from the set randomly online to control the system. Specifically, given a bounded Petri net(PN) as the reference formalism and an SMattack, an algorithm that synthesizes a liveness-enforcing nondeterministic supervisor tolerant to the SM-attack is proposed for the first time.展开更多
基金supported in part by the National Sci-ence Foundation (NSF-ECCS-1509420, NSF-CSSI-2004766)。
文摘The supervisory control problem for discrete event system(DES) under control involves identifying the supervisor, if one exists, which, when synchronously composed with the DES,results in a system that conforms to the control specification. In this context, we consider a non-deterministic DES under complete observation and control specification expressed in action-based propositional μ-calculus. The key to our solution is the process of quotienting the control specification against the plan resulting in a new μ-calculus formula such that a model for the formula is the supervisor. Thus the task of control synthesis is reduced a problem of μ-calculus satisfiability. In contrast to the existing μ-calculus quotienting-based techniques that are developed in deterministic setting, our quotienting rules can handle nondeterminism in the plant models. Another distinguishing feature of our technique is that while existing techniques use a separate μ-calculus formula to describe the controllability constraint(that uncontrollable events of plants are never disabled by a supervisor), we absorb this constraint as part of quotienting which allows us to directly capture more general state-dependent controllability constraints. Finally, we develop a tableau-based technique for verifying satisfiability of quotiented formula and model generation. The runtime for the technique is exponential in terms of the size of the plan and the control specification. A better complexity result that is polynomial to plant size and exponential to specification size is obtained when the controllability property is state-independent. A prototype implementation in a tabled logic programming language as well as some experimental results are presented.
基金supported by the National Natural Science Foundation of China (No.61501065, 91438104,No.61571069 and No.61601067)the Fundamental Research Funds for the Central Universities (No.106112015CDJXY160002,No.106112016CDJXY160001)the Chongqing Research Program of Basic Research and Frontier Technology (No.CSTC2016JCYJA0021)
文摘The spectrum allocation for cognitive radio networks(CRNs) has received considerable studies under the assumption that the bandwidth of spectrum holes is static. However, in practice, the bandwidth of spectrum holes is time-varied due to primary user/secondary user(PU/SU) activity and mobility, which result in non-determinacy. This paper studies the spectrum allocation for CRNs with non-deterministic bandwidth of spectrum holes. We present a novel probability density function(PDF) through order statistics as well as its simplified form to describe the statistical properties of spectrum holes, with which a statistical spectrum allocation model based on stochastic multiple knapsack problem(MKP) is formulated for spectrum allocation with non-deterministic bandwidth of spectrum holes. To reduce the computational complexity, we transform this stochastic programming problem into a constant MKP through exploiting the properties of cumulative distribution function(CDF), which can be solved via MTHG algorithm by using auxiliary variables. Simulation results illustrate that the proposed statistical spectrum allocation algorithm can achieve better performance compared with the existing algorithms when the bandwidth of spectrum holes is time-varied.
文摘Watson Crick automata are finite automata working on double strands. Extensive research work has already been done on non deterministic Watson Crick automata and on deterministic Watson Crick automata. Parallel Communicating Watson Crick automata systems have been introduced by E. Czeziler et al. In this paper we discuss about a variant of Watson Crick automata known as the two-way Watson Crick automata which are more powerful than non-deterministic Watson Crick automata. We also establish the equivalence of different subclasses of two-way Watson crick automata. We further show that recursively enumerable (RE) languages can be realized by an image of generalized sequential machine (gsm) mapping of two-way Watson-Crick automata.
文摘Modeling and forecasting of the groundwater water table are a major component of effective planning and management of water resources. One way to predict the groundwater level is analysis using a non-deterministic model. This study assessed the performance of such models in predicting the groundwater level at Kashan aquifer. Data from 36 piezometer wells in Kashan aquifer for 1999 to 2010 were used. The desired statistical interval was divided into two parts and statistics for 1990 to 2004 were used for modeling and statistics from 2005 to 2010 were used for valediction of the model. The Akaike criterion and correlation coefficients were used to determine the accuracy of the prediction models. The results indicated that the AR(2) model more accurately predicted ground water level in the plains;using this model, the groundwater water table was predicted for up to 60 mo.
基金supported in part by the Public Technology Research Plan of Zhejiang Province (LGJ21F030001)the National Natural Science Foundation of China (62302448)the Zhejiang Provincial Key Laboratory of New Network Standards and Technologies (2013E10012)。
文摘In this paper, we study the supervisory control problem of discrete event systems assuming that cyber-attacks might occur. In particular, we focus on the problem of liveness enforcement and consider a sensor-reading modification attack(SM-attack) that may disguise the occurrence of an event as that of another event by intruding sensor communication channels. To solve the problem, we introduce non-deterministic supervisors in the paper, which associate to every observed sequence a set of possible control actions offline and choose a control action from the set randomly online to control the system. Specifically, given a bounded Petri net(PN) as the reference formalism and an SMattack, an algorithm that synthesizes a liveness-enforcing nondeterministic supervisor tolerant to the SM-attack is proposed for the first time.
