Search

Mathematical optimization is ubiquitous in modern applications. However, in practice, we often need to use nonlinear optimization models, for which the existing optimization tools such as Cplex or Gurobi may not be directly applicable and an (error-prone) manual transformation often has to be done. Thus, to address this issue, in this paper we investigate the problem of automatically verifying and synthesizing reductions, the solution of which may allow an automatic linearization of nonlinear models. We show that the synthesis of reductions can be formulated as an $\exists^* \forall^*$ synthesis problem, which can be solved by an SMT solver via the counter-example guided inductive synthesis approach (CEGIS)., Comment: 4 pages, conference

A survey was designed to inquire about the practice of proton SBRT treatment for prostate cancer. The survey was distributed to all 30 proton therapy centers in the United States that participate in the National Clinical Trial Network in Feb. 2023. The survey focused on usage, patient selection criteria, prescriptions, target contours, dose constraints, treatment plan optimization and evaluation methods, patient-specific QA, and IGRT methods. Results: We received responses from 25 centers (83% participation). Only 8 respondent proton centers (32%) reported performing SBRT of the prostate. The remaining 17 centers cited three primary reasons for not offering this treatment: no clinical need, lack of volumetric imaging, and/or lack of clinical evidence. Only 1 center cited the reduction in overall reimbursement as a concern for not offering prostate SBRT. Several common practices among the 8 centers offering SBRT for the prostate were noted, such as using Hydrogel spacers, fiducial markers, and MRI for target delineation. Most proton centers (87.5%) utilized pencil beam scanning (PBS) delivery and completed Imaging and Radiation Oncology Core (IROC) phantom credentialing. Treatment planning typically used parallel opposed lateral beams, and consistent parameters for setup and range uncertainties were used for plan optimization and robustness evaluation. Measurements-based patient-specific QA, beam delivery every other day, fiducial contours for IGRT, and total doses of 35-40 GyRBE were consistent across all centers. However, there was no consensus on the risk levels for patient selection. Conclusion: Prostate SBRT is used in about 1/3 of proton centers in the US. There was a significant consistency in practices among proton centers treating with proton SBRT. It is possible that the adoption of proton SBRT may become more common if proton SBRT is more commonly offered in clinical trials.

Stereotactic body radiation therapy (SBRT) and hypofractionation using pencil-beam scanning (PBS) proton therapy (PBSPT) is an attractive option for thoracic malignancies. Combining the advantages of target coverage conformity and critical organ sparing from both PBSPT and SBRT, this new delivery technique has great potential to improve the therapeutic ratio, particularly for tumors near critical organs. Safe and effective implementation of PBSPT SBRT/hypofractionation to treat thoracic malignancies is more challenging than the conventionally-fractionated PBSPT due to concerns of amplified uncertainties at the larger dose per fraction. NRG Oncology and Particle Therapy Cooperative Group (PTCOG) Thoracic Subcommittee surveyed US proton centers to identify practice patterns of thoracic PBSPT SBRT/hypofractionation. From these patterns, we present recommendations for future technical development of proton SBRT/hypofractionation for thoracic treatment. Amongst other points, the recommendations highlight the need for volumetric image guidance and multiple CT-based robust optimization and robustness tools to minimize further the impact of uncertainties associated with respiratory motion. Advances in direct motion analysis techniques are urgently needed to supplement current motion management techniques., Comment: 36 pages, 4 figures, 4 tables

Highly automated assembly lines enable significant productivity gains in the manufacturing industry, particularly in mass production condition. Nonetheless, challenges persist in job scheduling for make-to-job and mass customization, necessitating further investigation to improve efficiency, reduce tardiness, promote safety and reliability. In this contribution, an advantage actor-critic based reinforcement learning method is proposed to address scheduling problems of distributed flexible assembly lines in a real-time manner. To enhance the performance, a more condensed environment representation approach is proposed, which is designed to work with the masks made by priority dispatching rules to generate fixed and advantageous action space. Moreover, a Monte-Carlo tree search based soft shielding component is developed to help address long-sequence dependent unsafe behaviors and monitor the risk of overdue scheduling. Finally, the proposed algorithm and its soft shielding component are validated in performance evaluation., Comment: 7 pages,5 figures, 4 tables, conference paper

This work investigates the problem of synthesizing fortified supervisors against covert actuator attackers. For a non-resilient supervisor S, i.e., there exists at least a covert actuator attacker that is capable of inflicting damage w.r.t S, a fortified supervisor S' satisfies two requirements: 1) S' is resilient against any covert actuator attacker, and 2) the original closed-behavior of the closed-loop system under S is preserved, that is, S' is control equivalent to S. By designing a sound and complete procedure, we show the problem of determining the existence of a fortified supervisor against covert actuator attackers is decidable. We also discuss how to extend the decidability result to the case against the worst-case attacker., Comment: arXiv admin note: substantial text overlap with arXiv:2205.02383

