China
Africa
Explore chapters and articles related to this topic
On the Morality of Artificial Agents
Published in Wendell Wallach, Peter Asaro, Machine Ethics and Robot Ethics, 2020
A transition system comprises a (non-empty) set S of states and a family of operations, called the transitions on S. Each transition may take input and may yield output, but at any rate it takes the system from one state to another and in that way forms a (mathematical) relation on S. If the transition does take input or yield output then it models an interaction between the system and its environment and so is called an external transition; otherwise the transition lies beyond the influence of the environment (at the given LoA) and is called internal. It is to be emphasised that input and output are, like state, observed at a given LoA. Thus the transition that models a system is dependent on the chosen LoA. At a lower LoA an internal transition may become external; at a higher LoA an external transition may become internal.
Formal Methods in the Automotive Domain: The Case of TTA
Published in Nicolas Navet, Françoise Simonot-Lion, Automotive Embedded Systems Handbook, 2017
Bounded model checking [43] is basically a technique to check whether a state-transition system contains an execution that reaches a state in k steps that violates a given property P. This problem can be translated into one determining the satisfiability of the formula F = I(s0) Λ T(s0, s1) Λ ··· Λ T(sk-1,sk) Λ P(sk), where I is a predicate defining the initial states of the system, and T is the transition relation. For finite systems, I and T are encoded as Boolean formulae and satisfiability solvers are used to check the formula. Infinite-state bounded model checkers rely on decision procedures that solve quantifier-free first-order formulae over a combination of decidable theories. As these SMT-solvers have become ever more efficient, bounded model checking has gained increasing attention as a method for analyzing systems.
Applications of Formal Methods, Modeling, and Testing Strategies for Safe Software Development
Published in Qamar Mahboob, Enrico Zio, Handbook of RAMS in Railway Systems, 2018
Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi
In this case, it is the concurrent behavior of the system being specified that stands at the heart of the model. The main idea is to define how the system reacts to a set of stimuli or events. A state of the resulting transition system represents a particular configuration of the modeled system. This formalism, and the derived ones such as statecharts (Harel 1987) and their dialects, is particularly adequate for the specification of reactive, concurrent, or communicating systems and protocols. They are, however, less appropriate to model systems where the sets of states and transitions are difficult to express.
LTL cross entropy optimisation for quadcopter task orchestration
Published in Cyber-Physical Systems, 2023
Christopher Banks, Samuel Coogan, Magnus Egerstedt
We experimentally validate the application of the task orchestration framework through a fire-fighting quadcopters scenario. Consider a set of quadcopters, capable of carrying water, surveying various locations and identifying resources within a predefined area. How does one dynamically allocate these quadcopters to different regions, extinguish fires and monitor their internal states in an efficient manner? Using the task orchestration framework, users give a desired global goal for the team of quadcopters to satisfy; the framework then dynamically allocates tasks to each agent based on input cost and trajectory length, environment and agent constraints and plans trajectories for each agent. Experimentally, we define desired regions as hoops in the work space and generate an environment transition system to indicate how regions are connected. The internal state of a quadcopter is represented as the robot transition system. With these formulations, we consider LTL as the global specification syntax users provide the task orchestration framework.
Expectations for agents with goal-driven autonomy
Published in Journal of Experimental & Theoretical Artificial Intelligence, 2021
Dustin Dannenhauer, Héctor Muñoz-Avila, Michael T. Cox
The state transition system is where actions are executed. After an action is executed the agent will perceive the subsequent state. GDA agents start in some initial state with some initial goal . The planner (shown at the top) receives a problem, , that includes the current state and goal along with the state transition system, . Note that the initial problem will be . The planner then returns a plan with corresponding expectations .
Radiative transition probabilities between low-lying electronic states of N2
Published in Molecular Physics, 2019
Zhi Qin, Junming Zhao, Linhua Liu
The first-positive () system is one of the most important band transition systems in N2 spectrum and has been extensively studied so far. The state is less studied although it has the same symmetry as . In our work, the state is found to have a potential well above the dissociation limit, which enable to carry 9 vibrational levels. Just as transition system, the state is expected to undergo radiative transitions to the state. We calculate the TDMs of the band transition system (given in Table 3), which are then adopted to compute the radiative transition probabilities. Large Einstein coefficients (shown in Table 7) are obtained, which means that this band transition system is most likely to observe experimentally.