Search

This paper deals with a "digital twin" (DT) approach for processing, reprocessing, and scrapping (P/R/S) technology running on a modular production system (MPS) assisted by a mobile cyber–physical robotic system (MCPRS). The main hardware architecture consists of four line-shaped workstations (WSs), a wheeled mobile robot (WMR) equipped with a robotic manipulator (RM) and a mobile visual servoing system (MVSS) mounted on the end effector. The system architecture integrates a hierarchical control system where each of the four WSs, in the MPS, is controlled by a Programable Logic Controller (PLC), all connected via Profibus DP to a central PLC. In addition to the connection via Profibus of the four PLCs, related to the WSs, to the main PLC, there are also the connections of other devices to the local networks, LAN Profinet and LAN Ethernet. There are the connections to the Internet, Cloud and Virtual Private Network (VPN) via WAN Ethernet by open platform communication unified architecture (OPC-UA). The overall system follows a DT approach that enables task planning through augmented reality (AR) and uses virtual reality (VR) for visualization through Synchronized Hybrid Petri Net (SHPN) simulation. Timed Petri Nets (TPNs) are used to control the processes within the MPS's workstations. Continuous Petri Nets (CPNs) handle the movement of the MCPRS. Task planning in AR enables users to interact with the system in real time using AR technology to visualize and plan tasks. SHPN in VR is a combination of TPNs and CPNs used in the virtual representation of the system to synchronize tasks between the MPS and MCPRS. The workpiece (WP) visits stations successively as it is moved along the line for processing. If the processed WP does not pass the quality test, it is taken from the last WS and is transported, by MCPRS, to the first WS where it will be considered for reprocessing or scrapping. [ABSTRACT FROM AUTHOR]

This paper introduces a novel algorithm for the efficient verification of a Petri net-based concurrent control system. The proposed method is based on the computation of transition invariant coverage to detect possible errors in the modelled system. Transition invariants play a crucial role in ensuring the correctness and reliability of such systems; however, existing methods often struggle with high computational demand, especially in the case of large and complex systems. The proposed approach addresses this challenge by performing a fast polynomial-time analysis to identify uncovered transitions, thereby streamlining the verification process. The effectiveness and efficiency of the proposed technique is verified experimentally with a set of 386 test modules (benchmarks) and compared against two well-known established methods: the classical method proposed by Martínez–Silva (as a reference algorithm) and PIPE (Platform Independent Petri Net Editor) tool. The results of the experiments confirm high performance of the presented algorithm, which was able to compute results for all the tested cases. In contrast, both the reference algorithm as well as the PIPE tool failed to deliver results for all examined models within one hour. The proposed algorithm is especially useful in early design stages, offering system designers timely insights into potential issues. [ABSTRACT FROM AUTHOR]

Intrusion Detection Systems (IDSs) are a crucial component of modern corporate firewalls. The ability of IDS to identify malicious traffic is a powerful tool to prevent potential attacks and keep a corporate network secure. In this context, Machine Learning (ML)-based methods have proven to be very effective for attack identification. However, traditional approaches are not always applicable in a real-time environment as they do not integrate concrete traffic management after a malicious packet pattern has been identified. In this paper, a novel combined approach to both identify and discard potential malicious traffic in a real-time fashion is proposed. In detail, a Long Short-Term Memory (LSTM) supervised artificial neural network model is provided in which consecutive packet groups are considered as they flow through the corporate network. Moreover, the whole IDS architecture is modeled by a Petri Net (PN) that either blocks or allows packet flow throughout the network based on the LSTM model output. The novel hybrid approach combining LSTM with Petri Nets achieves a 99.71% detection accuracy—a notable improvement over traditional LSTM-only methods, which averaged around 97%. The LSTM–Petri Net approach is an innovative solution combining machine learning with formal network modeling for enhanced threat detection, offering improved accuracy and real-time adaptability to meet the rapid security needs of virtual environments and CPS. Moreover, the approach emphasizes the innovative role of the Intrusion Detection System (IDS) and Intrusion Prevention System (IPS) as a form of "virtual sensing technology" applied to advanced network security. An extensive case study with promising results is provided by training the model with the popular IDS 2018 dataset. [ABSTRACT FROM AUTHOR]

Ventricular assist devices (VADs) are designed to provide sufficient blood flow to patients with severe heart failure. Once implanted, the patient becomes dependent on the VAD, making it essential to prevent situations that could harm the patient while receiving circulatory support. VADs are classified as critical systems (CS), and adverse events (AEs) can lead to serious consequences, including hospitalization or even death. At present, patient care is provided through in-person consultations, with incidents reported via medical device reports (MDRs) to the Food and Drug Administration (FDA). However, there is no real-time monitoring of AEs or oversight of these events. In response to this gap, a system for supervising critical adverse processes in patients with implanted VADs (SCVAD) is proposed, based on horizontally and vertically integrated architecture. This system aims to address the complexity of AEs by considering multiple domains of operation: the device, the patient, and the medical team, as well as the interactions between these entities. In this context, the formalism of Petri nets (PN) is used to develop models that represent adverse processes based on the actions recommended by the medical team. These models allow for the mapping of events with the potential to cause harm to the patient. Therefore, the medical team will be able to monitor adverse processes, as the models in interpreted PN can be isomorphically transcribed into computable algorithms that can be processed on compatible devices, enabling the tracking of complications caused by adverse processes. [ABSTRACT FROM AUTHOR]

The NC-Link protocol, as an integrated communication protocol in the Computerized Numerical Control (CNC) machine tool industry, has drawn significant attention regarding its security since its inception. Although there have been studies proposing improvements to address security issues related to key management and message transmission, systematic security analysis of the protocol remains relatively weak. To better investigate and enhance the security of the NC-Link protocol, our research introduces a formal modeling and analysis method based on Colored Petri Nets (CPN). By establishing a CPN model of the protocol, we analyze the security issues present during communication and propose improvement measures for verification and analysis. First, we developed a CPN model for the NC-Link protocol and verified the model's feasibility through simulation analysis. Subsequently, we introduced an attacker model to analyze the protocol's authentication interaction process, revealing security issues, such as authentication vulnerabilities and key management flaws. Finally, we proposed an improved scheme addressing these issues and conducted a security validation and cost analysis of this scheme. The results show that the improved protocol reduces the computational overhead by 75% during the connection and interaction phases. This indicates that the improved protocol can achieve interactions at a faster speed while maintaining higher security and reliability. The implementation of this scheme provides new reference ideas for related research. [ABSTRACT FROM AUTHOR]