Purpose:The recently proposed IPO-IMPT framework allows simultaneous optimization of dose, dose rate, and LET for FLASH treatment planning. Finding solutions to IPO-IMPT is difficult due to computational intensiveness. Nevertheless, an inverse solution that simultaneously specifies the geometry of a sparse filter and weights of a proton intensity map is desirable for both clinical and preclinical applications. Such solutions can reduce effective biological dose to organs at risk in cancer patients as well as reduce the number of animal irradiations needed to derive extra biological dose models in preclinical studies. Methods:Unlike our initial forward heuristic, this inverse IPO-IMPT solution includes simultaneous optimization of sparse range compensation, sparse range modulation, and spot intensity. The daunting computational tasks vital to this endeavor were resolved iteratively with a distributed computing framework to enable Simultaneous Intensity and Energy Modulation and Compensation (SIEMAC). SIEMAC was demonstrated on a human lung cancer patient and a minipig. Results:SIEMAC improves maps of spot intensities and patient-field-specific sparse range compensators and range modulators. For the lung cancer patient, at our max nozzle current of 300 nA, dose rate coverage above 100 Gy/s increased from 57% to 96% in the lung and from 93% to 100% in the heart, and LET coverage above 4 keV/um dropped from 68% to 9% in the lung and from 26% to <1% in the heart. For a simple minipig plan, the FWHM of the dose, dose rate, and LET distributions decreased by 30%, 1.6%, and 57%, respectively, again with similar target dose coverage, thus reducing uncertainty in these quantities for preclinical studies. Conclusion:The inverse solution to IPO-IMPT demonstrated the capability to simultaneously modulate sub-spot proton energy and intensity distributions for clinical and preclinical studies.

FLASH is a new treatment modality that requires optimization of dose, dose rate, and LET. Here we validate these three quantities under FLASH conditions, which includes the quantum uncertainty in the time-dependent instantaneous dose rate (IDR) curves and LET spectra that underlie the newly proposed integrated optimization framework. Measurements of dose, IDR, and LET were performed at the Emory Proton Therapy Center using a FLASH proton beam with a nominal energy of 250 MeV and a 3D printed ridge filter. Because 3D printing resin is made from a proprietary chemical formula, we developed a method for realistically characterizing and modeling the material in simulations. Absolute dose in 3D space was measured using a 2D MatriXX PT detector as well as by a novel 4D multi-layer strip ionization chamber (MLSIC), which also simultaneously measures IDR. Further timing data was measured in the secondary beam by detecting prompt gammas using a Minipix Timepix3; a second detector, Advapix Timepix3, was used to measure LET. To account for the quantum mechanical nature of particle transport, we developed a technique for detecting individual protons within a high flux primary beam, which was necessary for properly measuring LET spectra. TOPAS simulations agreed with measurement, with absolute dose typically having a gamma passing rate of at least 95% (3 mm/3% criteria). Likewise, IDR and LET showed good agreement, with averaged IDR values agreeing within 0.3% with fluctuations on the order of 10%, and LET distributions overlapping by at least 85% and showing an increase in high LET components (greater than 4 keV/um) with increasing depth. As LET and FLASH optimization continues to grow in popularity, measuring IDR, LET, and dose will become even more important, and we expect that the methods described here will prove to be useful tools in radiotherapy treatment planning and QA.

Proton FLASH therapy leverages ultra-high dose-rate radiation to enhance the sparing of organs at risk without compromising tumor control probability. To prepare for the delivery of high doses to targets, we aim to develop a deep learning-based image-guide framework to enable fast volumetric image reconstruction for accurate target localization before FLSAH beam delivery. The proposed framework comprises four modules, including orthogonal kV x-ray projection acquisition, DL-based volumetric image generation, image quality analyses, and water equivalent thickness evaluation. We investigated volumetric image reconstruction using four kV projection pairs with different source angles. Thirty lung patients were identified from the institutional database, and each patient contains a four-dimensional computed tomography dataset with ten respiratory phases. The retrospective patient study indicated that the proposed framework could reconstruct patient volumetric anatomy, including tumors and organs at risk from orthogonal x-ray projections. Considering all evaluation metrics, the kV projections with source angles of 135 and 225 degrees yielded the optimal volumetric images. The proposed framework has been demonstrated to reconstruct volumetric images with accurate lesion locations from two orthogonal x-ray projections. The embedded WET module can be used to detect potential proton beam-specific patient anatomy variations. The framework can deliver fast volumetric image generation and can potentially guide treatment delivery systems for proton FLASH therapy.

