China 
Africa 
Explore chapters and articles related to this topic
Multi-Aerial-Robot Planning
Published in Yasmina Bestaoui Sebbane, Multi-UAV Planning and Task Allocation, 2020
The cost function can evaluate the steady state time between satisfying instances of ∏. This form of the cost is motivated by persistent monitoring tasks, where the long-term behavior is optimized. A timed automaton can be considered. The semantics of the timed automaton can be understood as follows: starting from the initial state qA0, the values of all clocks increase at rate one, and the system remains at this state until a clock constraint corresponding to an outgoing transition is satisfied. When this happens, the transition is immediately taken, and the clocks in the clock regions are reset [456]. A timed automaton has a finite set of clock regions RA, which is the set of equivalence classes of clock valuations induced by its clock constraints GA. A clock region r ∈ RA is a subset of the infinite set of all clock valuations of CA in which all clock valuations are equivalent in the sense that the future behavior of the system is the same. A clock region is either a corner point (0, 1), an open line segment x ∈ [0, 1] or an open region 0 ≤ x1 ≤ x2 ≤ 1. The clock region RA of a timed automaton A induces an equivalence relation à over its state space.
Modeling and Simulation Concepts
Published in Gabriel A. Wainer, Discrete-Event Modeling and Simulation, 2017
Timed automata, in particular, use clocks to describe the model’s timing behavior [21]. The automaton is defined as a graph of states associated with clocks that determine the passage of time since the occurrence of an event. Every link is associated with a timing constraint that will define when the transition can be triggered. Whenever a transition executes, the associated clocks are reset. Timing constraints can also be associated with the model states, defining the duration of each of the states.
Formal Methods in the Automotive Domain: The Case of TTA
Published in Nicolas Navet, Françoise Simonot-Lion, Automotive Embedded Systems Handbook, 2017
For the startup problem, a central aspect is how to adequately capture the notion of time in the formal model. Timed automata are a successful formalism for the verification of real-time systems and treat time in the most realistic formal way as a continuous variable. Still, model checking timed automata are decidable, and there are specialized model checking tools such as Kronos and UPPAAL. Lônn [21] considers startup algorithms for TDMA systems similar to TTA and verifies one of them using UPPAAL.
A method for reliability detection of automated guided vehicle based on timed automata
Published in Systems Science & Control Engineering, 2021
Xuefeng Deng, Bingqian Zhou, Xinyi Sun, Hua Yang, Lingyu Chen
A timed automata is a finite automaton with a set of clocks. A clock set is a finite set of clocks, each of which is a variable with a value range of 0 or positive numbers. Transitions between timed automata states can only occur if clock constraints are satisfied. The state of a timed automata can be attached with the property of ‘position invariance’, which is also a clock constraint to ensure that the state does not stay in place. This kind of automation is called a ‘time safe automaton’. The timed automata not only has several real-valued variables attached but also is an abstract model of the timing system. The state of a clock can only jump if it satisfies the clock constraint. The state transitions of each node of the timed automata are closely related to time, that is, whether an action can occur at a certain time interval is completely determined by all the time values related to the behaviour of the system. The timed automata tool does not provide a reliability calculation method in the modelling process. Here, a counter related to reliability calculation is introduced to complete the analysis of the system state. The counter is added in the state transition of timed automata to complete the calculation function of reliability.
Formal analysis and control of timed automata with guards using (max, +) and (min, +) algebras
Published in International Journal of Systems Science, 2020
F. Ait Oumeziane, R. Kara, S. Amari
Several tools have been introduced and experienced for modelling, control and performance analysis of Discrete Event Systems (DES). Among those, some models have been proposed to handle the dynamic behaviour of these systems and describe their timing mechanisms, which can be grouped into the theory of timed DES. However, automata-based models have the advantage of more easily calculating the durations of transitions and sequences. The model of timed automata initially introduced by Alur et al. (1990), is an extension of the finite automaton model with clock variables and simple constraints over clocks and states. This formalism offers the possibility of model the dynamic behaviour expressed in a real-time basis and the logical behaviour of discrete event systems. Based on works on timed transition systems (Henzinger et al., 1991), a first extension of those automata was proposed in Alur and Dill (1994), in order to prevent deadlocks in the systems caused by time elapsing (no more transition is validated for the clocks values). This tool was used more often for verification by model-checking and was the basis for the conception of UPPAAL timed automata (Bengtsson et al., 1996). Another form of modelling used to quantitatively model the behaviours of discrete event systems is the automata with multiplicities in algebra (also called automata) which combine two approaches: automata model and the approach based on algebra introduced in Baccelli et al. (1992). In Gaubert (1995), the author demonstrates that automata can handle some characteristics of DES such as conflicts or choices, which cannot be expressed with conventional automata. Numerous publications, during the last few years, have used automata for performance evaluation (Boukra et al., 2015; Gaubert & Mairesse, 1999). In this study, we deal with an extended class of timed automata which is Timed Automata with Guards (TAGs). Instead of exact times, this formalism has timed transitions with time intervals (guards) that can model some uncertainties in DES (as an alternative to stochastic approaches). This makes it useful for industrial applications where the durations of tasks and other data are not accurate (Li & Ierapetritou, 2008).