Monitoring natural phenomena using a variety of methods to predict disasters is a trend that is growing over time. However, there is a great disunity among methods and means of data analysis, formats and interfaces of storing and providing data, and software and information systems for data processing. As part of a large project to create a planetary observatory that combines data from spatially distributed geosphere monitoring systems, the efforts of leading institutes of the Russian Academy of Sciences are also aimed at creating an information and computing ecosystem to unite researchers processing and analyzing the data obtained. This article provides a brief overview of the current state of publications on information ecosystems in various applied fields, and it also proposes a concept for an ecosystem on a multiagent basis with unique technical features. The concept of the ecosystem includes the following: the ability to function in a heterogeneous environment on federal principles, the parallelization of data processing between agents using Petri nets as a mechanism ensuring the correct execution of data processing scenarios, the concept of georeferenced alarm events requiring ecosystem reactions and possible notification of responsible persons, and multilevel information protection allowing data owners to control access at each stage of information processing. [ABSTRACT FROM AUTHOR]

This paper presents a simulation model to study the effect of the battery charging rate of Automated Guided Vehicles (AGVs) on the overall output of a toy car production environment. This paper uses Modular Petri Nets for modeling and the General Petri Net Simulator (GPenSIM) for model implementation on MATLAB and simulation. The main focus of this paper is to analyze the operational efficiency of AGVs under varying conditions, such as the impact of battery charge reduction rates and the strategic placement of Charging Stations within the production line. By employing Modular Petri Nets implemented with GPenSIM, this paper presents a detailed model that captures the dynamics (movements and interactions) of AGVs in a simulated manufacturing environment. The model is also extensible, as newer functionalities can be added to it as Petri Modules. This paper specifically focuses on two critical operational parameters: (a) the number of AGVs and their battery charge reduction rate; (b) the number of Charging Stations. In summary, the goal, aim, and novelty of this paper is to provide a simpler yet effective model to practitioners so that they can study and experiment without needing advanced mathematical skills. [ABSTRACT FROM AUTHOR]

This study develops a timed Petri net (TPN)-based controller to mitigate traffic congestion resulting from sudden accidents by adapting traffic light sequences in real-time. The traditional traffic light signal (TLS) sequences are ineffective in resolving congestion from such accidents. To mitigate congestion, we propose immediately changing the sequence of TLSs at the traffic accident scene. Traffic accidents are categorized into three types (A-type, B-type and C-type) based on the direction in which they occur, and their traffic light sequences are designed according to their specific characteristics. By analyzing the timing of signal changes, ours proves to be more effective than traditional sequences in relieving traffic congestion. [ABSTRACT FROM AUTHOR]

This work addresses the analysis and characterization of deadlocks in discrete-event systems modeled by labeled Petri nets (LPNs) with undistinguishable and unobservable transitions. To provide a solution for the notorious problem, it is essential to present an effective characterization in such a way that deadlock control and synthesis are technically and methodologically possible. To this end, we introduce the notion of dangerous implicit vectors (DIVs), which implicitly threaten the system deadlock-freedom. The set of dead markings is divided into two subsets: dead basis markings (DBMs) and dangerous implicit markings (DIMs). An algorithm is designed to compute the sets of DIVs and DIMs at a given basis state of a system. Moreover, by virtue of linear algebraic equations, we formulate sufficient conditions for identifying the existence of blocking markings in an LPN. Finally, an algorithm is developed to construct an observed graph that is a compendious presentation of the reachability graph of a net system, with respect to the existence of dead reaches. At the end of this paper, experiment results that illustrate the correctness and effectiveness of the reported solution are presented. [ABSTRACT FROM AUTHOR]

DC converter stations have a high voltage level, a long transmission distance, and complex internal equipment, and contain power electronic devices, which seriously endanger the stable operation of the system itself and the active distribution network at the receiving end when faults occur. Accurate fault analysis and diagnosis are critical to the safe and stable operation of power systems. Traditional fault diagnosis methods often rely on a single source of information, leading to issues such as insufficient information utilization and incomplete diagnostic scope when applied to DC transmission systems. To address these problems, a fault diagnosis method for converter stations based on preliminary identification of the fault range and the fusion of evidence information of the switch signal and electrical quantity is proposed. First, the preprocessing of converter station sequential event recording (SER) events and a statistical analysis of event characteristics are completed to initially determine the range of the fault.Then, a fuzzy Petri net model and a BP neural network model are constructed on the basis of the fault data from a real-time digital simulation system (RTDS), and the corresponding evidence information of the switch signal and electrical quantity are obtained via iterative inference and deep learning methods. Finally, on the basis of D-S evidence theory, a comprehensive diagnosis result is obtained by fusing the switch and electric evidence information. Taking the fault data of a DC converter station as an example, the proposed method is analyzed and compared with the traditional method, which is based on single information. The results show that the proposed method can reliably and accurately identify fault points in the protected area of the converter station. [ABSTRACT FROM AUTHOR]

Since the 1990s, Petri nets have been used in systems biology for quantitative modeling. Despite the increasing number of models developed during this period, doubts remain about their biological relevance. Although biological systems predominantly exhibit intracellular or cellular structures, the models rely largely on deterministic predictions, failing to capture the inherent randomness and uncertainties of such systems. The question arises whether these models accurately describe the dynamic behavior of biological systems. This paper introduces a methodology for selecting the appropriate modeling paradigms in systems biology. Initially, we construct a Petri net model and perform deterministic, stochastic, and fuzzy stochastic simulations. Then we perform various statistical tests to measure the discrepancies between the simulation results. Based on scale-density analysis, we determine the modeling approach that best approximates the biological system. Finally, we compare the results of the statistical tests and the scale-density analysis to identify the optimal modeling approach. We applied the proposed methodology to the synthesis of spinal motor neuron protein from the spinal motor neuron-2 gene. Analysis revealed significant discrepancies between the simulation results of different modeling paradigms. Due to the sparse nature of the underlying drug-disease network, we conclude that the fuzzy stochastic paradigm provides the most biologically relevant results. We predict drug combinations that could lead to an up to 149-fold increase in spinal motor neuron protein levels, indicating a promising treatment for the disease. This methodology has the potential for application to other gene-drug-disease networks and broader biological systems. [ABSTRACT FROM AUTHOR]

This paper presents an approach for the verification of access control in smart contracts written in the Digital Asset Modeling Language (DAML). The approach utilizes Colored Petri Nets (CPNs) and their analysis tool CPN Tools. It is a model-driven-based approach that employs a new meta-model for capturing access control requirements in DAML contracts. The approach is supported by a suite of tools that fully automates all of the steps: parsing DAML code, generating DAML model instances, transforming the DAML models into CPN models, and model checking the generated CPN models. The approach is tested using several DAML scripts involving access control extracted from different domains of blockchain applications. [ABSTRACT FROM AUTHOR]

