China
Africa
Explore chapters and articles related to this topic
Design and Verification Languages
Published in Louis Scheffer, Luciano Lavagno, Grant Martin, EDA for IC System Design, Verification, and Testing, 2018
PSL is based on CTL [46], a powerful but rather cryptic temporal logic for specifying properties of finite-state systems. It is able to specify both safety properties (“this bad thing will never happen”) as well as liveness properties (“this good thing will eventually happen”). Liveness properties can only be checked formally because they make a statement about all the possible behaviors of a system while safety properties can also be tested in simulation. Linear Temporal Logic (LTL), a subset of CTL, expresses only safety properties and can therefore be turned into checking automata meant to be run in concert with a simulationto look for unwanted behavior. PSL carefully defines which subset of its properties are purely LTL and are therefore candidates for use in simulation-based checking.
Temporal Logic Motion Planning in Robotics
Published in Jitendra R. Raol, Ajith K. Gopal, Mobile Intelligent Autonomous Systems, 2016
The formulas of CTL consist of atomic propositions, standard Boolean connectives of prepositional logic and temporal operators. Each temporal operator is composed of two parts, a path quantifier (universal ∀ or existential ∃) followed by a temporal modality (◊, □, X, U). Note that some authors use G and F for ∀ and ∃, respectively. The temporal modalities have the same meanings as in Section 13.4.1. The syntax is given by the BNF: α::=p|¬α|α∨β|α∧β|∃Xα|∃[αUβ]|∀[αUβ]
Modeling and Analysis of Hadoop MapReduce Systems for Big Data Using Petri Nets
Published in Applied Artificial Intelligence, 2021
Dai-Lun Chiang, Sheng-Kuan Wang, Yu-Ying Wang, Yi-Nan Lin, Tsang-Yen Hsieh, Cheng-Ying Yang, Victor R. L. Shen, Hung-Wei Ho
CTL is a branching-time logic which models the system evolution as a tree-like structure where each state can evolve in several ways. Future directions cannot be confirmed, and any branch could become reality. CTL is often used to analyze and verify software and hardware systems (Camilli et al. 2014).