408 research outputs found
Penguatan Program CHSE Mendukung Kebangkitan Pariwisata dan Bali Reborn di Banjar Penestanan Kelod, Desa Sayan
No full textPariwisata menjadi sektor paling terdampak akibat pandemi Corona Virus Disease (Covid-19). Provinsi Bali sebagai penyumbang terbesar sektor pariwisata di negara Indonesia menjadi salah satu destinasi yang paling terkena dampak dari pandemi ini. Salah satu pusat destinasi di Bali yang sangat terkenal sampai mancanegara adalah Desa Sayan, Kecamatan Ubud, Kabupaten Gianyar. Banjar Penestanan Kelod merupakan salah satu banjar yanga ada di Desa Sayan yang beberapa penyedia jasa akomodasinya masih belum menerapkan cleanliness, health, safety and environmental sustainability (CHSE) dengan baik. Dari hasil diskusi tim pengabdian dengan kader didapatkan beberapa permasalahan terkait penerapan CHSE. Permasalahan tersebut diantaranya masih kurangnya pengetahuan yang didapatkan kader mengenai program CHSE yang diselenggarakan oleh Kementerian Pariwisata dan Ekonomi Kreatif yang harus diterapkan di masa new normal pada destinasi wisata. Masih minimnya pengetahuan kader tentang bagaimana penyebaran virus Corona yang telah melumpuhkan pariwisata Bali. Para kader masih sedikit memiliki gambaran dan informasi mengenai protokol kesehatan yang baik dan tepat guna mencegah penyebaran Covid-19 ini. Metode yang digunakan dalam pengabdian ini adalah diawali dengan sosialisasi program kepada mitra, Focus Group Discussion (FGD) dengan kader, pemberian edukasi tentang CHSE dan pencegahan penyebaran Covid-19 dan pelatihan tentang penerapan CHSE. Hasil dari kegiatan pengabdian ini adalah semua kelompok mitra telah mampu melakukan kegiatan program penguatan CHSE di Banjar Penestanan Kelod, Desa Sayan. Kegiatan “peer†penerapan CHSE dan pencegahan penyebaran Covid-19 sudah berjalan dengan lancar. FGD telah mampu merumuskan permasalahan yang para kader alami dalam penerapan program CHSE, kendala-kendala pun sudah terpecahkan. Saran yang dapat kami berikan dalam kegiatan pengabdian ini adalah agar kelompok mitra dapat menjadi ujung tombak perekrutan mitra lainnya sebagai partner dalam melakukan kegiatan “peer†penguatan program CHSE dalam mendukung bangkitnya pariwisata dan Bali reborn di Desa Sayan, Kecamatan Ubud, Kabupaten Gianyar
A two-level path planning and monitoring architecture for real-world autonomous driving systems
Get PDFIn the past two decades, the safety of autonomous vehicles has drawn in-creasing attention from both academic researchers and industrial experts.This work presents a novel two-level path planning and monitoring architecture to promote safety in autonomous driving. We implemented a HybridA* offline path planner that can generate paths for the vehicle to navigate through static obstacles. The path is guaranteed to be achievable by the vehicle. Also an online monitor is developed using reachability analysis. It simulates the movements of the vehicle based on the vehicle’s physical model and checks the safety of interaction between the vehicle and surrounding dynamic environment in near-real-time (∼0.1 s). The combined architecture, as part of the GEM project, has been tested in both real world and simulation environments. In the experiments, the output path from the path planner is always achievable by the vehicle without colliding with static obstacles, and the online monitor shows high fidelity in predictions while the running time is only slightly longer than that of a simple baseline algorithm.Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2022-05-01The student, Tianqi Liu, accepted the attached license on 2020-05-06 at 10:47.The student, Tianqi Liu, submitted this Thesis for approval on 2020-05-06 at 10:57.This Thesis was approved for publication on 2020-05-11 at 08:42.DSpace SAF Submission Ingestion Package generated from Vireo submission #15246 on 2020-08-25 at 17:29:50Made available in DSpace on 2020-08-26T23:58:39Z (GMT). No. of bitstreams: 2
LIU-THESIS-2020.pdf: 6370962 bytes, checksum: 5ecf3a1c62c07191fee2f0a2599e8daa (MD5)
LICENSE.txt: 4207 bytes, checksum: 6e40987a0801efe8336a07d123e610cd (MD5)
Previous issue date: 2020-05-11Embargo set by: Seth Robbins for item 115775
Lift date: 2022-08-26T23:58:55Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemAuthor requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemU of I Onl
Software tools for scenario verification of autonomous systems exploiting dynamical symmetries
Get PDFSubmission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-12-01The student, Yangge Li, accepted the attached license on 2021-12-06 at 15:39.The student, Yangge Li, submitted this Thesis for approval on 2021-12-06 at 16:08.This Thesis was approved for publication on 2021-12-06 at 16:30.DSpace SAF Submission Ingestion Package generated from Vireo submission #17393 on 2022-04-06 at 17:17:56Made available in DSpace on 2022-04-29T21:46:19Z (GMT). No. of bitstreams: 2
LI-THESIS-2021.pdf: 3056683 bytes, checksum: 7f2c59f98c06ea3e190abbaa6179b13a (MD5)
LICENSE.txt: 4206 bytes, checksum: d2456dff4f67d41461426012486e2156 (MD5)
Previous issue date: 2021-12-06Embargo set by: Seth Robbins for item 123375
Lift date: 2024-04-29T21:46:25Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemEmbargo set by: Seth Robbins for item 123375
Lift date: 2024-04-29T21:47:53Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemAuthor requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemU of I OnlyIn this thesis, we discuss using formal verification techniques to ensure the safety of autonomous systems. We present a particular type of verification problem called scenario verification, which involves vehicles executing complex plans in large cluttered workspaces.
To solve the scenario verification problem, we present the tool SceneChecker. SceneChecker converts the scenario verification problem to a standard hybrid system verification problem and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. SceneChecker implements symmetry abstractions, a novel refinement algorithm, and is built to enhance the performance of existing reachability analysis tools as a plug-in subroutine. We evaluated SceneChecker on several complicated scenarios with different types of agents. Compared to two leading tools, DryVR and Flow*, SceneChecker shows 20x speedup in verification time, even while using those tools as reachability subroutines.
We further look into a variation of the scenario verification problem, with multiple agents running independently in the shared workspace. In addition, the plan is generated as the agent executing the scenario, which requires safety checking to be performed during runtime. To solve this problem, we present Swerve, an open-source cloud computing toolkit for efficient runtime collision checking for multi-agent autonomous systems. Swerve implements a remote server to check safety for different agents by using boundedtime reachability analysis. In addition, Swerve implements a cache to store already computed reachable sets and reuses them to avoid repeated computations. We evaluate Swerve on several scenarios and are able to show that Swerve is able to properly detect potential collisions between agents and static obstacles. In addition, we show that with symmetry and caching, Swerve is able to obtain 16x average speedup in service response time
State estimation of switched nonlinear systems and systems with bounded inputs: Entropy and bit rates
Get PDFState estimation is a fundamental problem when monitoring and controlling dynamical systems. Engineering systems interconnect sensing and computing devices over shared bandwidth-limited channels, and therefore, estimation algorithms should strive to use bandwidth optimally. Often, the dynamics of these systems are affected by external factors. In certain cases, these factors would lead the system to switch between different modes. In other cases, they would affect the dynamics of the system continuously in time without leading to explicit mode transitions. In this thesis, we present two notions of entropy for state estimation of nonlinear switched and non-autonomous dynamical systems as lower bounds on the average number of bits needed to be sent from the sensors to the estimators to estimate the states with deterministic (worst case) error bounds. Our approach relies on the notion of topological entropy and uses techniques from control under limited information. Since the computation of these entropies is hard in general, we compute corresponding upper bounds. Additionally, we design a state estimation algorithm for switched systems when their modes cannot be observed. We show that the average bit rate used by the algorithm is optimal in the sense that the efficiency gap is within an additive constant from the gap between the entropy of the considered system and its computed upper-bound. Finally, we apply our theory and algorithms to linear and nonlinear models of systems such as a glycemic index for diabetic patients, a controller of a Harrier jet and a Pendulum.Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2019-12-01The student, Hussein Sibai, accepted the attached license on 2017-12-15 at 15:44.The student, Hussein Sibai, submitted this Thesis for approval on 2017-12-15 at 15:49.This Thesis was approved for publication on 2017-12-15 at 16:00.DSpace SAF Submission Ingestion Package generated from Vireo submission #11998 on 2018-03-13 at 09:58:00Made available in DSpace on 2018-03-13T15:28:45Z (GMT). No. of bitstreams: 2
SIBAI-THESIS-2017.pdf: 685850 bytes, checksum: 665f514c5b7ff03fa95dfe46673267db (MD5)
LICENSE.txt: 4210 bytes, checksum: 28f03afbc2f358f290426af5e2be40d1 (MD5)
Previous issue date: 2017-12-15Embargo set by: Seth Robbins for item 105229
Lift date: 2020-03-13T15:28:52Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemU of I Only Restriction Lifted for Item 105229 on 2020-03-14T09:15:31Z
Automatic simulation-driven reachability using matrix measures
Get PDFSimulation-driven verification is a promising approach that provides formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set over-approximations from a set of initial states through numerical simulations. This thesis introduces algorithms for this key step, which relies on computing piece-wise exponential bounds on the rate at which trajectories starting from neighboring states converge or diverge. We call this discrepancy function. The algorithms rely on computing local bounds on the matrix measure of the Jacobian matrices. We discuss different techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function is locally minimized.
The proposed methods enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy function give soundness and relative completeness of the overall simulation-driven safety verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the approach.Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2018-08-01The student, Chuchu Fan, accepted the attached license on 2016-07-15 at 15:42.The student, Chuchu Fan, submitted this Thesis for approval on 2016-07-15 at 15:50.This Thesis was approved for publication on 2016-07-18 at 10:29.DSpace SAF Submission Ingestion Package generated from Vireo submission #9968 on 2016-11-10 at 12:25:29Made available in DSpace on 2016-11-10T18:43:03Z (GMT). No. of bitstreams: 2
FAN-THESIS-2016.pdf: 716203 bytes, checksum: 77e377890b4498a11edb70e480df23d8 (MD5)
LICENSE.txt: 4207 bytes, checksum: 102da73cd46f53afa5c17cc69676127b (MD5)
Previous issue date: 2016-07-18Embargo set by: Seth Robbins for item 95492
Lift date: 2018-11-10T18:43:22Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemU of I Only Restriction Lifted for Item 95492 on 2018-11-11T10:15:36Z
A verification framework for hybrid systems
Get PDFThesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007.Includes bibliographical references (p. 193-205) and index.Combining; discrete state transitions with differential equations, Hybrid system models provide an expressive formalism for describing software systems that interact with a physical environment. Automatically checking properties, such as invariance and stability, is extremely hard for general hybrid models, and therefore current research focuses on models with restricted expressive power. In this thesis we take a complementary approach by developing proof techniques that are not necessarily automatic, but are applicable to a general class of hybrid systems. Three components of this thesis, namely, (i) semantics for ordinary and probabilistic hybrid models, (ii) methods for proving invariance, stability, and abstraction, and (iii) software tools supporting (i) and (ii), are integrated within a common mathematical framework. (i) For specifying nonprobabilistic hybrid models, we present Structured Hybrid I/O Automata (SHIOAs) which adds control theory-inspired structures, namely state models, to the existing Hybrid I/O Automata, thereby facilitating description of continuous behavior. We introduce a generalization of SHIOAs which allows both nondeterministic and stochastic transitions and develop the trace-based semantics for this framework. (ii) We present two techniques for establishing lower-bounds on average dwell time (ADT) for SHIOA models. This provides a sufficient condition of establishing stability for SHIOAs with stable state models. A new simulation-based technique which is sound for proving ADT-equivalence of SHIOAs is proposed. We develop notions of approximate implementation and corresponding proof techniques for Probabilistic I/O Automata. Specifically, a PIOA A is an E-approximate implementation of B, if every trace distribution of A is c-close to some trace distribution of B-closeness being measured by a metric on the space of trace distributions.(cont.) We present a new class of real-valued simulation functions for proving c-approximate implementations, and demonstrate their utility in quantitatively reasoning about probabilistic safety and termination. (iii) We introduce a specification language for SHIOAs and a theorem prover interface for this language. The latter consists of a translator to typed high order logic and a set of PVS-strategies that partially automate the above verification techniques within the PVS theorem prover.by Sayan Mitra.Ph.D
Localization of robot and landmark with indistinguishability
No full textWe research localization problems with robots and landmarks related to the aspect of indistinguishability in multi-dimensional spaces. With the initial position ranges for the robot and landmarks using specific measurement models, we develop a general algorithm for minimizing the position ranges under various conditions, which are related to the number of dimensions, the number of landmarks, and the value of the measurement model radius. We also study the characteristics of indistinguishable systems to derive propositions that are useful to help us distinguish the optimal ranges for robots and landmarks.Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2027-12-01The student, Ye Liu, accepted the attached license on 2025-12-04 at 12:06.The student, Ye Liu, submitted this Thesis for approval on 2025-12-04 at 12:13.This Thesis was approved for publication on 2025-12-11 at 10:15.DSpace SAF Submission Ingestion Package generated from Vireo submission #23059 on 2026-02-19 at 18:46:4
Compositional bounded reachability using time partitioning and abstraction
Get PDFAutomatic verification of cyber-physical systems (CPS) typically involves computing the reachable set of states of such systems. This computation is known to be exponential in the number of continuous variables. For systems that can be decomposed into separate components with lower dimensionality, we present an algorithm that verifies global safety properties of the complete system using the reach sets of the components. Here, the components are only coupled through a shared time variable. Using a satellite system case study, we are able to show significant savings in memory and runtime computation costs for this approach. For systems whose components are coupled through additional continuous variables, we present an abstraction to overapproximate the interaction between the components such that the aforementioned algorithm can be used. The feasibility of this abstraction is demonstrated experimentally, which also shows additional work is necessary to develop a more efficient abstraction.Item withdrawn by Mark Zulauf ([email protected]) on 2012-07-18T14:59:19Z
Item was in collections:
University of Illinois Theses & Dissertations (ID: 1)
No. of bitstreams: 1
Green_Jeremy.pdf: 558271 bytes, checksum: 247b7fbaf074fee20019eb7cd44c4cb0 (MD5)Made available in DSpace on 2012-09-18T21:12:45Z (GMT). No. of bitstreams: 2
Green_Jeremy.pdf: 558271 bytes, checksum: 247b7fbaf074fee20019eb7cd44c4cb0 (MD5)
license.txt: 4062 bytes, checksum: b9f13395f27fb350a4e492038fb4c05f (MD5
Location sensitive shared memory implementation for mobile system
No full textThis thesis presents the implementation of an attributed key-value store distributed shared memory (DSM) that provides a way of programming distributed robotics applications. Traditional message-passing method requires the programmer to explicitly specify when and how information should be propagated between different agents while allowing them to communicate. In contrast with the message-passing method, shared memory makes the communication more implicit, allowing the agents to exchange information through read and write operations on shared variables. This feature allows a broad set of algorithms being implemented with more sufficient programs. To reduce the message overheads, an alternative type of shared memory is implemented. The alternative publish/subscribe shared memory will only deliver messages to intended receivers instead of broadcasting all the messages. This property especially benefits applications where one agent requests information from only a subset of neighbors. The shared memory and the publish/subscribe system does reduce the number of messages compared to the shared memory.U of I OnlyUndergraduate senior thesis not recommended for open acces
Fault-tolerant distributed cyber-physical systems: two case studies
No full textFault-tolerance in distributed computing systems has been investigated extensively in the literature and has a rich history and detailed theory. This thesis studies fault-tolerance for distributed cyber-physical systems (DCPS), where distributed computation is combined with dynamics of physical processes. Due to their interaction with the physical world, DCPS may suffer from failures that are qualitatively different from the types of failures studied in distributed computing. Failures of the components of DCPS which interact with the physical processes---such as actuators and sensors---must be considered. Failures in the cyber domain may interact with failures of sensors and actuators in adverse ways.
This thesis takes a first step in analyzing fault-tolerance in DCPS through the presentation of two case studies. In each case study, the DCPS are modeled as distributed algorithms executed by a set of agents, where each agent acts independently based on information obtained from its communication neighbors and agents may suffer from various failures. The first case study is a distributed traffic control problem, where agents control regions of roadway to move vehicles toward a destination, in spite of some agents' computers crashing permanently. The second case study is a distributed flocking problem, where agents form a flock, or a roughly equally spaced distribution in one dimension, and move towards a destination, in spite of some agents' actuators becoming stuck at some value.
Each algorithm incorporates self-stabilization in order to solve the problem in spite of failures. The traffic algorithm uses a local signaling mechanism to guarantee safety and a self-stabilizing routing protocol to guarantee progress. The flocking algorithm uses a failure detector combined with an additional control strategy to ensure safety and progress.Item withdrawn by Mark Zulauf ([email protected]) on 2010-04-25T16:08:02Z
Item was in collections:
University of Illinois Theses & Dissertations (ID: 1)
No. of bitstreams: 2
Johnson_Taylor.zip: 2947778 bytes, checksum: 6b41f0e740bf0ad382fc1858b494bae2 (MD5)
Johnson_Taylor.pdf: 1372164 bytes, checksum: bcaaa8bdb0fc902dd595fd3c7ef64584 (MD5)Made available in DSpace on 2010-05-19T18:40:12Z (GMT). No. of bitstreams: 3
Johnson_Taylor.zip: 2947778 bytes, checksum: 6b41f0e740bf0ad382fc1858b494bae2 (MD5)
Johnson_Taylor.pdf: 1372164 bytes, checksum: bcaaa8bdb0fc902dd595fd3c7ef64584 (MD5)
license.txt: 4064 bytes, checksum: ad61452a3d1d4f15d0d18a47539a246a (MD5
- …