To solve the problems of chaotic information management and difficult traceability in the manufacturing process of transformer coils, a traceability and management method oriented towards the manufacturing process of transformer coils has been proposed. This method integrates industrial internet identification resolution and extension of Petri net modeling theory. A comprehensive identification and resolution framework for coil manufacturing processes has been constructed. In this manuscript, the authors proposed an industrial data-sharing space based on the producer-consumer model with unified coding identification. This enables information sharing for all resources, including personnel, machinery, materials, methods, environment, and measurements. A method for modeling extensible identification primitives of coil manufacturing process information was proposed, which formalizes the correlation and data structure of process information. A Petri net model for the comprehensive acquisition and integration of elemental information in coil manufacturing processes, as well as a mathematical model for quality traceability, were constructed, thereby forming a complete path for quality traceability information. Finally, based on the method proposed above, a software and hardware environment for identification and traceability for coil manufacturing was established. Taking a certain type of coil as an example, validation was carried out; the results indicate a significant enhancement in the production management and information traceability capabilities of the coil production workshop. This study provides reference and guidance for the process traceability management of power equipment manufacturing. [ABSTRACT FROM AUTHOR]

Oil refining is a branch of industry that delivers energy to move our vehicles. The transportation of people and goods by airplanes, ships, trains, trucks, buses, and cars is unthinkable for modern mankind without the use of refined petroleum automotive fuels. Thus, the optimal functioning of this industrial branch is vital to contemporary human society. The modeling of processes that take place during refined oil products' manufacturing, which are parallel in their essence, by generalized nets enables their activity optimization and better management. The generalized nets, which are in principle extensions of Petri nets, are applied in this research as a toolkit to model all processes from crude oil selection and delivery to a high complex refinery (Nelson index of 10.6) to the production of a great diversity of fuels, propylene, and polypropylene. The proposed article is a continuation and extension of the articles, published in Mathematics Journal in 2021 and 2023. It is the first (theoretical part) of our comprehensive study of modeling petroleum products' production processes in a refinery, and the second part will discuss the results of the software implementation of the model. [ABSTRACT FROM AUTHOR]

Self-driving cars are one of the main areas of research today, but it has to be acknowledged that the information from the sensors (the perceptron) is a huge amount of data, which is now unmanageable even when projected onto a single traffic junction. In the case of self-driving, the nodes have to be sequenced and organized according to the planned route. A self-driving car in Hungary would have to be able to interpret more than 70,000 traffic junctions to be able to drive all over the country. Besides the huge amount of data, another problem is the issue of validation and verification. For self-driving cars, this implies a level of complexity using traditional methods that calls into question the economics of the already existing system. Fuzzy Petri nets provide an alternative solution to both problems. They allow us to obtain a model that accurately describes the reliability of a node through its dynamics, which is essential in perception since the more reliable a node is, the smaller the deep learning mesh required. In this paper, we outline the analysis of a traffic node's safety using Petri nets and fuzzy analysis to gain information on the reliability of the node, which is essential for the modeling of self-driving cars, due to the deep learning model of perception. The reliability of the dynamics of the node is determined by using the modified fuzzy Petri net procedure. The need for a fuzzy extension of the Petri net was developed by knowledge of real traffic databases. [ABSTRACT FROM AUTHOR]

In order to express the energy flow, motion flow, and control flow in wireless rechargeable sensor networks accurately and intuitively, and to maximize the charging benefit of MVs (mobile vehicles), a type of MTS-HACO (Mobile Transition Sequence Hybrid Ant Colony Optimization) is proposed. Firstly, node places are grouped according to the firing time of node's energy consumption transition to ensure that in each time slot, MV places only enable charging transitions for the node places with lower remaining lifetimes. Then, the FSOMCT (Firing Sequence Optimization of Mobile Charging Transition) problem is formulated under the constraints of MV places capacity, travelling arc weight, charging arc weight, and so on. The elite strategy and the Max–Min Ant Colony system are further introduced to improve the ant colony algorithm, while the improved FWA (fireworks algorithm) optimizes the path constructed by each ant. Finally, the optimal mobile charging transition firing sequence and charging times are obtained, ensuring that MVs have sufficient energy to return to the base station. Simulation results indicate that, compared with the periodic algorithm and the PE-FWA algorithm, the proposed method can improve charging benefit by approximately 48.7% and 26.3%, respectively. [ABSTRACT FROM AUTHOR]

The airport apron is a high-risk area for aircraft collisions due to its heavy operational load and high aircraft density. Currently, existing quantitative models for apron collision risk provide limited consideration and classification of risk areas. In response, this paper proposes a Petri net-based method for assessing aircraft collision risk. The method predicts the probability of aircraft reaching different areas at different times based on operational data, enabling the calculation of collision risks within the Petri net framework. This approach highlights areas with potential collision risks and provides a classification evaluation. Subsequently, aircraft path re-planning is carried out to reduce collision risks. The model simplifies the complex operations of the apron system, making the calculation process clearer. The results show that, during the mid-phase of aircraft taxiing, there is a significant deviation between the actual and ideal positions of aircraft. Areas with high taxiway occupancy are more prone to collision risks. On peak days, due to relatively high flight volumes, the frequency of collision risks is 14% higher than on regular days, with an average risk increase of 23.3%, and the risks are more concentrated. Therefore, reducing collision risks through path planning becomes more challenging. It is recommended to focus attention on areas with high taxiway occupancy during peak periods and carefully plan routes to ensure apron safety. [ABSTRACT FROM AUTHOR]

In order to improve quality assurance in wafer manufacturing, there are strict process requirements. Besides the well-known residency time constraints (RTCs), a dual-arm cluster tool also requires each robot arm to execute a specific set of tasks. We call such a tool an arm task-constrained dual-arm cluster tool (ATC-DACT). To do this, one of the arms is identified as the dirty one and the other as the clean one. The dirty one can deal with raw wafers, while the clean one can deal with processed wafers. This requirement raises a new problem for scheduling a cluster tool. This paper discusses the scheduling problem of ATC-DACTs with RTCs. Due to the arm task constraints, the proven, effective swap strategy is no longer applicable to ATC-DACTs, making the scheduling problem difficult. To address this problem, we explicitly describe the robot waiting as an event and build a Petri net (PN) model. Then, we propose a hybrid task sequence (HTS) as an operation strategy by combining the swap and backward strategies. Based on the HTS, the necessary and sufficient conditions for schedulability are established; also, a linear programming model is developed. We then develop an algorithm using these results to optimally schedule the system. Industrial case studies demonstrate the application of this method. [ABSTRACT FROM AUTHOR]

This paper addresses the one-dimensional cutting stock problem, focusing on minimizing total stock usage. Most procedures that deal with this problem reside on linear programming methods, heuristics, metaheuristics, and hybridizations. These methods face drawbacks like handling only low-complexity instances or requiring extensive parameter tuning. To address these limitations we develop a Petri-net model to construct cutting patterns. Using the filtered beam search algorithm, the reachability tree of the Petri net is constructed level by level from its root node to find the best solution, pruning the nodes that worsen the solution as the search progresses through the tree. Our algorithm is compared with the Least Lost Algorithm and the Generate and Solve algorithm over five datasets of instances. These algorithms share some characteristics with ours and have proven to be effective and efficient. Experimental results demonstrate that our algorithm effectively finds optimal and near-optimalsolutions for both low and high-complexity instances. These findings confirm that Petri nets are suitable for modeling and solving the one-dimensional cutting stock problem. [ABSTRACT FROM AUTHOR]

