China
Africa
Explore chapters and articles related to this topic
Survivability of Optical Networks
Published in Partha Pratim Sahu, Advances in Optical Networks and Components, 2020
We have already mentioned static protection tree for survivability of network traffic. This problem is minimizing the cost of setting up a multicast tree in a network and has been resolved with and without QoS guarantees such as bandwidth, reliability, delay, and jitter [2,51–53]. This minimum-cost multicast tree is modeled using a minimum Steiner tree [54], and the problem of finding a Steiner Minimum Tree (SMT) in a graph is NP-complete [55]. Two heuristics are employed to resolve SMT problems: Pruned Prim’s Heuristic (PPH) and Minimum-cost Path Heuristic (MPH). In PPH, a minimum spanning tree (MST) is formed by using Prim’s MST algorithm and then clipped by eliminating unwanted arcs. In MPH, the closest destination nodes are selected one by one and added to a partially built tree. Alight-tree is based on a directed Steiner tree, and the problem of finding a Directed Steiner Minimum Tree (DSMT) is NP-complete. In the absence of wavelength converters in a network, this light-tree-based multicast session reveals the wavelength-continuity constraint [56].
Algorithms and Tools
Published in Hamidreza Ahmadian, Roman Obermaisser, Jon Perez, Distributed Real-Time Architecture for Mixed-Criticality Systems, 2018
SMT is a method for checking the satisfiability of logic formulas in first-order formulation against a specific background theory, e.g.,linear integer arithmetic (LA(Z $ \mathcal LA (\mathbb Z $ )) or bit-vectors (BV $ \mathcal BV $ ) [175,176]. A first-order formula consists of variables, quantifiers, logical operators, and functional and predicate symbols [177]. Scheduling problems can be naturally expressed in linear arithmetic and are thus suitable for solving with the use of SMT solvers (see for e.g.,[178]).
Formal Property Verification
Published in Luciano Lavagno, Igor L. Markov, Grant Martin, Louis K. Scheffer, Electronic Design Automation for IC System Design, Verification, and Testing, 2017
Limor Fix, Ken McMillan, Norris Ip, Leopold Haller
The field of SMT attempts to generalize the advances of propositional solvers to fragments of first-order logic interpreted over a given first-order theory. An SMT solver can handle logical formulas that contain variables and operations over some nonpropositional target domain. Popular first-order theories supported by SMT solvers include linear and rational integer arithmetic, equality with uninterpreted functions, bit vectors, and theories for specific data types such as floating-point numbers or arrays. An informative overview over SMT technology is provided in [95]. Modern solvers include Z3 [96], MathSat [97], Yices [98], and CVC4 [99]. The SMT-LIB project [100] standardizes first-order theories handled by solvers as well as file formats.
Preference-Based Multi-Robot Planning for Nuclear Power Plant Online Monitoring and Diagnostics
Published in Nuclear Science and Engineering, 2023
Alan Hesu, Sungmin Kim, Fan Zhang
The LTL-based approach has been extended in a number of areas. Reference [45] uses a cross entropy optimization method to generate agent plans when the task costs are not known a priori. Reference [46] combines the LTL approach and a Markov decision process model to generate plans given uncertainties in task completion from either the environment or robots. The ability to reallocate and replan when conditions change and invalidate the previously generated plan is also discussed in Ref. [46] as well as in Refs. [47] and [48], where both lower-level motion planning and higher-level autonomy and replanning may be required in dynamic environments. The potential for multi-robot, collaborative tasks is also addressed under an LTL framework in Ref. [49] via the addition of a satisfiability modulo theories (SMT) solver.
A Method for Backward Failure Propagation in Conceptual System Design
Published in Nuclear Science and Engineering, 2023
Ali Mansoor, Xiaoxu Diao, Carol Smidts
The proposed method uses propositional logic (PL), which is a branch of discrete mathematics, to translate the physics of a system from conditional statements to logic expressions suitable for mathematical operations. Also known as sentential logic, PL allows the representation of general sentences as formal logical expressions. These logical expressions can be evaluated for satisfiability of a system’s model, which can be performed using a Satisfiability Modulo Theories (SMT)–based solver. It may be noted that adopting a SMT solver for this method allows us to define the system using a higher-order logic. SMT-based verification has been widely used in the software industry for the verification of programs, although it has not been used for deductive failure propagation analysis. The unavailability of operational and failure data for the novel engineering designs makes the physics-based verification of an abstract design a fruitful option. Therefore, building on PL, SMT-based verification for novel system designs is suggested in this research paper.
Safe reinforcement learning for dynamical systems using barrier certificates
Published in Connection Science, 2022
Qingye Zhao, Yi Zhang, Xuandong Li
Recently, neural networks have been adopted as barrier certificates in verifying the safety property of dynamical systems. Zhao et al. (2020) introduce networks with Bent-ReLU activation functions as barrier certificates and rely on the satisfiability modulo theories (SMT) solver iSAT3 (Winterer, 2017) to identify real barrier certificates. Peruffo et al. (2021) propose a counterexample-based, formal, and automated sequential loop to synthesise candidate barrier certificates, and use the SMT solvers dReal (Gao et al., 2013) and Z3 (De Moura & Bjørner, 2008) to certify them. The disadvantage of the above methods is that they only provide safety verification but do not participate in the construction of safe systems.