Ultra-high dose rate (FLASH) proton planning with only transmission beams (TBs) has limitations in normal tissue sparing. The single-energy spread-out Bragg peaks (SESOBPs) of FLASH dose rate have been demonstrated feasible for proton FLASH planning. A hybrid inverse optimization method was developed to combine the TBs and SESOBPs (TB-SESOBP) for FLASH planning. The SESOBPs were generated from spreading out the BPs by pre-designed general bar ridge filters and placed at the central target by range shifters to obtain a uniform dose within the target. The SESOBPs and TBs were fully sampled field-by-field allowing automatic spot selection and weighting in the optimization process. The TB-SESOBP plans were validated in comparison with the TB only (TB-only) plans and the plans with the combination of TBs and BPs (TB-BP) regarding 3D dose and dose rate distributions for five lung cases. Comparing to the TB-only plans, the mean spinal cord D1.2cc drastically reduced 41%, the mean lung V7Gy and V7.4Gy moderately reduced by up to 17% and the target dose homogeneity slightly increased in the TB-SESOBP plans. Comparable dose homogeneity was achieved in both TB-SESOBP and TB-BP plans. Besides, prominent improvements were achieved in lung sparing for the cases of relatively large targets by the TB-SESOBP plans comparing to the TB-BP plans. The targets were fully covered with the FLASH dose rate in all the three plans. For the OARs, V40Gy/s = 100% was achieved by the TB-only plans while V40Gy/s > 85% was obtained by the other two plans. We have demonstrated that the hybrid TB-SESOBP planning was feasible to achieve FLASH dose rate for proton therapy. The hybrid TB-SESOBP planning has great potential in improving OAR sparing while maintaining high target dose homogeneity, and can be potentially implemented for adaptive radiotherapy.

We aim to investigate the feasibility of online monitoring of irradiation time (IRT) and scan time for FLASH radiotherapy using a pixelated semiconductor detector. Measurements of the time structure of FLASH irradiations were performed using fast, pixelated spectral detectors, AdvaPIX-TPX3 and Minipix-TPX3. The latter has a fraction of its sensor coated with a neutron sensitive material. With little or no dead time and an ability to resolve events that are closely spaced in time (tens of ns), both detectors can accurately determine IRTs as long as pile-ups are avoided. To avoid pile-ups, we placed the detectors beyond the Bragg peak or at a large scattering angle. We acquired prompt gamma rays and secondary neutrons and calculated IRTs based on timestamps of the first (beam-on) and the last (beam-off) charged species. We also measured scan times in x, y, and diagonal directions. We performed these measurements for a single spot, a small animal field, a patient field, and a ridge filter optimized field to demonstrate in vivo online monitoring of IRT. All measurements were compared to vendor log files. Differences between measurements and log files for a single spot, a small animal field, and a patient field were within 1%, 0.3% and 1%, respectively. In vivo monitoring of IRTs was accurate within 0.1% for AdvaPIX-TPX3 and within 6.1% for Minipix-TPX3. The scan times in x, y, and diagonal directions were 4.0, 3.4, and 4.0 ms, respectively. Overall, the AdvaPIX-TPX3 can measure FLASH IRTs within 1% accuracy, indicating that prompt gamma rays are a good surrogate for primary protons. The Minipix-TPX3 showed a higher discrepancy, suggesting a need for further investigation. The scan times (3.4 \pm 0.05 ms) in the 60-mm distance of y-direction were less than (4.0 \pm 0.06 ms) in the 24-mm distance of x-direction, confirming the much faster scanning speed of the Y magnets than that of X., Comment: 11 pages, 5 figures

Recently, shoot-through proton FLASH has been proposed where the highest energy is extracted from the cyclotron to maximize the dose rate (DR). Even though our proton pencil beam scanning system can deliver 250 MeV (the highest energy), it is not typical to use 250 MeV protons for routine clinical treatments and as such 250 MeV may not have been characterized in the commissioning. In this study, we aim to characterize 250 MeV protons from Varian ProBeam system for FLASH RT as well as assess the ability of clinical monitoring ionization chamber (MIC) for FLASH-readiness. We measured data needed for beam commissioning: integral depth dose (IDD) curve, spot sigma, and absolute dose calibration. To evaluate MIC, we measured output as a function of beam current. To characterize a 250 MeV FLASH beam, we measured: (1) central axis DR as a function of current and spot spacing and arrangement, (2) for a fixed spot spacing, the maximum field size that still achieves FLASH DR (i.e., > 40 Gy/s), (3) DR reproducibility. All FLASH DR measurements were performed using ion chamber for the absolute dose and irradiation times were obtained from log files. We verified dose measurements using EBT-XD films and irradiation times using a fast, pixelated spectral detector. R90 and R80 from IDD were 37.58 and 37.69 cm, and spot sigma at isocenter were {\sigma}x=3.336 and {\sigma}y=3.332 mm, respectively. The absolute dose output was measured as 0.377 GyE*mm2/MU for the commissioning conditions. Output was stable for beam currents up to 15 nA, and it gradually increased to 12-fold for 115 nA. DR depended on beam current, spot spacing and arrangement and could be reproduced within 4.2% variations. Even though FLASH was achieved and the largest field size that delivers FLASH DR was determined as 35x35 mm2, current MIC has DR dependence and users should measure DR each time for their FLASH applications., Comment: 11 pages, 6 figures