In business process management, business process change analysis is the key link to ensure the flexibility and adaptability of the system. The existing methods mostly focus on the change analysis of a single business process from the perspective of control flow, ignoring the influence of data changes on collaborative processes with information interaction. In order to compensate for this deficiency, this paper proposes a rule-driven consistency analysis method for data changes in collaborative processes. Firstly, it analyzes the influence of data changes on other elements (such as activities, data, roles, and guards) in collaborative processes, and gives the definition of data influence. Secondly, the optimal alignment technology is used to explore how data changes interfere with the expected behavior of deviation activities, and decision rules are integrated into the Petri net model to accurately evaluate and screen out the effective expected behavior that conforms to business logic and established rules. Finally, the initial optimal alignment is repaired according to the screened effective expected behavior, and the consistency of business processes is recalculated. The experimental results show that the introduced rule constraint mechanism can effectively avoid the misjudgment of abnormal behavior. Compared with the traditional method, the average accuracy, recall rate, and F1-score of effective expected behavior are improved by 4%, 4.7%, and 4.3%, respectively. In addition, the repaired optimal alignment significantly enhances the system's ability to respond quickly and self-adjust to data changes, providing a strong support for the intelligent and automated transformation of business process management. [ABSTRACT FROM AUTHOR]

This paper presents an analysis of NO2 emissions in Mashhad City utilizing statistical evaluations and the Cisco Network Model. The present study begins by evaluating NO2 emissions through statistical analysis, followed by the application of histograms and radar statistical appraisals. Subsequently, a model execution logic is developed using the Cisco Network Model to further understand the distribution and sources of NO2 emissions in the city. Additionally, the research incorporates managerial insights by employing Petri Net modeling, which enables a deeper understanding of the dynamic interactions within the air quality management system. This approach aids in identifying critical control points and optimizing response strategies, thus enhancing the overall effectiveness of urban air pollution mitigation efforts. The findings of this study provide valuable insights into the levels of NO2 pollution in Mashhad City and offer a structured approach to modeling NO2 emissions for effective air quality management strategies which can be extended to the other megacities as well. [ABSTRACT FROM AUTHOR]

In this study, we analyzed the evolution of online public opinion on emergencies using a new Stochastic Petri Net modeling approach. First, an intuitive description of the emergency online public opinion development process was conceptualized from the life cycle evolution law perspective. Then, based on Petri net theory, a Stochastic Petri Net isomorphic Markov chain model was constructed to simulate the evolution of online public opinion on emergencies. Finally, four real-life cases were selected to validate and analyze the model, demonstrating that the evolutionary leaps, complexity, critical nodes, evolutionary rate, and execution time differ across different online public opinions on emergencies. The study results indicate that this modeling approach has certain advantages in examining the evolution based on multi-factor coupling and quantifying the evolution law in online public opinion on emergencies. [ABSTRACT FROM AUTHOR]

This paper is devoted to Petri net (PN)-based models of automated manufacturing systems (AMSs) with resources in order to prevent deadlocks in them. Their sustainability can be seen as the result of their deadlock freeness, leading to correct and fluent production, because AMSs with deadlocks work neither correctly nor fluently, need reconstruction and cause downtime in production. The paradigm of such PN models, S3PRs (systems of simple sequential processes with resources), is well known from the deadlock prevention point of view. Here, an extended S3PR (ES3PR) will be explored, with respect to its modelling and deadlock prevention. While in the case of S3PRs, ordinary Petri nets (OPNs) are used for these aims, here, for ES3PRs, generalized Petri nets (GPNs) are used. The reason for such a procedure is the possible presence of multiplex-directed arcs in the structure of PN models of AMSs. The significant alternation is that while, in the former case, the elementary siphons and dependent ones are sufficient for supervisor synthesis, here, in the later case, the GPNs and their siphons have to satisfy the max cs property. [ABSTRACT FROM AUTHOR]

Petri nets are a graphical notation for describing a class of discrete event dynamic systems whose behaviours are characterised by concurrency, synchronisation, mutual exclusion and conflict. They have been used over the years for the modelling of various distributed systems applications. With the advent of pervasive systems and the Internet of Things, the Calculus of Context-aware Ambients (CCA) has emerged as a suitable formal notation for analysing the behaviours of these systems. In this paper, we are interested in comparing the expressive power of Petri nets to that of CCA. That is, can the class of systems represented by Petri nets be modelled in CCA? To answer this question, an algorithm is proposed that maps any Petri net onto a CCA process. We prove that a Petri net and its corresponding CCA process are behavioural equivalent. It follows that CCA is at least as expressive as Petri nets, i.e., any system that can be specified in Petri nets can also be specified in CCA. Moreover, tools developed for CCA can also be used to analyse the behaviours of Petri nets. [ABSTRACT FROM AUTHOR]

Critical systems, in which failure and malfunction may result in severe human, environmental, and financial damages, are essential components in various sectors and particularly in energy domains. Although undesirable, integration error problems in the supervision of critical systems do occur, incurring significant expenses due to an operator's subjective analysis and hardware topology failures. In this work, a malleable model design approach is proposed to formulate and solve the integration error problem in critical systems' supervision in terms of reliability. A real hybrid power plant (HPP) case is considered for a case study with simulated data. A method framework with an informal approach (C4 diagram) and formal approach (hierarchical colored Petri nets) in a radial spectrum is applied to the HPP supervision design. In using formal methods, a formulation and solution to this problem through structured, scalable, and compact mathematical representations are possible. This malleable model is intended to guarantee the functional correctness and also reliability of the plant supervision system based on system software architecture. The outcomes suggest that the malleable model is appropriate for the energy domain and can be used for other types of critical systems, bringing all the benefits of this methodology to the context in which it will be applied. [ABSTRACT FROM AUTHOR]

As a typical information system, a cloud file system enables the storage, retrieval, and management of data on remote servers or server clusters. The reliable design of such systems is critical to ensure the security of data and availability of services. However, designing correct-by-construction systems is challenging due to the complexity of and concurrency inherent in cloud file systems. Further, existing works on cloud file system analysis often focus on specific systems or lack formal modeling and verification, leading to potential design flaws and security vulnerabilities. To address these issues, we propose MSCFS-RP, which is a formal analysis model based on colored Petri nets. Leveraging the strengths of colored Petri nets in representing diverse information types with colored tokens and defining explicit rules for concurrent interactions, our model captures the writing and reading processes of clients, meta servers, and clusters. With strong formalism and support for verification using CPN Tools, we rigorously evaluate key properties such as replication consistency under various scenarios. The results demonstrate that MSCFS-RP satisfies these properties, validating its effectiveness and trustworthiness in managing information within cloud storage systems. [ABSTRACT FROM AUTHOR]

