Search results for: reachability

Authors: Riddhi Jangid, Gajendra Pratap Singh

Abstract:

Petri nets, a formalized modeling language that was introduced back around 50-60 years, have been widely used for modeling discrete event dynamic systems and simulating their behavior. Reachability analysis of Petri nets gives many insights into a modeled system. This idea leads us to study the reachability technique and use it in the reachability problem in the state space of reachable markings. With the same concept, Crisp Boolean Petri nets were defined in which the marking vectors that are boolean are distinct in the reachability analysis of the nets. We generalize the concept and define ‘Crisp’ Petri nets that generate the marking vectors exactly once in their reachability-based analysis, not necessarily Boolean.

Keywords: marking vector, n-vector, Petri nets, reachability

Procedia PDF Downloads 47

Authors: Ahmad Termimi Ab Ghani, Kojiro Higuchi

Abstract:

In this paper, we present some results of simultaneous infinite games. We mainly work with generalized reachability games and Buechi games. These games are two-player concurrent games where each player chooses simultaneously their moves at each step. Our goal is to give simple expressions of values for each game. Moreover, we are interested in the question of what type of optimal (ε-optimal) strategy exists for both players depending on the type of games. We first show the determinacy (optimal value) and optimal (ε-optimal) strategies in generalized reachability games. We provide a simple expressions of value of this game and prove the existence of memoryless randomized ε-optimal strategy for Player I in any generalized reachability games. We then observe games with more complex objectives, games with Buechi objectives. We present how to compute an ε-optimal strategies and approximate a value of game in some way. Specifically, the results of generalized reachability games are used to show the value of Buechi games can be approximated as values of some generalized reachability games.

Keywords: optimal Strategies, generalized reachability games, Buechi games

Procedia PDF Downloads 564

Authors: Riddhi Jangid, Gajendra Pratap Singh

Abstract:

Petri nets, a mathematical tool, is used for modeling in different areas of computer sciences, biological networks, chemical systems and many other disciplines. A Petri net model of a given system is created by the graphical representation that describes the properties and behavior of the system. While looking for the behavior of any system, 1-safe Petri nets are of particular interest to many in the application part. Boolean Petri nets correspond to those class in 1- safe Petri nets that generate all the binary n-vectors in their reachability analysis. We study the class by changing different parameters like the token counts in the places and how the structure of the tree changes in the reachability analysis. We discuss here an extended class of Boolean Petri nets that generates n-ary trees in their reachability-based analysis.

Keywords: marking vector, n-vector, petri nets, reachability

Procedia PDF Downloads 52

Authors: Jung-Min Yang

Abstract:

Corrective control enables us to change the stable state behavior of an asynchronous sequential machine without modifying inner logic of the machine. This paper addresses corrective control for asynchronous machines with switching capability. The considered asynchronous machine consists of a set of different submachines and switches to each machine according to a constant switching sequence. The control goal is to design a corrective controller such that the closed-loop system can match the behavior of a reference model. The reachability of the switched asynchronous machine is described by a logic calculation of the reachability of submachines. The design procedure of the proposed corrective controller is outlined, and the applicability of the proposed scheme is validated in an example.

Keywords: switched asynchronous sequential machines, corrective control, state feedback, switching sequences

Procedia PDF Downloads 424

Authors: Jung–Min Yang

Abstract:

Solvability of the model matching problem for input/output switched asynchronous sequential machines is discussed in this paper. The control objective is to determine the existence condition and design algorithm for a corrective controller that can match the stable-state behavior of the closed-loop system to that of a reference model. Switching operations and correction procedures are incorporated using output feedback so that the controlled switched machine can show the desired input/output behavior. A matrix expression is presented to address reachability of switched asynchronous sequential machines with output equivalence with respect to a model. The presented reachability condition for the controller design is validated in a simple example.

Keywords: asynchronous sequential machines, corrective control, model matching, input/output control

Procedia PDF Downloads 305

Authors: Hyunsun Lee, Yi Zhu