Purpose: Patient-specific ridge filters can modulate proton energy to obtain a conformal dose. We describe a new framework for optimization of filter design and spot maps to meet the unique demands of FLASH radiotherapy. We demonstrate an Integrated Biological Optimization IMPT (IBO-IMPT) approach for optimization of dose, dose-averaged dose rate (DADR), and dose-averaged LET (LETd). Methods: We developed inverse planning software to design patient-specific ridge filters that spread the Bragg peak from a fixed-energy, 250 MeV beam to a proximal beam-specific planning target volume. The software optimizes patient-specific ridge filter and uses a Monte Carlo calculation engine, based on Geant4, to provide dose and LET influence matrices. Plan optimization, using matRAD, accommodates the IBO-IMPT objective function considering dose, dose rate, and LET simultaneously with minimum MU constraints. The framework enables design of both regularly spaced and sparse-optimized ridge filters, which allow faster delivery and selective LET optimization. Volume distributions and histograms for dose, DADR, and LETd are compared using evaluation structures specific to the heart and lung. Results: We used IBO-IMPT to design ridge filters for a central lung tumor patient. The IBO-IMPT framework selectively spared heart and lung by reducing LET and increasing dose rate, relative to IMPT planning. Sparse-optimized ridge filters were superior to regularly spaced ridge filters in dose rate. Together, these innovations substantially increased the DADR in the heart and lung while maintaining good target coverage. The volume that received a FLASH dose rate of higher 40 Gy/second increased by 31% for heart and 50% for lung. Conclusion: This proof-of-concept study demonstrates the feasibility of using an IBO-IMPT framework to accomplish proton FLASH SBPT, accounting for dose, DADR, and LETd simultaneously.

This work investigates the problem of synthesizing obfuscated supervisors against covert actuator attackers. For a non-resilient supervisor S, for which there exist some covert actuator attackers that are capable of inflicting damage, we propose an algorithm to compute all the obfuscated supervisors, with the requirements that: 1) any obfuscated supervisor S' is resilient against any covert actuator attacker, and 2) the original closed-behavior of the closed-loop system under S is preserved, that is, any obfuscated supervisor S' is control equivalent to the original non-resilient supervisor S. We prove that the designed algorithm to synthesize obfuscated supervisors against covert actuator attack is sound and complete.

In this paper, we consider the problem of synthesizing the supremal covert damage-reachable attacker, in the setup where the model of the supervisor is unknown to the adversary but the adversary has recorded a (prefix-closed) finite set of observations of the runs of the closed-loop system. The synthesized attacker needs to ensure both the damage-reachability and the covertness against all the supervisors which are consistent with the given set of observations. There is a gap between the de facto supremality, assuming the model of the supervisor is known, and the supremality that can be attained with a limited knowledge of the model of the supervisor, from the adversary's point of view. We consider the setup where the attacker can exercise sensor replacement/deletion attacks and actuator enablement/disablement attacks. The solution methodology proposed in this work is to reduce the synthesis of the supremal covert damage-reachable attacker, given the model of the plant and the finite set of observations, to the synthesis of the supremal safe supervisor for certain transformed plant, which shows the decidability of the observation-assisted covert attacker synthesis problem. The effectiveness of our approach is illustrated on a water tank example adapted from the literature., Comment: arXiv admin note: text overlap with arXiv:2106.12268