With the rapid development of new-generation cyber–physical system (CPS) technologies, the smart operation and management of the broad bean harvesting system are enabled. This paper proposed a smart broad bean harvesting system (SBHS) and a self-adaptive control method based on CPS technologies. Firstly, the overall architecture of the SBHS is designed, which consists of four main components, namely optimal intelligent perception environment configuration, digital twin model construction, virtual simulation and real-time optimization, self-adaptive adjustment and control. Then, three key enabling technologies are discussed in detail, namely, intelligent perception environment configuration for the SBHS, digital twin model construction for the SBHS, colored Petri net (CPN)-based self-adaptive analysis and control of the harvesting system. Lastly, a proof-of-concept experiment based on a cooperative company is presented to illustrate the main work logic and advantage of the proposed SBHS. After the edge–cloud cooperative intelligent harvesting environment is configured, the CPN model for the workflow of the SBHS is created to analyze and optimize the harvesting processes. In addition, a management and control platform are developed to further illustrate the implementation of the proposed SBHS and the self-adaptive control method. [ABSTRACT FROM AUTHOR]

This research introduces the NeuRaiSya (Neural Railway System Application), an innovative railway signaling system integrating deep learning for passenger analysis. The objectives of this research are to simulate the NeuRaiSya and evaluate its effectiveness using the GreatSPN tool (graphical editor for Petri nets). GreatSPN facilitates evaluations of system behavior, ensuring safety and efficiency. Five models were designed and simulated using the Petri nets model, including the Dynamics of Train Departure model, Train Operations with Passenger Counting model, Timestamp Data Collection model, Train Speed and Location model, and Train Related-Issues model. Through simulations and modeling using Petri nets, the study demonstrates the feasibility of the proposed NeuRaiSya system. The results highlight its potential in enhancing railway operations, ensuring passenger safety, and maintaining service quality amidst the evolving railway landscape in the Philippines. [ABSTRACT FROM AUTHOR]

