In this work, we address the codiagnosability analysis problem of a networked discrete event system under malicious attacks. The considered system is modeled by a labeled Petri net and is monitored by a series of site...In this work, we address the codiagnosability analysis problem of a networked discrete event system under malicious attacks. The considered system is modeled by a labeled Petri net and is monitored by a series of sites, in which each site possesses its own set of sensors, without requiring communication among sites or to any coordinators. A net is said to be codiagnosable with respect to a fault if at least one site could deduce the occurrence of this fault within finite steps. In this context, we focus on a type of malicious attack that is called stealthy intermittent replacement attack. The stealthiness demands that the corrupted observations should be consistent with the system's normal behavior, while the intermittent replacement setting entails that the replaced transition labels must be recovered within a bounded of consecutive corrupted observations(called as K-corruption intermittent attack). Particularly, there exists a coordination between attackers that are separately effected on different sites, which holds the same corrupted observation for each common transition under attacks. From an attacker viewpoint, this work aims to design Kcorruption intermittent attacks for violating the codiagnosability of systems. For this purpose, we propose an attack automaton to analyze K-corruption intermittent attack for each site, and build a new structure called complete attack graph that is used to analyze all the potential attacked paths. Finally, an algorithm is inferred to obtain the K-corruption intermittent attacks, and examples are given to show the proposed attack strategy.展开更多
This paper addresses the verification of strong currentstate opacity with respect to real-time observations generated from a discrete-event system that is modeled with time labeled Petri nets. The standard current-sta...This paper addresses the verification of strong currentstate opacity with respect to real-time observations generated from a discrete-event system that is modeled with time labeled Petri nets. The standard current-state opacity cannot completely characterize higher-level security. To ensure the higher-level security requirements of a time-dependent system, we propose a strong version of opacity known as strong current-state opacity. For any path(state-event sequence with time information)π derived from a real-time observation that ends at a secret state, the strong current-state opacity of the real-time observation signifies that there is a non-secret path with the same real-time observation as π. We propose general and non-secret state class graphs, which characterize the general and non-secret states of time-dependent systems, respectively. To capture the observable behavior of non-secret states, a non-secret observer is proposed.Finally, we develop a structure called a real-time concurrent verifier to verify the strong current-state opacity of time labeled Petri nets. This approach is efficient since the real-time concurrent verifier can be constructed by solving a certain number of linear programming problems.展开更多
Mobile robot local motion planning is responsible for the fast and smooth obstacle avoidance,which is one of the main indicators for evaluating mobile robots'navigation capabilities.Current methods formulate local...Mobile robot local motion planning is responsible for the fast and smooth obstacle avoidance,which is one of the main indicators for evaluating mobile robots'navigation capabilities.Current methods formulate local motion planning as a unified problem;therefore it cannot satisfy the real-time requirement on the platform with limited computing ability.In order to solve this problem,this paper proposes a fast local motion planning method that can reach a planning frequency of 500 Hz on a low-cost CPU.The proposed method decouples the local motion planning as the front-end path searching and the back-end optimization.The front-end is composed of the environment topology analysis and graph searching.The back-end includes dynamically feasible trajectory generation and optimal trajectory selection.Different from the popular methods,the proposed method decomposes the local motion planning into four sub-modules,each of which aims to solve one problem.Combining four sub-modules,the proposed method can obtain the complete local motion planning algorithm which can fast generate a smooth and collision-free trajectory.The experimental results demonstrate that the proposed method has the ability to obtain the smooth,dynamically feasible and collision-free trajectory and the speed of the planning is fast.展开更多
Kuala Lumpur of Malaysia,as a tropical city,has experienced a notable decline in its critical urban green infrastructure(UGI)due to rapid urbanization and haphazard development.The decrease of UGI,especially natural f...Kuala Lumpur of Malaysia,as a tropical city,has experienced a notable decline in its critical urban green infrastructure(UGI)due to rapid urbanization and haphazard development.The decrease of UGI,especially natural forest and artificial forest,may reduce the diversity of ecosystem services and the ability of Kuala Lumpur to build resilience in the future.This study analyzed land use and land cover(LULC)and UGI changes in Kuala Lumpur based on Landsat satellite images in 1990,2005,and 2021and employed the overall accuracy and Kappa coefficient to assess classification accuracy.LULC was categorized into six main types:natural forest,artificial forest,grassland,water body,bare ground,and built-up area.Satellite images in 1990,2005,and 2021 showed the remarkable overall accuracy values of 91.06%,96.67%,and 98.28%,respectively,along with the significant Kappa coefficient values of 0.8997,0.9626,and 0.9512,respectively.Then,this study utilized Cellular Automata and Markov Chain model to analyze the transition of different LULC types during 1990-2005 and 1990-2021 and predict LULC types in 2050.The results showed that natural forest decreased from 15.22%to 8.20%and artificial forest reduced from 18.51%to 15.16%during 1990-2021.Reductions in natural forest and artificial forest led to alterations in urban surface water dynamics,increasing the risk of urban floods.However,grassland showed a significant increase from 7.80%to 24.30%during 1990-2021.Meanwhile,bare ground increased from 27.16%to 31.56%and built-up area increased from 30.45%to 39.90%during 1990-2005.In 2021,built-up area decreased to 35.10%and bare ground decreased to 13.08%,indicating a consistent dominance of built-up area in the central parts of Kuala Lumpur.This study highlights the importance of integrating past,current,and future LULC changes to improve urban ecosystem services in the city.展开更多
基金supported in part by the IN2CCAM project that has received funding from the European Union's Horizon Europe research and innovation programme(101076791)the National Natural Science Foundation of China(62403378)the Natural Science Basic Research Program of Shaanxi Province(2024JC-YBQN-0669)
文摘In this work, we address the codiagnosability analysis problem of a networked discrete event system under malicious attacks. The considered system is modeled by a labeled Petri net and is monitored by a series of sites, in which each site possesses its own set of sensors, without requiring communication among sites or to any coordinators. A net is said to be codiagnosable with respect to a fault if at least one site could deduce the occurrence of this fault within finite steps. In this context, we focus on a type of malicious attack that is called stealthy intermittent replacement attack. The stealthiness demands that the corrupted observations should be consistent with the system's normal behavior, while the intermittent replacement setting entails that the replaced transition labels must be recovered within a bounded of consecutive corrupted observations(called as K-corruption intermittent attack). Particularly, there exists a coordination between attackers that are separately effected on different sites, which holds the same corrupted observation for each common transition under attacks. From an attacker viewpoint, this work aims to design Kcorruption intermittent attacks for violating the codiagnosability of systems. For this purpose, we propose an attack automaton to analyze K-corruption intermittent attack for each site, and build a new structure called complete attack graph that is used to analyze all the potential attacked paths. Finally, an algorithm is inferred to obtain the K-corruption intermittent attacks, and examples are given to show the proposed attack strategy.
基金supported by the Special Fund for Scientific and Technological Innovation Strategy of Guangdong Province(2022A0505030025)the Science and Technology Fund,FDCT,Macao SAR(0064/2021/A2)
文摘This paper addresses the verification of strong currentstate opacity with respect to real-time observations generated from a discrete-event system that is modeled with time labeled Petri nets. The standard current-state opacity cannot completely characterize higher-level security. To ensure the higher-level security requirements of a time-dependent system, we propose a strong version of opacity known as strong current-state opacity. For any path(state-event sequence with time information)π derived from a real-time observation that ends at a secret state, the strong current-state opacity of the real-time observation signifies that there is a non-secret path with the same real-time observation as π. We propose general and non-secret state class graphs, which characterize the general and non-secret states of time-dependent systems, respectively. To capture the observable behavior of non-secret states, a non-secret observer is proposed.Finally, we develop a structure called a real-time concurrent verifier to verify the strong current-state opacity of time labeled Petri nets. This approach is efficient since the real-time concurrent verifier can be constructed by solving a certain number of linear programming problems.
基金the National Key R&D Program of China (No.2017YFB1301300)。
文摘Mobile robot local motion planning is responsible for the fast and smooth obstacle avoidance,which is one of the main indicators for evaluating mobile robots'navigation capabilities.Current methods formulate local motion planning as a unified problem;therefore it cannot satisfy the real-time requirement on the platform with limited computing ability.In order to solve this problem,this paper proposes a fast local motion planning method that can reach a planning frequency of 500 Hz on a low-cost CPU.The proposed method decouples the local motion planning as the front-end path searching and the back-end optimization.The front-end is composed of the environment topology analysis and graph searching.The back-end includes dynamically feasible trajectory generation and optimal trajectory selection.Different from the popular methods,the proposed method decomposes the local motion planning into four sub-modules,each of which aims to solve one problem.Combining four sub-modules,the proposed method can obtain the complete local motion planning algorithm which can fast generate a smooth and collision-free trajectory.The experimental results demonstrate that the proposed method has the ability to obtain the smooth,dynamically feasible and collision-free trajectory and the speed of the planning is fast.
基金supported by the Malaysia-Japan International Institute of Technology(MJIIT),Universiti Teknologi Malaysia.
文摘Kuala Lumpur of Malaysia,as a tropical city,has experienced a notable decline in its critical urban green infrastructure(UGI)due to rapid urbanization and haphazard development.The decrease of UGI,especially natural forest and artificial forest,may reduce the diversity of ecosystem services and the ability of Kuala Lumpur to build resilience in the future.This study analyzed land use and land cover(LULC)and UGI changes in Kuala Lumpur based on Landsat satellite images in 1990,2005,and 2021and employed the overall accuracy and Kappa coefficient to assess classification accuracy.LULC was categorized into six main types:natural forest,artificial forest,grassland,water body,bare ground,and built-up area.Satellite images in 1990,2005,and 2021 showed the remarkable overall accuracy values of 91.06%,96.67%,and 98.28%,respectively,along with the significant Kappa coefficient values of 0.8997,0.9626,and 0.9512,respectively.Then,this study utilized Cellular Automata and Markov Chain model to analyze the transition of different LULC types during 1990-2005 and 1990-2021 and predict LULC types in 2050.The results showed that natural forest decreased from 15.22%to 8.20%and artificial forest reduced from 18.51%to 15.16%during 1990-2021.Reductions in natural forest and artificial forest led to alterations in urban surface water dynamics,increasing the risk of urban floods.However,grassland showed a significant increase from 7.80%to 24.30%during 1990-2021.Meanwhile,bare ground increased from 27.16%to 31.56%and built-up area increased from 30.45%to 39.90%during 1990-2005.In 2021,built-up area decreased to 35.10%and bare ground decreased to 13.08%,indicating a consistent dominance of built-up area in the central parts of Kuala Lumpur.This study highlights the importance of integrating past,current,and future LULC changes to improve urban ecosystem services in the city.