In this work, we investigate how to make use of model reduction techniques to identify the vulnerability of a closed-loop system, consisting of a plant and a supervisor, that might invite attacks. Here, the system vulnerability refers to the existence of key observation sequences that could be exploited by a specific smart sensor attack to cause damage infliction. We consider a nondeterministic smart attack, i.e., there might exist more than one attack choice over each received observation, and adopt our previously proposed modeling framework, where such an attack is captured by a standard finite-state automaton. For a given supervisor S and a smart sensor attack model A, another smart attack model A' is called attack equivalent to A with respect to S, if the resulting compromised supervisor, defined as the composition of the supervisor S and attack model A', is control equivalent to the original compromised supervisor, defined as the composition of S and A. Following the spirit of supervisor reduction that relies on the concept of control congruence, we will show that, this problem of synthesizing a reduced smart attack model A' that is attack equivalent to A with respect to S, can be transformed to a classical supervisor reduction problem, making all existing synthesis tools available for supervisor reduction directly applicable to our problem. A simplified and ideally minimum-state attack model can reveal all necessary observation sequences for the attacker to be successful, thus, reminds system designers to take necessary precautions in advance, which may improve system resilience significantly. An example is presented to show the effectiveness of our proposed attack model reduction technique to identify the system vulnerability.

In this paper, we shall present a topological approach for the computation of some supremal sublanguages, often specified by language equations, which arise from the study of the supervisory control theory. The basic idea is to identify the solutions of the language equations as open sets for some (semi)-topologies. Then, the supremal sublanguages naturally correspond to the supremal open subsets, i.e., the interiors. This provides an elementary and uniform approach for computing various supremal sublanguages encountered in the supervisory control theory and is closely related to a theory of approximation, known as the rough set theory, in artificial intelligence.

In this paper, we consider the problem of synthesis of maximally permissive covert damage-reachable attackers in the setup where the model of the supervisor is unknown to the adversary but the adversary has recorded a (prefix-closed) finite set of observations of the runs of the closed-loop system. The synthesized attacker needs to ensure both the damage-reachability and the covertness against all the supervisors which are consistent with the given set of observations. There is a gap between the de facto maximal permissiveness, assuming the model of the supervisor is known, and the maximal permissiveness that can be attained with a limited knowledge of the model of the supervisor, from the adversary's point of view. We consider the setup where the attacker can exercise sensor replacement/deletion attacks and actuator enablement/disablement attacks. The solution methodology proposed in this work is to reduce the synthesis of maximally permissive covert damage-reachable attackers, given the model of the plant and the finite set of observations, to the synthesis of maximally permissive safe supervisors for certain transformed plant, which shows the decidability of the observation-assisted covert attacker synthesis problem. The effectiveness of our approach is illustrated on a water tank example adapted from the literature.

In this work, we investigate the problem of privacy-preserving supervisory control against an external passive intruder via co-synthesis of dynamic mask, edit function, and supervisor for opacity enforcement and requirement satisfaction. We attempt to achieve the following goals: 1) the system secret cannot be inferred by the intruder, i.e., opacity of secrets against the intruder, and the existence of the dynamic mask and the edit function should not be discovered by the intruder, i.e., covertness of dynamic mask and edit function against the intruder; 2) the closed-loop system behaviors should satisfy some safety and nonblockingness requirement. We assume the intruder can eavesdrop both the sensing information generated by the sensors and the control commands issued to the actuators, and we refer to such an intruder as a sensor-actuator eavesdropping intruder. Our approach is to model the co-synthesis problem as a distributed supervisor synthesis problem in the Ramadge-Wonham supervisory control framework, and we propose an incremental synthesis heuristic to incrementally synthesize a dynamic mask, an edit function, and a supervisor, which consists of three steps: 1) we first synthesize an ensemble ME of dynamic mask and edit function to ensure the opacity and the covertness against a sensor eavesdropping but command non-eavesdropping intruder, and marker-reachability; 2) we then decompose ME into a dynamic mask and an edit function by using a constraint-based approach, with the help of a Boolean satisfiability (SAT) solver; 3) finally, we synthesize a supervisor such that opacity and covertness can be ensured against the sensor-actuator eavesdropping intruder, and at the same time safety and nonblockingness requirement can be ensured. The effectiveness of our approach is illustrated on an example about the enforcement of location privacy for an autonomous vehicle., Comment: arXiv admin note: text overlap with arXiv:2104.04299

This paper investigates the problem of co-synthesis of edit function and supervisor for opacity enforcement in the supervisory control of discrete-event systems (DES), assuming the presence of an external (passive) intruder, where the following goals need to be achieved: 1) the external intruder should never infer the system secret, i.e., the system is opaque, and never be sure about the existence of the edit function, i.e., the edit function remains covert; 2) the controlled plant behaviors should satisfy some safety and nonblockingness requirements, in the presence of the edit function. We focus on the class of edit functions that satisfy the following properties: 1) the observation capability of the edit function in general can be different from those of the supervisor and the intruder; 2) the edit function can implement insertion, deletion, and replacement operations; 3) the edit function performs bounded edit operations, i.e., the length of each string output of the edit function is upper bounded by a given constant. We propose an approach to solve this co-synthesis problem by modeling it as a distributed supervisor synthesis problem in the Ramadge-Wonham supervisory control framework. By taking the special structure of this distributed supervisor synthesis problem into consideration and to improve the possibility of finding a non-empty distributed supervisor, we propose two novel synthesis heuristics that incrementally synthesize the supervisor and the edit function. The effectiveness of our approach is illustrated on an example in the enforcement of the location privacy.