Efficient multiprocessor scheduling is pivotal in optimizing the performance of parallel computing systems. This paper leverages the power of Petri nets and the tool GPenSIM to model and simulate a variety of multiprocessor scheduling algorithms (the basic algorithms such as first come first serve, shortest job first, and round robin, and more sophisticated schedulers like multi-level feedback queue and Linux's completely fair scheduler). This paper presents the evaluation of three crucial performance metrics in multiprocessor scheduling (such as turnaround time, response time, and throughput) under various scheduling algorithms. However, the primary focus of the paper is to develop a robust simulation platform consisting of Petri Modules to facilitate the dynamic representation of concurrent processes, enabling us to explore the real-time interactions and dependencies in a multiprocessor environment; more advanced and newer schedulers can be tested with the simulation platform presented in this paper. [ABSTRACT FROM AUTHOR]

Due to the extremely irregular nonlinear degradation of images obtained in real underwater environments, it is difficult for existing underwater image enhancement methods to stably restore degraded underwater images, thus making it challenging to improve the efficiency of marine work. We propose a hybrid algorithm model for underwater image color restoration and texture enhancement, termed HA-Net. First, we introduce a dynamic color correction algorithm based on depth estimation to restore degraded images and mitigate color attenuation in underwater images by calculating the depth of targets and backgrounds. Then, we propose a multi-scale U-Net to enhance the network's feature extraction capability and introduce a parallel attention module to capture image spatial information, thereby improving the model's accuracy in recognizing deep semantics such as fine texture. Finally, we propose a global information compensation algorithm to enhance the output image's integrity and boost the network's learning ability. Experimental results on synthetic standard data sets and real data demonstrate that our method produces images with clear texture and bright colors, outperforming other algorithms in both subjective and objective evaluations, making it more suitable for real marine environments. [ABSTRACT FROM AUTHOR]

Deep learning-based image deblurring techniques have made great advancements, improving both processing speed and deblurring efficacy. However, existing methods still face challenges when dealing with complex blur types and the semantic understanding of images. The segment anything model (SAM), a versatile deep learning model that accurately and efficiently segments objects in images, facilitates various tasks in computer vision. This article leverages SAM's proficiency in capturing object edges and enhancing image content comprehension to improve image deblurring. We introduce the edge-sensitive focusing encoder (EFE) module, which utilizes masks generated by the SAM framework and re-weights the masked portion following SAM segmentation by detecting its features and high-frequency information. The EFE module uses the masks to locate the position of the blur in an image while identifying the intensity of the blur, allowing the model to focus more accurately on specific features. Masks with greater high-frequency information are assigned higher weights, prompting the network to prioritize them during processing. Based on the EFE module, we develop a deblurring network called the edge-sensitive focusing encoder-based convolution–normalization and attention network (EFE-CNA Net), which utilizes the EFE module to enhance the deblurring process, employs an image-mask decoder to merge features from both the image and the mask from the EFE module, and incorporates the CNA Net as its base network. This design enables the model to focus on distinct features at various locations, enhancing its learning process through the guidance provided by the EFE module and the blurred images. Testing results on the RealBlur and REDS datasets demonstrate the effectiveness of the EFE-CNA Net, achieving peak signal-to-noise ratio (PSNR) and structural similarity (SSIM) metrics of 28.77, 0.902 (RealBlur-J), 36.40, 0.956 (RealBlur-R), 31.45, and 0.919 (REDS). [ABSTRACT FROM AUTHOR]

Controllers for discrete-event systems are commonly designed using state-based formalisms, like state diagrams and Petri nets. These formalisms are strongly supported by the concept of events, which, from an automation system perspective, can be associated with a simple change in the value of a signal or more complex behavioral evolutions of the signals. In this paper, the characterization of several types of events is proposed, associated with different types of signals, such as Boolean and multivalued signals. The major goal of this characterization is to improve the compactness of the model, benefiting the editing and visual interpretation of the graphical model but keeping precise execution semantics, which in turn allows for the use of computational tools covering the different stages of system development. The behavioral model of the controller is produced using a non-autonomous class of Petri nets, the IOPT nets, and the associated IOPT-Tools, which supports the specification, simulation, property verification, and automatic code generation ready to be deployed into implementation platforms. All the types of proposed events have a behavioral sub-model executed concurrently with the main model of the controller. An application example is provided to illustrate some of the advantages of the adoption of the proposed approach, encapsulating the behavioral dependencies on the evolution of input signals into events. [ABSTRACT FROM AUTHOR]

Featured Application: The proposed research method is strictly aimed at further practical applications. The authors present the design technique aimed at the effective implementation of the modeled concurrent control system within the FPGA device. The main goal is the reduction in the logic resources of the destination FPGA by adequate modeling and optimization of the system. The proposed idea is illustrated by a real-life application of the photovoltaic control system implemented in the FPGA device from Xilinx (Artix-7 family). A novel design technique of a Petri net-based concurrent control system is proposed in this paper. The idea is oriented on the effective implementation of the system within the FPGA device. In order to reduce the resources of the targeted device, the concurrent control system is optimized by the use of the authors' techniques. The complete design flow is shown, including the modeling of the system by an interpreted Petri net, its further transformation to the hardware description language, adequate logic optimization, and final implementation within the destination FPGA. The presented method is explained by a case study example of the photovoltaic control system and compared with the already known technique. The performed experiments indicated a very high effectiveness of the proposed technique. It is shown that the photovoltaic control system designed according to the presented method reduces the logic resources of the destination FPGA device by up to 28%. [ABSTRACT FROM AUTHOR]

The accurate recognition of a brain tumor (BT) is crucial for accurate diagnosis, intervention planning, and the evaluation of post-intervention outcomes. Conventional methods of manually identifying and delineating BTs are inefficient, prone to error, and time-consuming. Subjective methods for BT recognition are biased because of the diffuse and irregular nature of BTs, along with varying enhancement patterns and the coexistence of different tumor components. Hence, the development of an automated diagnostic system for BTs is vital for mitigating subjective bias and achieving speedy and effective BT segmentation. Recently developed deep learning (DL)-based methods have replaced subjective methods; however, these DL-based methods still have a low performance, showing room for improvement, and are limited to heterogeneous dataset analysis. Herein, we propose a DL-based parallel features aggregation network (PFA-Net) for the robust segmentation of three different regions in a BT scan, and we perform a heterogeneous dataset analysis to validate its generality. The parallel features aggregation (PFA) module exploits the local radiomic contextual spatial features of BTs at low, intermediate, and high levels for different types of tumors and aggregates them in a parallel fashion. To enhance the diagnostic capabilities of the proposed segmentation framework, we introduced the fractal dimension estimation into our system, seamlessly combined as an end-to-end task to gain insights into the complexity and irregularity of structures, thereby characterizing the intricate morphology of BTs. The proposed PFA-Net achieves the Dice scores (DSs) of 87.54%, 93.42%, and 91.02%, for the enhancing tumor region, whole tumor region, and tumor core region, respectively, with the multimodal brain tumor segmentation (BraTS)-2020 open database, surpassing the performance of existing state-of-the-art methods. Additionally, PFA-Net is validated with another open database of brain tumor progression and achieves a DS of 64.58% for heterogeneous dataset analysis, surpassing the performance of existing state-of-the-art methods. [ABSTRACT FROM AUTHOR]

The supervisory control of Petri nets aims to enforce the undesired behavior as unreachable by designing a set of control places. This work presents a set cover approach to design maximally permissive supervisors. For each first-met bad marking, an integer linear programming problem is developed to obtain a control place to prohibit it. An objective function is formulated to make the maximal number of first-met bad markings forbidden. Then, we develop a set covering approach to minimize the number of selected control places. The proposed approach can guarantee the maximal permissiveness of the obtained supervisor and provide a trade-off between structural complexity and computational cost. Several examples are considered to validate the proposed method. [ABSTRACT FROM AUTHOR]

In the field of straw recycling, a cotton straw-harvesting mechanism is an important piece of agricultural equipment. The mechanistic analysis method of the harvesting mechanism is a major focus of research and development in this field. Currently, in the mechanistic analysis of the cotton straw recycling mechanism, the kinematic and mechanical analysis of the recycling mechanism is generally the main focus. There is not a lot of research based on the quantitative analysis between different recycling mechanisms. In this study, a clamped cotton straw pulling mechanism is optimized and designed, and two different pulling structures are designed. In addition, a two-dimensional modeling and analysis method is used to establish the two-dimensional equations of motion of the two pulling mechanisms, analyze the leakage and breakage rates of the two clamping structures, predict the final pulling effect, and verify the results of the field tests. According to the analysis, the belt-clamping side has more uniform clamping stress and a larger clamping contact area than the chain-clamping side, and the tangential stress on cotton straw is smaller. Based on the field-test verification, the band-clamping side had a higher pulling net rate by an average of 19.32% and a lower missed pulling rate by an average of 6.01% than the chain-clamping side. Therefore, it was determined that the main reason for the lower pulling net rate of the chain-gripped side than that of the belt-gripped side was the higher pulling breakage rate, and the secondary reason was the high leakage pulling rate. Thus, the feasibility and accuracy of the analytical method of this study are verified. [ABSTRACT FROM AUTHOR]

The production of high-quality products and efficient manufacturing processes in modern environments, where processes vary widely, is one of the most crucial issues today. Statistical process control (SPC) and process mining (PM) effectively trace and enhance the manufacturing processes. In this direction, this paper proposes an innovative approach involving SPC and PM strategies to empower the manufacturing environment. SPC monitors key performance indicators (KPIs) and identifies out-of-control processes that deviate from specification limits, while PM discovery techniques are applied for those abnormal processes to extract the actual process flow from event logs and model it using Petri nets. Different enhancement techniques in PM, such as decision rules and root cause analysis, are then used to return the process to control and prevent future deviations. The application of the integrated SPC–PM approach is shown through case studies of production processes. SPC charts found that over 6% of processes exceeded specification limits. At the same time, PM methodologies revealed that prolonged times for the 'Quality Control' activity is the fundamental factor increasing the cycle time. Moreover, decision tree analysis provides rules for decreasing the cycle times of unbalanced processes. The absence of a transition from the 'Return from Waiting' activity to 'Packing and Shipment' is a critical factor in decreasing cycle times, as is the shift information. Our newly proposed methodology, which combines process analysis from PM with statistical monitoring from SPC, ensures operational excellence and consistent quality in manufacturing. This study illustrates the application of the proposed methodology through a case study in production processes, highlighting its effectiveness in identifying and addressing process deviations. [ABSTRACT FROM AUTHOR]

The mechatronic industry is currently subject to huge changes challenging it to offer products matching individual customer requirements at competitive prices. The design of such products calls for sophisticated and complex components integration following different technologies. Since we are on the cusp of the Fourth Industrial Revolution, in which the world of mechatronic production, network connectivity, the Internet of Things, and cyber-physical systems are correlated, the complexity of these systems increases exponentially, and we are talking about advanced mechatronic systems. To assist these changes, various methods, sweeping all project phases, are used by business houses. Predictive dependability assessment in the earlier design stage is considered a powerful metric used to evaluate the performances of different kinds of mechatronic products before the production phase. Altogether, dependability analysis ties the design directly to the desired functionality, operability, and integrity of the system. This paper explores an approach to assessing the dependability attributes, reliability, availability, and maintainability (RAM), of repairable mechatronic systems based on timed colored Petri nets and a Monte Carlo simulation, integrating simultaneously diverse components technologies: mechanical, electronic, and software. The proposed approach is tested taking the case of a regenerative braking system. The methodology appears to be efficient for evaluating predictive RAM indicators (MTTFF, MTTR, MTBF...) for the whole system and for each individual component separately. [ABSTRACT FROM AUTHOR]

Flight delay identification is an important way to coordinate the operation time of airport ground service providers and improve the efficiency of airport operations. By analyzing the flight turnaround operation process, considering the randomness and synchronization of the turnaround process, and using Colored Petri Nets and Python (4.0.1), we explore the correlation between various links in the flight turnaround process and the take-off delay at the next station. This paper is committed to improving the service performance of airports and airlines, dynamically predicting flight delays, and providing guidance for avoiding excessive time in the actual operation of bad combinations. The results show that there are six kinds of bad combinations in the departure slip-out link, which is the most likely to affect the transit time. The maximum lifting degree in the bad combination is 2.043, and the maximum average delay time in the bad combination is 22.5 min. When the combination of passenger boarding and departure slip-out time is too long, it has a great positive correlation with delay. When the other links are in a state of being able to pass the station on time, the departure time and baggage loading and unloading are the two links that most affect the flight delay value. [ABSTRACT FROM AUTHOR]

In the context of small unmanned aerial vehicles (UAVs), infrared imaging faces challenges such as low quality, difficulty in detecting small targets, high false alarm rates, and computational resource constraints. To address these issues, we introduce AIMED-Net, an enhancing infrared small target detection net in UAVs with multi-layer feature enhancement for edge computing. Initially, the network encompasses a multi-layer feature enhancement architecture for infrared small targets, including a generative adversarial-based shallow-feature enhancement network and a detection-oriented deep-feature enhancement network. Specifically, an infrared image-feature enhancement method is proposed for the shallow-feature enhancement network, employing multi-scale enhancement to bolster target detection performance. Furthermore, within the YOLOv7 framework, we have developed an improved object detection network integrating multiple feature enhancement techniques, optimized for infrared targets and edge computing conditions. This design not only reduces the model's complexity but also enhances the network's robustness and accuracy in identifying small targets. Experimental results obtained from the HIT-UAV public dataset indicate that, compared to YOLOv7s, our method achieves a 2.5% increase in F1 score, a 6.1% rise in AP for detecting OtherVehicle targets, and a 2.6% improvement in mAP across all categories, alongside a 15.2% reduction in inference time on edge devices. Compared to existing state-of-the-art approaches, our method strikes a balance between detection efficiency and accuracy, presenting a practical solution for deployment in aerial edge computing scenarios. [ABSTRACT FROM AUTHOR]

It is well known that if a poset satisfies Property A and its dual form, then the o-convergence and o 2 -convergence in the poset are equivalent. In this paper, we supply an example to illustrate that a poset in which the o-convergence and o 2 -convergence are equivalent may not satisfy Property A or its dual form, and carry out some further investigations on the equivalence of the o-convergence and o 2 -convergence. By introducing the concept of the local Frink ideals (the dually local Frink ideals) and establishing the correspondence between ID-pairs and nets in a poset, we prove that the o-convergence and o 2 -convergence of nets in a poset are equivalent if and only if the poset is ID-doubly continuous. This result gives a complete solution to the problem of E.S. Wolk in two modes of order convergence, which states under what conditions for a poset the o-convergence and o 2 -convergence in the poset are equivalent. [ABSTRACT FROM AUTHOR]

Accurate and reliable pose estimation of boom-type roadheaders is the key to the forming quality of the tunneling face in coal mines, which is of great importance to improve tunneling efficiency and ensure the safety of coal mine production. The multi-laser-beam target-based visual localization method is an effective way to realize accurate and reliable pose estimation of a roadheader body. However, the complex background interference in coal mines brings great challenges to the stable and accurate segmentation and extraction of laser beam features, which has become the main problem faced by the long-distance visual positioning method of underground equipment. In this paper, a semantic segmentation network for underground laser beams in coal mines, RCEAU-Net, is proposed based on U-Net. The network introduces residual connections in the convolution of the encoder and decoder parts, which effectively fuses the underlying feature information and improves the gradient circulation performance of the network. At the same time, by introducing cascade multi-scale convolution in the skipping connection section, which compensates for the lack of contextual semantic information in U-Net and improves the segmentation effect of the network model on tiny laser beams at long distance. Finally, the introduction of an efficient multi-scale attention module with cross-spatial learning in the encoder enhances the feature extraction capability of the network. Furthermore, the laser beam target dataset (LBTD) is constructed based on laser beam target images collected from several coal mines, and the proposed RCEAU-Net model is then tested and verified. The experimental results show that, compared with the original U-Net, RCEAU-Net can ensure the real-time performance of laser beam segmentation while increasing the Accuracy by 0.19%, Precision by 2.53%, Recall by 22.01%, and Intersection and Union Ratio by 8.48%, which can meet the requirements of multi-laser-beam feature segmentation and extraction under complex backgrounds in coal mines, so as to further ensure the accuracy and stability of long-distance visual positioning for boom-type roadheaders and ensure the safe production in the working face. [ABSTRACT FROM AUTHOR]

Precise and rapid detection of seatbelts is an essential research field for intelligent traffic management. In order to improve the detection precision of seatbelts and speed up algorithm inference velocity, a lightweight seatbelt detection algorithm is proposed. Firstly, by adding the G-ELAN module designed in this paper to the YOLOv7-tiny network, the optimization of construction and reduction of parameters are accomplished, and the ResNet is compressed with the channel pruning approach to decrease computational overheads. Then, the Mish activation function is utilized to replace the Leaky Relu in the neck to enhance the non-linear competence of the network. Finally, the triplet attention module is integrated into the model after pruning to make up for the underlying performance reduction caused by the previous stage and upgrade overall detection precision. The experimental results based on the self-built seatbelt dataset showed that, compared to the initial network, the Mean Average Precision (mAP) achieved by the proposed GM-YOLOv7 was improved by 3.8%, while the volume and the computation amount were lowered by 20% and 24.6%, respectively. Compared with YOLOv3, YOLOX, and YOLOv5, the mAP of GM-YOLOv7 increased by 22.4%, 4.6%, and 4.2%, respectively, and the number of computational operations decreased by 25%, 63%, and 38%, respectively. In addition, the accuracy of the improved RST-Net increased to 98.25%, while the parameter value was reduced by 48% compared to the basic model, effectively improving the detection performance and realizing a lightweight structure. [ABSTRACT FROM AUTHOR]

Atherosclerosis, a chronic inflammatory and oxidative stress-mediated disease impacting the arterial system, stands as a primary cause of morbidity and mortality worldwide. The complexity of this disease, driven by numerous factors, requires a thorough investigation of its underlying mechanisms. In our study, we explore the complex interplay between cholesterol homeostasis, macrophage dynamics, and atherosclerosis development using a Petri net-based model anchored in credible, peer-reviewed biological and medical research. Our findings underscore the significant role of macrophage colony-stimulating factor (M-CSF) inhibition in reducing atherosclerotic plaque formation by modulating inflammatory responses and lipid accumulation. Furthermore, our model highlights the therapeutic potential of targeting the C-X-C motif ligand 12 (CXCL12)/ C-X-C motif chemokine receptor type 4 (CXCR4) pathway to hinder hematopoietic stem and progenitor cells' (HSPCs') mobilization and plaque development. Based on the results obtained, which are in agreement with current studies, additional strategies are also proposed, such as decreasing M1 macrophage polarization for therapeutic gains, opening the door to future research and novel treatment approaches. [ABSTRACT FROM AUTHOR]