Abstract:

Wireless ad-hoc network is a decentralized type of temporary machine-to-machine connection that is spontaneous or impromptu so that it does not rely on any fixed infrastructure and centralized administration. As unmanned aerial vehicles (UAVs), also called drones, have recently become more accessible and widely utilized in military and civilian domains such as surveillance, search and detection missions, traffic monitoring, remote filming, product delivery, to name a few. The communication between these UAVs become possible and materialized through Flying Ad-hoc Networks (FANETs). However, due to the high mobility of UAVs that may cause different types of transmission interference, it is vital to design robust routing protocols for FANETs. In this talk, the multicast routing method based on a modified stochastic branching process is proposed. The stochastic branching process is often used to describe an early stage of an infectious disease outbreak, and the reproductive number in the process is used to classify the outbreak into a major or minor outbreak. The reproductive number to regulate the local transmission rate is adapted and modified for flying ad-hoc network communication. The performance of the proposed routing method is compared with other well-known methods such as flooding method and gossip method based on three measures; average reachability, average node usage and average branching factor. The proposed routing method achieves average reachability very closer to flooding method, average node usage closer to gossip method, and outstanding average branching factor among methods. It can be concluded that the proposed multicast routing scheme is more efficient than well-known routing schemes such as flooding and gossip while it maintains high performance.

Keywords: Flying Ad-hoc Networks, Multicast Routing, Stochastic Branching Process, Unmanned Aerial Vehicles

Procedia PDF Downloads 82

Authors: Michael Naderhirn, Marco Pavone

Abstract:

Problem statement, motivation, and aim of work: So far, the development of control algorithms was done by control engineers in a way that the controller would fit a specification by testing. When it comes to the certification of an autonomous car in highly complex scenarios, the challenge is much higher since such a controller must mathematically guarantee to implement the rules of the road while on the other side guarantee aspects like safety and real time executability. What if it becomes reality to solve this demanding problem by combining Formal Verification and System Theory? The aim of this work is to present a workflow to solve the above mentioned problem. Summary of the presented results / main outcomes: We show the usage of an English like language to transform the rules of the road into system specification for an autonomous car. The language based specifications are used to define system functions and interfaces. Based on that a formal model is developed which formally correctly models the specifications. On the other side, a mathematical model describing the systems dynamics is used to calculate the systems reachability set which is further used to determine the system input boundaries. Then a motion planning algorithm is applied inside the system boundaries to find an optimized trajectory in combination with the formal specification model while satisfying the specifications. The result is a control strategy which can be applied in real time independent of the scenario with a mathematical guarantee to satisfy a predefined specification. We demonstrate the applicability of the method in simulation driving scenarios and a potential certification. Originality, significance, and benefit: To the authors’ best knowledge, it is the first time that it is possible to show an automated workflow which combines a specification in an English like language and a mathematical model in a mathematical formal verified way to synthesizes a controller for potential real time applications like autonomous driving.

Keywords: formal system verification, reachability, real time controller, hybrid system

Procedia PDF Downloads 210

Authors: Seong Woo Kwak, Jung-Min Yang

Abstract:

A strategy of fault diagnosis and tolerance for asynchronous sequential machines is discussed in this paper. With no synchronizing clock, it is difficult to diagnose an occurrence of permanent or stuck-in faults in the operation of asynchronous machines. In this paper, we present a fault detector comprised of a timer and a set of static functions to determine the occurrence of faults. In order to realize immediate fault tolerance, corrective control theory is applied to designing a dynamic feedback controller. Existence conditions for an appropriate controller and its construction algorithm are presented in terms of reachability of the machine and the feature of fault occurrences.

Keywords: asynchronous sequential machines, corrective control, fault diagnosis and tolerance, fault detector

Procedia PDF Downloads 315

Authors: Jung-Min Yang

Abstract:

A method of tolerating input faults for input/state asynchronous sequential machines is proposed. A corrective controller is placed in front of the considered asynchronous machine to realize model matching with a reference model. The value of the external input transmitted to the closed-loop system may change by fault. We address the existence condition for the controller that can counteract adverse effects of any input fault while maintaining the objective of model matching. A design procedure for constructing the controller is outlined. The proposed reachability condition for the controller design is validated in an illustrative example.

Keywords: asynchronous sequential machines, corrective control, fault tolerance, input faults, model matching

Procedia PDF Downloads 388

Authors: Loyd R. Hook, Maryam Moharek

Abstract:

With the envisioned future growth of low altitude urban aircraft operations for airborne delivery service and advanced air mobility, strategies to coordinate and deconflict aircraft flight paths must be prioritized. Autonomous coordination and planning of flight trajectories is the preferred approach to the future vision in order to increase safety, density, and efficiency over manual methods employed today. Difficulties arise because any conflict resolution must be constrained by all other aircraft, all airspace restrictions, and all ground-based obstacles in the vicinity. These considerations make pair-wise tactical deconfliction difficult at best and unlikely to find a suitable solution for the entire system of vehicles. In addition, more traditional methods which rely on long time scales and large protected zones will artificially limit vehicle density and drastically decrease efficiency. Instead, strategic planning, which is able to respond to highly dynamic conditions and still account for high density operations, will be required to coordinate multiple vehicles in the highly constrained low altitude urban environment. This paper develops and evaluates such a planning algorithm which can be implemented autonomously across multiple aircraft and situations. Data from this evaluation provide promising results with simulations showing up to 10 aircraft deconflicted through a relatively narrow low-altitude urban canyon without any vehicle to vehicle or obstacle conflict. The algorithm achieves this level of coordination beginning with the assumption that each vehicle is controlled to follow an independently constructed flight path, which is itself free of obstacle conflict and restricted airspace. Then, by preferencing speed change deconfliction maneuvers constrained by the vehicles flight envelope, vehicles can remain as close to the original planned path and prevent cascading vehicle to vehicle conflicts. Performing the search for a set of commands which can simultaneously ensure separation for each pair-wise aircraft interaction and optimize the total velocities of all the aircraft is further complicated by the fact that each aircraft's flight plan could contain multiple segments. This means that relative velocities will change when any aircraft achieves a waypoint and changes course. Additionally, the timing of when that aircraft will achieve a waypoint (or, more directly, the order upon which all of the aircraft will achieve their respective waypoints) will change with the commanded speed. Put all together, the continuous relative velocity of each vehicle pair and the discretized change in relative velocity at waypoints resembles a hybrid reachability problem - a form of control reachability. This paper proposes two methods for finding solutions to these multi-body problems. First, an analytical formulation of the continuous problem is developed with an exhaustive search of the combined state space. However, because of computational complexity, this technique is only computable for pairwise interactions. For more complicated scenarios, including the proposed 10 vehicle example, a discretized search space is used, and a depth-first search with early stopping is employed to find the first solution that solves the constraints.

Keywords: strategic planning, autonomous, aircraft, deconfliction

Procedia PDF Downloads 65

Authors: Alok Tiwari, Ming Show Wong

Abstract:

Lanthanum (La) doped Barium Tin Oxide (BaSnO₃) film is an excellent alternative for expensive Transparent Conducting Oxides (TCOs) film such as Indium Tin Oxide (ITO). However single crystal film of La-doped BaSnO₃ has been reported with a good amount of conductivity and transparency but in order to improve its reachability, it is important to grow doped BaSO₃ films on an inexpensive substrate. La-doped BaSnO₃ thin films have been grown on quartz substrate by Radio Frequency (RF) sputtering at a different substrate temperature (from 200⁰C to 750⁰C). The thickness of the film measured was varying from 360nm to 380nm with varying substrate temperature. Structure, optical and electrical properties have been studied. The carrier concentration is seen to be decreasing as we enhance the substrate temperature while mobility found to be increased up to 9.3 cm²/V-S. At low substrate temperature resistivity found was lower (< 3x10⁻³ ohm-cm) while sudden enhancement was seen as substrate temperature raises and the trend continues further with increasing substrate temperature. Optical transmittance is getting better with higher substrate temperature from 70% at 200⁰C to > 80% at 750⁰C. Overall, understanding of changes in microstructure, electrical and optical properties of a thin film by varying substrate temperature has been reported successfully.