In this work, we study the problem of supervisory control of networked discrete event systems. We consider lossy communication channels with bounded network delays, for both the control channel and the observation channel. By a model transformation, we transform the networked supervisor synthesis problem into the classical (non-networked) supervisor synthesis problem (for non-deterministic plants), such that the existing supervisor synthesis tools can be used for synthesizing networked supervisors. In particular, we can use the (state-based) normality property for the synthesis of the supremal networked supervisors, whose existence is guaranteed by construction due to our consideration of command non-deterministic supervisors. The effectiveness of our approach is illustrated on a mini-guideway example that is adapted from the literature, for which the supremal networked supervisor has been synthesized in the synthesis tools SuSyNA and TCT., Comment: This paper is under review for Automatica

In this work, we address the problem of synthesis of covert attackers in the setup where the model of the plant is available, but the model of the supervisor is unknown, to the adversary. To compensate the lack of knowledge on the supervisor, we assume that the adversary has recorded a (prefix-closed) finite set of observations of the runs of the closed-loop system, which can be used for assisting the synthesis. We present a heuristic algorithm for the synthesis of covert damage-reachable attackers, based on the model of the plant and the (finite) set of observations, by a transformation into solving an instance of the partial-observation supervisor synthesis problem. The heuristic algorithm developed in this paper may allow the adversary to synthesize covert attackers without having to know the model of the supervisor, which could be hard to obtain in practice. For simplicity, we shall only consider covert attackers that are able to carry out sensor replacement attacks and actuator disablement attacks. The effectiveness of our approach is illustrated on a water tank example adapted from the literature., Comment: This paper is under review for the journal of Discrete Event Dynamic Systems

In this paper, we investigate the covert sensor attack synthesis problem in the framework of supervisory control of networked discrete-event systems (DES), where the observation channel and the control channel are assumed to be non-FIFO and have bounded network delays. We focus on the class of sensor attacks satisfying the following properties: 1) the attacker might not have the same observation capability as the networked supervisor; 2) the attacker aims to remain covert, i.e., hide its presence against the networked monitor; 3) the attacker could insert, delete, or replace compromised observable events; 4) it performs bounded sensor attacks, i.e., the length of each string output of the sensor attacker is upper bounded by a given constant. The solution methodology proposed in this work is to solve the covert sensor attack synthesis problem for networked DES by modeling it as the well studied Ramadge-Wonham supervisor synthesis problem, and the constructions work for both the damage-reachable attacks and the damage-nonblocking attacks. In particular, we show the supremal covert sensor attack exists in the networked setup and can be effectively computed by using the normality property based synthesis approach.

This paper presents an overview of the networked supervisory control framework for discrete event systems with imperfect communication networks, which can be divided into the centralized supervisory control setup and the decentralized supervisory control setup. We review the state-of-art networked control frameworks with observation channel delays and control channel delays, for untimed and timed models. Data losses in communication channels are also considered. The review of the state-of-art networked control frameworks will be focused on the following parts: 1) the construction of the networked control closed-loop system 2) the condition to ensure the existence of a networked supervisor 3) the synthesis procedure for networked-delay resilient supervisor 4) the possibility of improving the synthesis efficiency.

Purpose: Dual-energy CT (DECT) has been used to derive relative stopping power (RSP) map by obtaining the energy dependence of photon interactions. The DECT-derived RSP maps could potentially be compromised by image noise levels and the severity of artifacts when using physics-based mapping techniques, which would affect subsequent clinical applications. This work presents a noise-robust learning-based method to predict RSP maps from DECT for proton radiation therapy. Methods: The proposed method uses a residual attention cycle-consistent generative adversarial (CycleGAN) network. CycleGAN were used to let the DECT-to-RSP mapping be close to a one-to-one mapping by introducing an inverse RSP-to-DECT mapping. We retrospectively investigated 20 head-and-neck cancer patients with DECT scans in proton radiation therapy simulation. Ground truth RSP values were assigned by calculation based on chemical compositions, and acted as learning targets in the training process for DECT datasets, and were evaluated against results from the proposed method using a leave-one-out cross-validation strategy. Results: The predicted RSP maps showed an average normalized mean square error (NMSE) of 2.83% across the whole body volume, and average mean error (ME) less than 3% in all volumes of interest (VOIs). With additional simulated noise added in DECT datasets, the proposed method still maintained a comparable performance, while the physics-based stoichiometric method suffered degraded inaccuracy from increased noise level. The average differences in DVH metrics for clinical target volumes (CTVs) were less than 0.2 Gy for D95% and Dmax with no statistical significance. Conclusion: These results strongly indicate the high accuracy of RSP maps predicted by our machine-learning-based method and show its potential feasibility for proton treatment planning and dose calculation.