This paper explores the concept of proportional lumpability as an extension of the original definition of lumpability, addressing the challenges posed by the state space explosion problem in computing performance indices for large stochastic models. Lumpability traditionally relies on state aggregation techniques and is applicable to Markov chains demonstrating structural regularity. Proportional lumpability extends this idea, proposing that the transition rates of a Markov chain can be modified by certain factors, resulting in a lumpable new Markov chain. This concept facilitates the derivation of precise performance indices for the original process. This paper establishes the well-defined nature of the problem of computing the coarsest proportional lumpability that refines a given initial partition, ensuring a unique solution exists. Additionally, a polynomial time algorithm is introduced to solve this problem, offering valuable insights into both the concept of proportional lumpability and the broader realm of partition refinement techniques. The effectiveness of proportional lumpability is demonstrated through a case study that consists of designing a model to investigate selfish mining behaviors on public blockchains. This research contributes to a better understanding of efficient approaches for handling large stochastic models and highlights the practical applicability of proportional lumpability in deriving exact performance indices. [ABSTRACT FROM AUTHOR]

The video game Factorio is a popular real-time strategy game that hosts a variety of gameplay scenarios analogous to real-world problems such as factory building, pipeline optimization, and conveyor belt logistics. It also considers environmental costs such as pollution and energy consumption. This game focuses on automation and resource management within the context of creating and maintaining factories. Players are challenged to design efficient factories, automate production, control energy consumption, and balance resource utilization, all while defending against environmental challenges such as pollution and hostile enemies. Factorio is a complex software; however, studies have demonstrated its ability to enhance student satisfaction when integrated as an educational module at the university level. This paper aims to utilize the power of Petri Net theory and the practical tool GPenSIM to model and simulate several Factorio pipelines and score them against one another, exploring which pipeline configuration is optimal. The primary objective is to make a mathematical model (Petri Net) to better understand the game's complex mechanisms, identify bottlenecks within the system, and explore opportunities for optimization within the network of modules. The insights gained from this paper may find practical applications in real-world scenarios. [ABSTRACT FROM AUTHOR]