Keywords: conductivity, perovskite, mobility, TCO film

Procedia PDF Downloads 135

Authors: Svetlana Cojocaru, Mircea Petic, Inga Titchiev

Abstract:

Humanity faces more and more often with different social disasters, which in turn can generate new accidents and catastrophes. To mitigate their consequences, it is important to obtain early possible signals about the events which are or can occur and to prepare the corresponding scenarios that could be applied. Our research is focused on solving two problems in this domain: identifying signals related that an accident occurred or may occur and mitigation of some consequences of disasters. To solve the first problem, methods of selecting and processing texts from global network Internet are developed. Information in Romanian is of special interest for us. In order to obtain the mentioned tools, we should follow several steps, divided into preparatory stage and processing stage. Throughout the first stage, we manually collected over 724 news articles and classified them into 10 categories of social disasters. It constitutes more than 150 thousand words. Using this information, a controlled vocabulary of more than 300 keywords was elaborated, that will help in the process of classification and identification of the texts related to the field of social disasters. To solve the second problem, the formalism of Petri net has been used. We deal with the problem of inhabitants’ evacuation in useful time. The analysis methods such as reachability or coverability tree and invariants technique to determine dynamic properties of the modeled systems will be used. To perform a case study of properties of extended evacuation system by adding time, the analysis modules of PIPE such as Generalized Stochastic Petri Nets (GSPN) Analysis, Simulation, State Space Analysis, and Invariant Analysis have been used. These modules helped us to obtain the average number of persons situated in the rooms and the other quantitative properties and characteristics related to its dynamics.

Keywords: lexicon of disasters, modelling, Petri nets, text annotation, social disasters

Procedia PDF Downloads 174

Authors: N. Nivedita, S. Durbha

Abstract:

Critical Infrastructure (CI) consists of services and technological networks such as healthcare, transport, water supply, electricity supply, information technology etc. These systems are necessary for the well-being and to maintain effective functioning of society. Critical Infrastructures can be represented as nodes in a network where they are connected through a set of links depicting the logical relationship among them; these nodes are interdependent on each other and interact with each at other at various levels, such that the state of each infrastructure influences or is correlated to the state of another. Disruption in the service of one infrastructure nodes of the network during a disaster would lead to cascading and escalating disruptions across other infrastructures nodes in the network. The operation of Healthcare Infrastructure is one such Critical Infrastructure that depends upon a complex interdependent network of other Critical Infrastructure, and during disasters it is very vital for the Healthcare Infrastructure to be protected, accessible and prepared for a mass casualty. To reduce the consequences of a disaster on the Critical Infrastructure and to ensure a resilient Critical Health Infrastructure network, knowledge, understanding, modeling, and analyzing the inter-dependencies between the infrastructures is required. The paper would present inter-dependencies related to Healthcare Critical Infrastructure based on Hierarchical Coloured Petri Nets modeling approach, given a flood scenario as the disaster which would disrupt the infrastructure nodes. The model properties are being analyzed for the various state changes which occur when there is a disruption or damage to any of the Critical Infrastructure. The failure probabilities for the failure risk of interconnected systems are calculated by deriving a reachability graph, which is later mapped to a Markov chain. By analytically solving and analyzing the Markov chain, the overall vulnerability of the Healthcare CI HCPN model is demonstrated. The entire model would be integrated with Geographic information-based decision support system to visualize the dynamic behavior of the interdependency of the Healthcare and related CI network in a geographically based environment.

Keywords: critical infrastructure interdependency, hierarchical coloured petrinet, healthcare critical infrastructure, Petri Nets, Markov chain