In this paper, we shall formulate and address a problem of covert actuator attacker synthesis for cyber-physical systems that are modelled by discrete-event systems. We assume the actuator attacker partially observes the execution of the closed-loop system and is able to modify each control command issued by the supervisor on a specified attackable subset of controllable events. We provide straightforward but in general exponential-time reductions, due to the use of subset construction procedure, from the covert actuator attacker synthesis problems to the Ramadge-Wonham supervisor synthesis problems. It then follows that it is possible to use the many techniques and tools already developed for solving the supervisor synthesis problem to solve the covert actuator attacker synthesis problem for free. In particular, we show that, if the attacker cannot attack unobservable events to the supervisor, then the reductions can be carried out in polynomial time. We also provide a brief discussion on some other conditions under which the exponential blowup in state size can be avoided. Finally, we show how the reduction based synthesis procedure can be extended for the synthesis of successful covert actuator attackers that also eavesdrop the control commands issued by the supervisor., Comment: The paper has been accepted for the journal Discrete Event Dynamic Systems

In this paper, we investigate the problem of synthesizing resilient supervisors against combined actuator and sensor attacks, for the subclass of cyber-physical systems that can be modelled as discrete-event systems. We assume that the attackers can carry out actuator enablement and disablement attacks as well as sensor replacement attacks. We consider both risky attackers and covert attackers in the setup where the (partial-observation) attackers may or may not eavesdrop the control commands (issued by the supervisor). A constraint-based approach for the bounded synthesis of resilient supervisors is developed, by reducing the problem to the Quantified Boolean Formulas (QBF) problem. The bounded synthesis problem can then be solved either with a QBF solver or with repeated calls to a propositional satisfiability (SAT) solver, by employing maximally permissive attackers, which can be synthesized with the existing partial-observation supervisor synthesis procedures, as counter examples in the counter example guided inductive synthesis loop., Comment: This paper has been submitted to IEEE Transactions on Automatic Control for review

In this paper, we propose and address the problem of supervisor obfuscation against actuator enablement attack, in a common setting where the actuator attacker can eavesdrop the control commands issued by the supervisor. We propose a method to obfuscate an (insecure) supervisor to make it resilient against actuator enablement attack in such a way that the behavior of the original closed-loop system is preserved. An additional feature of the obfuscated supervisor, if it exists, is that it has exactly the minimum number of states among the set of all the resilient and behavior-preserving supervisors. Our approach involves a simple combination of two basic ideas: 1) a formulation of the problem of computing behavior-preserving supervisors as the problem of computing separating finite state automata under controllability and observability constraints, which can be efficiently tackled by using modern SAT solvers, and 2) the use of a recently proposed technique for the verification of attackability in our setting, with a normality assumption imposed on both the actuator attackers and supervisors., Comment: This paper has been accepted by European Control Conference, 2018. The first two authors contribute equally to this work

Timed discrete-event systems (TDES), which is a modelling formalism proposed by Brandin and Wonham, can be used for modelling scheduling and production planning problems. This paper aims to show that TDES are essentially synchronous product structures. The proof is constructive in the sense that a generalized synchronous product rule is provided to generate a TDES from the activity automaton and the timer automata (that is, the syntactic description of the TDES) after some model transformation. We then also explain how the generalized synchronous product operation can be reduced into the standard synchronous product operation and how to reduce the number of (refined) events introduced in the model transformation. Thus, any software that can compute synchronous products can be used to compute a TDES from its activity automaton and its timer automata, after the model transformation.

In this work, we propose and develop a new discrete-event based actuator attack model on the closed-loop system formed by the plant and the supervisor. We assume the actuator attacker partially observes the execution of the closed-loop system and eavesdrops the control commands issued by the supervisor. The attacker can modify each control command on a specified subset of attackable events. The attack principle of the actuator attacker is to remain covert until it can establish a successful attack and lead the attacked closed-loop system into generating certain damaging strings. We present a characterization for the existence of a successful attacker, via a new notion of attackability, and prove the existence of the supremal successful actuator attacker, when both the supervisor and the attacker are normal (that is, unobservable events to the supervisor cannot be disabled by the supervisor and unobservable events to the attacker cannot be attacked by the attacker). Finally, we present an algorithm to synthesize the supremal successful attackers that are represented by Moore automata., Comment: This work has been submitted to the journal "Discrete Event Dynamic Systems: Theory and Applications". These two authors contribute equally to this work

