A system is said to be opaque if a given secret behavior remains (uncertain) an intruder who can partially observe activities. This work addresses the verification of state-based opacity in systems modeled with Petri nets. The defined as set states. More precisely, two properties are considered: current-state and initial-state opacity. We show that both problems bounded nets efficiently solved by using compact representation reachability graph, called basis graph (BRG). approach practically...

In this paper, a compact representation of the reachability graph Petri net is proposed. The transition set partitioned into subsets explicit and implicit transitions in such way that subnet induced by does not contain directed cycles. firing can be abstracted so completely characterized subset reachable markings called basis makings. We show to determine max-cardinality-TI partition an NP-hard problem, but max-set-TI determined polynomial time. generalized version marking problem solved...

Observation structures considered for Petri net generators usually assume that the firing of transitions may be observed through a static mask and marking some places measurable. These observation structures, however, are rather limited, namely they do not cover all cases practical interest where complex observations possible. We consider in this paper more general ones, by correspondingly defining two new classes generators: labeled nets with outputs (LPNOs) adaptive (ALPNs). To compare...

Carbon nanotubes (CNTs) are a promising material for humidity sensors and wearable electronics due to their solution capability, good flexibility, high conductivity. However, the performance of CNT-based is limited by low sensitivity slow response. Herein CNTs hydrophilic polymers were mixed form composite. The hydrophilicity network structure empowered with response 171% fast response/recovery time 23 s/10 s. Owing sticky flexible polymers, showed strong adhesion PET substrate exhibited...

Space weather significantly impacts the Earth’s magnetic field and can severely disrupt power systems. As modern society increasingly relies on systems, space effects cascade into other sectors, with severe events posing catastrophic economic risks. Research losses caused by remains in its early stages, leading to potential inadequacies risk assessment mitigation measures heightening vulnerability of social This study employs Dynamic Inoperability Input-Output Model assess GDP...

Severe geomagnetic storms can induce geomagnetically induced currents (GICs) in infrastructures like power grids, leading to transformer overheating, voltage instability, and outages. With the rapid expansion large-scale deployment of these systems worldwide, space weather effects have become an increasing concern. To address urgent need assess impacts weather, a systematic modelling framework is essential. However, absence complete grid data has hindered development GICs model during...

A system is said to be language opaque if the intruder cannot infer generated event sequence belongs a secret based on its partial observation. In this paper we address problem of verifying language-based opacity in systems modeled by bounded labeled Petri nets. We generalize notion strict deal with case where only interested subset transitions. Furthermore, show that identical for special class secrets. verifier constructed analyze under assumption cares about observable

A Petri net system is said to be initial-state opaque if its initial state remains an external observer (called intruder). In other words, the intruder never able ascertain that belongs a given set of states secret) based on observation system's evolution. This paper addresses problem verifying opacity in discrete event systems (DES) modeled by labeled nets. An efficient approach proposed notion basis reachability graph (BRG).

This paper addresses the problem of detection and prevention cyber attacks in discrete event systems where supervisor communicates with plant via network channels. Random control delays may occur such networked systems, hence could be affected. Furthermore, there is an attacker targeting vulnerable actuators. The can corrupt input generated by supervisor, aims at driving to unsafe states. We propose a new approach model closed-loop system subject attacks. notion AE-safe controllability...

Abstract The quest for reliable vehicle navigation in urban environments has led the integration of Light Detection and Ranging (LiDAR) Odometry (LO) with Global Navigation Satellite Systems (GNSS) Inertial Measurement Units (IMU). However, performance integrated system is limited by a lack accurate LO error modeling. In this paper, we propose weighted GNSS/IMU/LO integration-based novel model. Squared Exponential Gaussian Progress Regression (SE-GPR) based model developed considering...

This paper addresses the problem of current-state opacity discrete event systems (DES) modeled with Petri nets. A system is said to be opaque if intruder who only has partial observations on system's behavior never able infer that current state within a set secret states. Based notion basis markings, an efficient approach verifying in bounded nets proposed, without computing whole reachability or exhaustively enumerating markings consistent observation. An example showing efficiency presented.

Opacity is an important information secure property. A system said to be infinite-step opaque if the intruder never able ascertain that or has been in a secret state at some time, based on its observation of evolution. This work aims verify opacity discrete event systems modeled with labeled Petri nets. Based notion basis reachability graph, new structure called two-way observer proposed check bounded system, which shown more efficient than standard method graph.

The consensusability and global optimality problems are solved for the discrete-time linear multiagent system (MAS) with marginally stable strictly unstable dynamics. A unified framework is proposed by capturing maximal disc-guaranteed gain margin (GGM) of quadratic regulator (LQR). Sufficient necessary conditions on established. Two bounds consensus region derived only in terms eigenvalues agent' For single-input MAS, proving that radius exactly equals reciprocal Mahler measure dynamics, we...

In this paper a method to recognize the set of consistent markings in labelled Petri nets is proposed. method, unobservable transitions are partitioned into pseudo-observable and strictly ones, subnet induced by latter acyclic. The reach marking can be characterized union several basis markings, called representative subnet. linear algebraic system based on those markings. Based graph, current estimation problem for net efficiently solved. This does not require assumption that

The development of cyber-physical systems (CPS) has brought much attention researchers to cyber-attack and cyber-security. A sensor attacker targeting on a supervised discrete event system can modify set readings cause the closed-loop reach undesirable states. In this letter, we propose new attack detection mechanism under which supervisor only needs keep track last observable received. Given plant enforcing state specification, define <italic xmlns:mml="http://www.w3.org/1998/Math/MathML"...

This paper presents a MATLAB toolbox, called PetriBaR, for the analysis and control of Petri nets. PetriBaR is package functions devoted to basic net (including computation T-invariants, siphons, reachability graph, etc.), monitor design, analysis, state estimation, fault diagnosis, opacity verification. In particular, verification exploit construction Basis Reachability Graph avoid exhaustive enumeration reachable set, thus leading significant advantages in terms computational complexity....