Procedia PDF Downloads 493

Authors: Abolfazl Zaraki, Yoshikatsu Hayashi, Harry Thorpe, Vincent Strong, Gisle-Andre Larsen, William Holderbaum

Abstract:

Thanks to the high maneuverability of the cable-driven hyper-redundant manipulators (HRMs), this class of robots has shown a superior capability in highly confined and unstructured space applications. Although the large number of degrees of freedom (DOF) of HRMs enhances the motion flexibility and the robot’s reachability range, it highly increases the complexity of the kinematic configuration which makes the kinematic control problem very challenging or even impossible to solve. This paper presents our current progress achieved on the development of a kinematic-based leader-follower control system which is designed to control not only the robot’s body posture but also to control the trajectory of the robot’s movement in a semi-autonomous manner (the human operator is retained in the robot’s control loop). To obtain the forward kinematic model, the coordinate frames are established by the classical Denavit–Hartenburg (D-H) convention for a hyper-redundant serial manipulator which has a controlled cables-driven mechanism. To solve the inverse kinematics of the robot, unlike the conventional methods, a leader-follower mechanism, based on the sequential inverse kinematic, is followed. Using this mechanism, the inverse kinematic problem is solved for all sequential joints starting from the head joint to the base joint of the robot. To verify the kinematic design and simulate the robot motion, the MATLAB robotic toolbox is used. The simulation result demonstrated the promising capability of the proposed leader-follower control system in controlling the robot motion and trajectory in our confined space application.

Keywords: hyper-redundant robots, kinematic analysis, semi-autonomous control, serial manipulators

Procedia PDF Downloads 134

Authors: Arnesh Vijay

Abstract:

Ever since its early introduction in the late 1980s, the mobile industry has been rapidly evolving with each passing year. The development witnessed is not just in its ability to support diverse applications, but also its extension into diverse technological means to access and offer various services to users. Amongst the various technologies present, radio systems have clearly emerged as a strong contender, due to its fine attributes of accessibility, reachability, interactiveness, and cost efficiency. These advancements have no doubt guaranteed unprecedented ease, utility and sophistication to the cell phone users, but caused uncertainty due to the interdependence of various systems, making it extremely complicated to exactly map concepts on to 3GPP (3rd Generation Partnership Project) standards. Although the close interrelation and interdependence of intellectual property rights and mobile standard specifications have been widely acknowledged by the technical and legal community; there, however, is a requirement for clear distinction between the scope and future-proof of inventions to influence standards and its market place adoptability. For this, collaborative work is required between intellectual property professionals, researchers, standardization specialists and country specific legal experts. With the evolution into next generation mobile technology, i.e., to 5G systems, there is a need for further work to be done in this field, which has been felt now more than ever before. Based on these lines, this poster will briefly describe the importance of intellectual property rights in the European market. More specifically, will analyse the role played by intellectual property in various standardization institutes, such as 3GPP (3rd generation partnership project) and ITU (International Telecommunications Union). The main intention: to ensure the scope and purpose is well defined, and concerned parties on all four sides are well informed on the clear significance of good proposals which not only bring economic revenue to the company but those that are capable of improving the technology and offer better services to mankind. The poster will comprise different sections. The first segment begins with a background on the rapidly evolving mobile technology, with a brief insight on the industrial impact of standards and its relation to intellectual property rights. Next, section two will succinctly outline the interplay between patents and standards; explicitly discussing the ever changing and rapidly evolving relationship between the two sectors. Then the remaining sections will examine ITU and its role played in international standards development, touching upon the various standardization process and the common patent policies and related guidelines. Finally, it proposes ways to improve the collaboration amongst various sectors for a more evolved and sophisticated next generation mobile telecommunication system. The sole purpose here is to discuss methods to reduce the gap and enhance the exchange of information between the two sectors to offer advanced technologies and services to mankind.

Keywords: mobile technology, mobile standards, intellectual property rights, 3GPP

Procedia PDF Downloads 95