A reduction of a source distribution is a collection of smaller sized distributions that are collectively equivalent to the source distribution with respect to the property of decomposability. That is, an arbitrary language is decomposable with respect to the source distribution if and only if it is decomposable with respect to each smaller sized distribution (in the reduction). The notion of reduction of distributions has previously been proposed to improve the complexity of decomposability verification. In this work, we address the problem of generating (optimal) reductions of distributions automatically. A (partial) solution to this problem is provided, which consists of 1) an incremental algorithm for the production of candidate reductions and 2) a reduction validation procedure. In the incremental production stage, backtracking is applied whenever a candidate reduction that cannot be validated is produced. A strengthened substitution-based proof technique is used for reduction validation, while a fixed template of candidate counter examples is used for reduction refutation; put together, they constitute our (partial) solution to the reduction verification problem. In addition, we show that a recursive approach for the generation of (small) reductions is easily supported., Comment: Accepted for publication in IEEE Transactions on Automatic Control

In order to handle undesirable failures of a multicopter which occur in either the pre-flight process or the in-flight process, a failsafe mechanism design method based on supervisory control theory is proposed for the semi-autonomous control mode. Failsafe mechanism is a control logic that guides what subsequent actions the multicopter should take, by taking account of real-time information from guidance, attitude control, diagnosis, and other low-level subsystems. In order to design a failsafe mechanism for multicopters, safety issues of multicopters are introduced. Then, user requirements including functional requirements and safety requirements are textually described, where function requirements determine a general multicopter plant, and safety requirements cover the failsafe measures dealing with the presented safety issues. In order to model the user requirements by discrete-event systems, several multicopter modes and events are defined. On this basis, the multicopter plant and control specifications are modeled by automata. Then, a supervisor is synthesized by monolithic supervisory control theory. In addition, we present three examples to demonstrate the potential blocking phenomenon due to inappropriate design of control specifications. Also, we discuss the meaning of correctness and the properties of the obtained supervisor. This makes the failsafe mechanism convincingly correct and effective. Finally, based on the obtained supervisory controller generated by TCT software, an implementation method suitable for multicopters is presented, in which the supervisory controller is transformed into decision-making codes., Comment: 33 pages, 15 figures

In this paper, we model an operational planning and scheduling problem under multiple job deadlines in a time-weighted automaton framework. We first present a method to determine whether all given job specifications and deadlines can be met by computing a supremal controllable job satisfaction sublanguage. When this supremal sublanguage is not empty, we compute one of its controllable sublanguages that ensures the minimum total job earliness by adding proper delays. When this supremal sublanguage is empty, we will determine the minimal sets of job deadlines that need to be relaxed.

The purpose of this study is to determine whether organ sparing and target coverage can be simultaneously maintained for pencil beam scanning (PBS) proton therapy treatment of thoracic tumors in the presence of motion, stopping power uncertainties and patient setup variations. Ten consecutive patients that were previously treated with proton therapy to 66.6/1.8 Gy (RBE) using double scattering (DS) were replanned with PBS. Minimum and maximum intensity images from 4DCT were used to introduce flexible smearing in the determination of the beam specific PTV (BSPTV). Datasets from eight 4DCT phases, using +-3% uncertainty in stopping power, and +-3 mm uncertainty in patient setup in each direction were used to create 8X12X10=960 PBS plans for the evaluation of ten patients. Plans were normalized to provide identical coverage between DS and PBS. The average lung V20, V5, and mean doses were reduced from 29.0%, 35.0%, and 16.4 Gy with DS to 24.6%, 30.6%, and 14.1 Gy with PBS, respectively. The average heart V30 and V45 were reduced from 10.4% and 7.5% in DS to 8.1% and 5.4% for PBS, respectively. Furthermore, the maximum spinal cord, esophagus and heart dose were decreased from 37.1 Gy, 71.7 Gy and 69.2 Gy with DS to 31.3 Gy, 67.9 Gy and 64.6 Gy with PBS. The conformity index (CI), homogeneity index (HI), and global maximal dose were improved from 3.2, 0.08, 77.4 Gy with DS to 2.8, 0.04 and 72.1 Gy with PBS. All differences are statistically significant, with p values <0.05, with the exception of the heart V45 (p= 0.146). PBS with BSPTV achieves better organ sparing and improves target coverage using a repainting method for the treatment of thoracic tumors. Incorporating motion-related uncertainties is essential in maintaining marginal coverage and homogenous dose of treatment targets., Comment: This paper is under review by JACMP