China
Africa
Explore chapters and articles related to this topic
Force-System Resultants and Equilibrium
Published in Richard C. Dorf, The Engineering Handbook, 2018
Mathematical proofs of program properties are based on a formal description of program behavior. A description of program behavior is also known as the semantics of a programming language. There are several approaches to formal semantics. Operational semantics [40] models a computation as a step-bystep process in which commands are executed one after the other. The execution process is modeled on a mathematical, high-level representation of the bits and bytes in an actual computer. Denotational semantics [34] formalizes a program as simply its input-output behavior, that is, in the simplest case, how it maps an initial state to a final state. Axiomatic semantics [25] specifies relationships between program states, such as if a predicate is true of a state, then after executing a command, a somewhat different predicate is true of the next state. Once a formal semantics is in place, we have a foundation for mathematical reasoning about programs. The properties we want to prove must also be stated formally.
Tools and Methodologies for System-Level Design
Published in Louis Scheffer, Luciano Lavagno, Grant Martin, EDA for IC System Design, Verification, and Testing, 2018
Shuvra Bhattacharyya, Wayne Wolf
System-level design is less amenable to synthesis than are logic or physical design. As a result, system-level tools concentrate on modeling, simulation, design space exploration, and design verification. The goal of modeling is to correctly capture the system’s operational semantics, which helps with both implementation and verification. The study of models of computation provides a framework for the description of digital systems. Not only do we need to understand a particular style of computation such as dataflow, but we also need to understand how different models of communication can reliably communicate with each other. Design space exploration tools, such as hardware/software codesign, develop candidate designs to understand trade-offs. Simulation can be used not only to verify functional correctness but also to supply performance and power/energy information for design analysis.
Tools and Methodologies for System-Level Design
Published in Luciano Lavagno, Igor L. Markov, Grant Martin, Louis K. Scheffer, Electronic Design Automation for IC System Design, Verification, and Testing, 2017
Shuvra Bhattacharyya, Marilyn Wolf
System-level design is less amenable to synthesis than are logic or physical design. As a result, system-level tools concentrate on modeling, simulation, design space exploration, and design verification. The goal of modeling is to correctly capture the system’s operational semantics, which helps with both implementation and verification. The study of models of computation provides a framework for the description of digital systems. Not only do we need to understand a particular style of computation, such as dataflow, but we also need to understand how different models of communication can reliably communicate with each other. Design space exploration tools, such as hardware/software codesign, develop candidate designs to understand trade-offs. Simulation can be used not only to verify functional correctness but also to supply performance and power/energy information for design analysis.
Defining adaption measures for organisational multi-agent systems
Published in International Journal of Parallel, Emergent and Distributed Systems, 2023
Michael Köhler-Bußmeier, Jan Sudeikat
The Sonar organisational model [38] is based on Petri nets [5] and the execution loop is defined on top of the operational semantics of Petri nets. The interaction of agents are defined by a distributed workflow nets (Dwfn) , which is a multi-party version of the well-known workflow nets [39] where the interacting parties are called roles. Let be a universe of roles. Each transition of a distributed workflow net is mapped by r to a role with the meaning that a transition t can executed only by an agent that implements the role . If we restrict a DwfnD to transitions belonging to a given set of roles R we obtain the so-called role-component, which defines the service provided by D w.r.t. the role set R. We assume R to be a subset of the roles used in D, i.e. . For singletons we write .
The uncertainty and explainability in object recognition
Published in Journal of Experimental & Theoretical Artificial Intelligence, 2021
2But this form of rule lacks operability. First, what are the semantics of the predicate ? How does the argument in the predicate take from the real image? How do we judge the true value of the proposition after is instantiated? Second, in addition to , the airplane is also involved in other predicates, such as . There is a spatial position constraint between and , so how are the two predicates correlated? Finally, the airplane is diverse. For example, Wing’s form and size are not unique. Is it enough to use the predicate to express this uncertainty? It is for these reasons that traditional symbolic reasoning methods are difficult to use for object recognition. This is essentially a classic problem in artificial intelligence, the semantic grounding problem, a reappearance of how to implement the predicate meaning on the image. Formalising relatively macro predicates is easy, and it is difficult to materialise relatively micro-operational semantics.
Analysis of P-time event graphs in (max,+) and (min,+) semirings
Published in International Journal of Systems Science, 2021
Pavel Špaček, Jan Komenda, Sébastien Lahaye
We recall that according to the operational semantics of this PTEG every token entering a place p must stay in p at least time units and at most time units before this token becomes available for firing of its downstream transition. Note that for place it means that the token must spend in P1 exactly 40 time units. In some places () the upper bound of the sojourn time of token is finite, which means that the upper bound must be respected, while in other places (P8, P9, P10, P11) there is symbol ‘Inf’ as an upper bound of the sojourn time meaning the upper bound equals ∞ (i.e. there is no upper bound constraint for this place). This case with infinite upper bound is typical for places, which do not model an industrial operation, but rather some availability constraint.