Current testing methods for autonomous driving systems primarily focus on simple traffic scenarios, generating test cases based on traffic accidents, while research on generating edge test cases for complex driving environments by traffic regulations is not adequately comprehensive. Therefore, we propose a method for scenario modeling and violation testing using an autonomous driving system based on traffic regulations named TraModeAVTest. Initially, TraModeAVTest constructs a Petri net model for complex scenarios based on the combination relationships of basic traffic regulation scenarios and verifies the consistency of the model's design with traffic regulation requirements using formal methods, to provide a representation of traffic regulation scenario models for the violation testing of autonomous driving systems. Subsequently, based on the coverage criteria of the Petri net model, it utilizes a search strategy to generate model paths that represent traffic regulations, and employs a parameter combination method to generate test cases that cover the model paths, to test the violation behaviors of autonomous driving systems. Finally, simulation experiment results on the Baidu Apollo demonstrate that the test cases representing traffic regulations generated by TraModeAVTest can effectively identify the behaviors of autonomous vehicles violating traffic regulations, and TraModeAVTest can effectively improve the efficiency of generating different types of violation scenarios. [ABSTRACT FROM AUTHOR]

In recent years, graph convolutional networks (GCNs) have attracted increasing attention in hyperspectral image (HSI) classification owing to their exceptional representation capabilities. However, the high computational requirements of GCNs have led most existing GCN-based HSI classification methods to utilize superpixels as graph nodes, thereby limiting the spatial topology scale and neglecting pixel-level spectral–spatial features. To address these limitations, we propose a novel HSI classification network based on graph convolution called the spatial-pooling-based graph attention U-net (SPGAU). Specifically, unlike existing GCN models that rely on fixed graphs, our model involves a spatial pooling method that emulates the region-growing process of superpixels and constructs multi-level graphs by progressively merging adjacent graph nodes. Inspired by the CNN classification framework U-net, SPGAU's model has a U-shaped structure, realizing multi-scale feature extraction from coarse to fine and gradually fusing features from different graph levels. Additionally, the proposed graph attention convolution method adaptively aggregates adjacency information, thereby further enhancing feature extraction efficiency. Moreover, a 1D-CNN is established to extract pixel-level features, striking an optimal balance between enhancing the feature quality and reducing the computational burden. Experimental results on three representative benchmark datasets demonstrate that the proposed SPGAU outperforms other mainstream models both qualitatively and quantitatively. [ABSTRACT FROM AUTHOR]

Modeling and verification of the correct behavior of embedded real-time systems with strict timing constraints is a well-known and important problem. Failing to fulfill a deadline in system operation can have severe consequences in the practical case. This paper proposes an approach to formal modeling and schedulability analysis. A novel extension of Petri Nets named Constraint Time Petri Nets (C-TPN) is developed, which enables the modeling of a collection of interdependent real-time tasks whose execution is constrained by the use of priority and shared resources like processors and memory data. A C-TPN model is reduced to a network of Timed Automata in the context of the popular Uppaal toolbox. Both functional and, most importantly, temporal properties can be assessed by exhaustive model checking and/or statistical model checking based on simulations. This paper first describes and motivates the proposed C-TPN modeling language and its formal semantics. Then, a Uppaal translation is shown. Finally, three models of embedded real-time systems are considered, and their properties are thoroughly verified. [ABSTRACT FROM AUTHOR]

To ensure opacity, it is optimal to retain as many as possible occurring event sequences. Contrary to this problem, the other optimal goal is to preserve the minimal occurring event sequences. Based on the choosing cost, an optimal opacity-enforcing problem with minimal discount choosing cost is presented under two constraints in this paper. The first constraint is the opacity of the controlled system. The second is the retention of the secret to the maximum. To solve the model, two scenarios on opacity are considered. For the two scenarios, some algorithms are presented to achieve the optimal solution for the model by using the method of dynamic programming. Then, the solutions produced by the algorithms are proved to be correct by theoretical proof. Finally, some illustrations and an application example on location privacy protection for the algorithms are given. [ABSTRACT FROM AUTHOR]